CODEWITHSUNDEEP
equalityagdacubical-type-theoryhomotopy-type-theory
Cactus
Cactus

Reputation: 27636

Equality between paths

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 = ?

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.

Upvotes: 1

Views: 140

Answers (2)

Cactus
Cactus

Reputation: 27636

Based on Saizan's answer I looked up the proof in cubical-demo and ported it to the new cubical library. I can see how it works out (as in, I can see that the value of the given path is x on all three designated edges) but I don't see yet how I would come up with a similar proof for a similar situation:

{-# 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

Upvotes: 1

Saizan
Saizan

Reputation: 1401

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.

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

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

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

cubical has a better Id module for example:

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

Upvotes: 4

Related Questions