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.
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