Equality between paths

Question

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.

Answer 1

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