Как мне найти дополнительные ограничения, помимо граничных условий? - PullRequest
Новая
       47

Как мне найти дополнительные ограничения, помимо граничных условий?

0 голосов
/ 05 августа 2020

В следующем коде Agda у меня есть одна дыра с некоторым потенциальным заполнением; увы, начинка не проверяется. Кажется, он соответствует всем ограничениям, которые показывает Agda, поэтому я хотел бы знать, где я могу найти, какие еще есть невидимые ограничения. 

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Data.Nat

module UntypedNominalTerms
  (A : Type)
  where

  data Term : Type where
    var : ℕ → (x : A) → Term
    rename : ∀ n m x → var n x ≡ var m x
    trunc : isSet Term

  module _ (P : Term → Type) (PIsProp : ∀ x → isProp (P x))
    (P₀ : ∀ n X → P (var n X)) where

    elimIntoProp : ∀ t → P t
    elimIntoProp (var n X) = P₀ n X
    elimIntoProp (rename n m x i) = {!transport-filler Pt≡Ps Pt i!}
      where
        t s : Term
        t = var n x
        s = var m x

        q : t ≡ s
        q = rename n m x

        Pt : P t
        Pt = P₀ n x

        Ps : P s
        Ps = P₀ m x

        Pt≡Ps : P t ≡ P s
        Pt≡Ps = λ j → P (q j)
    elimIntoProp (trunc t s p q i j) = r (elimIntoProp t) (elimIntoProp s) (cong elimIntoProp p) (cong elimIntoProp q) (trunc t s p q) i j
      where
      r : isOfHLevelDep 2 P
      r = isOfHLevel→isOfHLevelDep (suc (suc zero)) λ t → isOfHLevelSuc 1 (PIsProp t)

Итак, в отверстии с правой стороны elimIntoProp (rename n m x i), если я попрошу Agda показать мне цель и тип, он покажет мне соответствующий тип и покажет мне граничные условия, которым должен удовлетворять transport-filler: 

Goal: P (rename n m x i)
Have: P (rename n m x i)
———— Boundary ——————————————————————————————————————————————
i = i0 ⊢ P₀ n x
i = i1 ⊢ P₀ m x

At i = i0 , у нас есть transport-filler Pt≡Ps Pt i0, которое должно быть Pt определено как P₀ n x, а в i = i1 у нас есть Ps, которое определяется как P₀ m x. Так что, похоже, у нас все в порядке.

Но когда я пытаюсь заменить отверстие его содержимым, я получаю ошибку типа: 

P₁ m x != transp (λ i → Pt≡Ps n m x i1 i) i0 (Pt n m x i1)
of type P₂ (rename n m x i1)
when checking the definition of elimIntoProp

Откуда это ограничение и как показать это (и подобные) в окне goal-and-context во время редактирования?

1 Ответ

1 голос
/ 06 августа 2020

transport-filler Pt≡Ps Pt i1 не Ps, однако вы можете увидеть это, запросив нормальную форму:

transp (λ i₁ → P (rename n m x i₁)) i0 (P₀ n x)

, поэтому нарушаемое ограничение действительно является граница.

(Другие соответствующие ограничения могут отображаться под контекстом, но в этом случае они снова являются просто границей.)

...