时间戳

首页 > 解决方案 > 我如何找到比边界条件更进一步的约束？

agda - 我如何找到比边界条件更进一步的约束？

问题描述

在下面的 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

在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在编辑过程中如何在窗口中显示这个（和类似的）？

标签： agdacubical-type-theory

解决方案

transport-filler Pt≡Ps Pt i1不是Ps，您可以通过询问正常形式来查看它：

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

所以被违反的约束确实是来自边界的约束。

（其他相关约束可能会显示在上下文下方，但在这种情况下，它们再次只是边界。）

推荐阅读