[Agda] How can I prove algebraic laws of HITs in Cubical Agda?

[Caryo Scelus]

On Sat, 2 Feb 2019 19:44:44 +0900
Hiromi ISHII <konn.jinro at gmail.com> wrote:

> Hi there,
> 
> I'm recently experimenting with Cubical Agda to implement some
> data-structures and algorithms within Cubical Type Theory.
> I have some problems to understand why my proof doesn't work
> in cubical settings.
> The detail is explained below.
> The complete code is available on [GitHub].
> 
> Why such error occurs? What is the proper way to prove such identities
> within Cubical Type Theory?
> I would appreciate if anyone kindly teach me.

Hello,

While i wasn't able to fix the proof on the spot, i believe the reason
for the error is the same as in the following simplified example:

data [0-1] : Set where
  𝟎 𝟏 : [0-1]
  int : 𝟎 ≡ 𝟏

0⇒x : (P : [0-1] → Set) (p : P 𝟎) → ∀ x → P x
-- 0⇒x P p 𝟎 = p
-- doesn't work: p != transp (λ i → P (int (i0 ∧ i))) i0 p of
-- type P (int i0)
0⇒x P p 𝟎 = subst P refl p -- this works
0⇒x P p 𝟏 = subst P int p
0⇒x P p (int i) = subst P (λ j → int (i ∧ j)) p

It appears that agda requires definitional equality of right-side
expressions corresponding to overlapping (due to paths) left-side
patterns; to check that, it substitutes interval variables with i0 and
i1 (reducing `rotate a l r j₀` to `mkQ (l L.∷ʳ a) r` and `mkQ l (r L.∷ʳ
a)`). Since equalities for cubical operations (subst/transp in mine
case, probably applies to hcomp as well) do not hold definitionally,
agda complains. So i would guess that in order for proof to work, you
need to rewrite your base case to match (reduced) path case. Hope that
would help