如何证明荒谬模式的两个应用在 Cubical Agda 中产生相同的结果？

Question

重范畴论（agda-categories）相关问题。

我试图定义一个自然变换并证明它的自然性广场通勤。本质上，我遇到的错误是接受空类型的函数的两个“应用程序”（因此 false quodlibdet 原则）无法返回相同的类型。这是相关的洞：

plugin1unit : NaturalTransformation idF (constantPolynomial ∘F plugIn1)
plugin1unit = record { 
    η = λ X → (λ x → x , λ _ → tt) ⇄ λ fromPos () ;
    commute = λ f@(mapDir ⇄ mapPos) -> {!   !} ;
   }
}

commute

孔的类型是：

((λ x → Arrow.mapPosition f x , (λ _ → tt)) ⇄
       (λ fromPos z → Arrow.mapDirection f fromPos ((λ ()) z)))
      Cubical.≡
      ((λ x → Arrow.mapPosition f x , (λ x₁ → tt)) ⇄
       (λ fromPos z → (λ ()) z))

我不想包括所有的支持定义；我只会在“附录”（问题结尾）中包含

Polynomial

类型及其

Arrow

的定义，以免这篇文章充斥着信息。我得到的错误很简单。如果我足够完善那个洞，这就是我得到的，一步一步： 1.

    commute = λ f@(mapDir ⇄ mapPos) -> λ i → {!   !} ;

目标类型：

Arrow X
      (MkPolynomial
       (Σ (Polynomial.position Y₁) (λ x → Polynomial.direction Y₁ x → ⊤))
       (λ _ → ⊥))

2. （一些自动解决/唯一明显的事情被省略）

    commute = λ f@(mapDir ⇄ mapPos) -> λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ {!   !} ;

目标类型：

(fromPos : Polynomial.position X) →
      ⊥ → Polynomial.direction X fromPos

3. this 提炼为两个参数的函数，当然其中一个是空类型⊥:

    commute = λ f@(mapDir ⇄ mapPos) -> λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ λ fromPos x → {!   !} ;

但是空模式匹配的明显解决方案不适用于以下错误：

(λ { fromPos () }) fromPos z != Arrow.mapDirection f fromPos ((λ ()) z)

如果我定义一个比请求的类型更通用的函数

(fromPos : Polynomial.position X) → ⊥ → Polynomial.direction X fromPos

：

fromAnythingToAnythingElse : {A B : Set} -> A -> ⊥ -> B
fromAnythingToAnythingElse x ()

并尝试在第二步将其放入孔中，我得到另一个关于无法实例化元变量的错误。

这是我认为是基本错误的另一个版本：

“(λ ()) z”怎么能与任何东西不同？根据定义，它返回 any 类型！

Answer 1

你做不到。有多个这样的功能是一致的。也一致只有一个

当我遇到那个问题时（Laplaza 专门针对 Agda 的 Set 的 Rig Categories 的一致性条件之一取决于此），我通过在 () 上仔细

not

匹配解决了它，而是通过了不可能。

我的猜测是您的定义之间存在一些非常微妙的相互作用，您需要弄清楚这些相互作用才能到达那里。

TL;DR：不要过早匹配

()

。这可能不是连贯的定义。