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

[Hiromi ISHII]

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

[GitHub]: https://github.com/konn/cubical-agda-playground/blob/master/Deq.agda

My first experiment is to implement a (naïve) deque expressed as a pair of lists,
where the first half corresponds to the front half of the queue, and the latter
part the reversed rear half.
With HITs, one can express non-trivial equality between deques  intuitively:

```agda
data Deq {𝓁} (A : Set 𝓁) : Set 𝓁 where
 mkQ    : List A → List A → Deq A
 rotate : (a : A) (l r : List A) → mkQ (l L.∷ʳ a) r ≡ mkQ l (r L.∷ʳ a)
```

Then, I could easily cons, snoc and (naïve) append operations on them.
The next goal is to prove that this deque forms a monoid, where I get stuck.

My first attempt is to prove the right identity law for deques:

```
++-identityʳ : RightIdentity [] _++_ -- ⇔ ∀ (xs : Deq A) → xs ++ [] ≡ xs
++-identity = ?
```

For the 0-dimensional case, the proof is straightforward (modulo basic properties
of lists):

```
++-identityʳ-base : ∀(l r : List A) → mkQ l r ++ [] ≡ mkQ l r
++-identityʳ-base l r =
   (mkQ (l L.++ L.reverse r) L.[])
 ≡⟨ aux-que-app-rev l (L.reverse r) L.[] ⟩
   (mkQ l (L.reverse (L.reverse r)))
 ≡⟨ cong (mkQ l) (L.reverse-involutive r) ⟩
   mkQ l r
 ∎
```

...and two-dimensional case:

```
   ++-identityʳ-i : ∀(a : A) (l r : List A) (j₀ : I) → rotate a l r j₀ ++ [] ≡ rotate a l r j₀
   ++-identityʳ-i a l r j₀ i =
     hfill
       (λ j → λ { (i = i0) → rotate a l r j ++ [] ; (i = i1) → rotate a l r j })
       (inc (++-identityʳ-base (l L.∷ʳ a) r i))
       j₀
```

So far, so good.
But I got stuck when I tried to combine them to get the entire proof for the right identity for deques.
I wrote the following (failed) proof:

```
++-identityʳ : RightIdentity [] _++_
++-identityʳ (mkQ l r) = ++-identityʳ-base l r
++-identityʳ (rotate a l r j₀) i = ++-identityʳ-i a l r j₀ i
```

Then, Cubical Agda halts with the following error:

```
Checking Deq (/Users/hiromi/Documents/Programming/agda/cubical/Deq.agda).
l L.++ L.reverse (r L.∷ʳ a) !=
hcomp
(λ { j (i = i0) → (l L.∷ʳ a) L.++ L.reverse r
  ; j (i = i1)
      → (l L.++ (a L.∷ L.[]) L.++ L.reverse r ≡⟨
         (λ i₁ → l L.++ L.reverse-++-commute r (a L.∷ L.[]) (~ i₁)) ⟩
         (λ _ → l L.++ L.reverse (r L.∷ʳ a)))
        j
  })
(L.++-assoc l (a L.∷ L.[]) (L.reverse r) i)
of type List A
when checking the definition of ++-identityʳ
```

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.

Thank you in advance,

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