路径之间的平等 [英] Equality between paths

问题描述

使用 cubical-demo 库，我想证明以下内容很简单：

Using the cubical-demo library, I thought the following would be trivial to prove:

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

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

可惜，它在定义上并不成立：尝试使用 refl 失败，

But alas, it doesn't hold definitionally: trying to use refl fails with

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

，我不知道从哪里开始。

and I don't know where to start.

推荐答案

不，可悲的是，在使用Path时，我们失去了一些定义上的相等性，因为如果添加这些缩减，我们不知道如何保持系统的融合。

No, sadly we lose some definitional equalities when using Path, because we don't know how to keep the system confluent if we were to add those reductions.

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

The eliminator of the Id type instead has the usual reduction rules.

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

在引理的情况下，您想证明有关 trans 的信息在

In the case of the lemma you want to prove about trans you can find a proof at

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

顺便说一下，三次演示有机地增长了，我们希望以更干净的设置（虽然有不同的基元）在

By the way, cubical-demo grew up organically, and we are starting fresh with hopefully a cleaner setup (altough with different primitives) at

https://github.com/agda/cubical

立方具有更好的 Id 模块，例如：

cubical has a better Id module for example:

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

这篇关于路径之间的平等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！