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

[Hiromi ISHII]

Hello Caryo,

> 2019/02/02 20:37、Caryo Scelus <caryoscelus at gmx.com>のメール:
> 
> 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

Thank you for your rapid reply and explanation!
While I haven't figured out the precise correction to be made, but your
suggestion helped me understanding the cause of error. Thanks!

-- Hiromi ISHII
konn.jinro at gmail.com
Doctoral program in Mathematics,
University of Tsukuba