1

使用该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

我不知道从哪里开始。

4

2 回答 2

4

不，遗憾的是，我们在使用 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

于 2018-11-06T16:27:44.940 回答
1

根据Saizan 的回答，我查找了证据cubical-demo并将其移植到新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
于 2018-11-07T13:16:50.697 回答