路径之间的平等

Question

使用 cubical-demo 库，我认为以下证明很简单：

{-# OPTIONS --cubical #-}
open import Cubical.PathPrelude

foo : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → trans refl p ≡ p
foo p = ?

但是，遗憾的是，它在定义上并不成立：尝试使用 refl 失败

primComp (λ _ → ;A) (~ i ∨ i) (λ { i₁ (i = i0) → ;x ; i₁ (i = i1) → p i₁ }) (refl i)
!= p i 
of type ;A

我不知道从哪里开始。

Answer 1

不，遗憾的是我们在使用 Path 时失去了一些定义等式，因为如果我们要添加这些减少，我们不知道如何保持系统的一致性。

Id 类型的消除器具有通常的减少规则。

https://github.com/Saizan/cubical-demo/blob/master/src/Cubical/Id.agda

如果你想证明关于 trans 的引理，你可以在

找到证明

https://github.com/Saizan/cubical-demo/blob/master/src/Cubical/Lemmas.agda

顺便说一句，cubical-demo 是有机地成长起来的，我们希望在

有一个更干净的设置（尽管有不同的基元）来重新开始

https://github.com/agda/cubical

cubical 有一个更好的 Id 模块，例如：

https://github.com/agda/cubical/blob/master/Cubical/Core/Id.agda

Answer 2

基于 I looked up the proof in cubical-demo and ported it to the new cubical 库。我可以看到它是如何工作的（例如，我可以看到给定路径的值在所有三个指定边上都是 x）但我还不知道我会如何得出类似的证明类似情况：

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Core.Prelude

refl-compPath : ∀ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) → compPath refl p ≡ p
refl-compPath {x = x} p i j = hcomp {φ = ~ j ∨ j ∨ i}
  (λ { k (j = i0) → x
     ; k (j = i1) → p k
     ; k (i = i1) → p (k ∧ j)
     })
  x

路径之间的平等

Equality between paths

equality

agda

cubical-type-theory

homotopy-type-theory