[Agda] Stuck on a cubical example

[Guillaume Allais]

Hi all,

I have been playing with cubical to try to get my head around it.
Reading the doc currently being written [1] has been helpful in
understanding components such as hcomp, however I am now stuck
and I have no idea what the problem is.

Here is my silly running example. The last equation (using hcomp)
is rejected: one of the side conditions is not respected. Below it
is the diagram I draw to explain my reasoning.

Cheers,

[1] https://github.com/agda/agda/pull/3571

=====================================================
{-# OPTIONS --safe --cubical #-}

module collapse where

open import Cubical.Core.Prelude

data Exp (A : Set) : Set where
  [_] : A → Exp A
  _∷_ : A → Exp A → Exp A
  del : ∀ x y → x ∷ y ≡ y

variable A : Set

_++_ : (e f : Exp A) → Exp A
[ x ]         ++ f = x ∷ f
(x ∷ e)       ++ f = x ∷ (e ++ f)
del x y i     ++ f = del x (y ++ f) i

collapse : (e f : Exp A) → e ++ f ≡ f
collapse [ x ]       f j = del x f j
collapse (x ∷ e)     f j = del x (collapse e f j) j
collapse (del x y i) f j =
  hcomp (λ k → λ { (j = i0) → del x (y ++ f) i
                 ; (j = i1) → del x (collapse y f k) k
                 })
        (del x (y ++ f) (i ∧ ~ j))

{-
hcomp should fill in the following square:

del x (y ++ f) i                                      f
     ^                                                ^
     |                                                |
   refl k                                    del x (collapse y f k) k
     |                                                |
     |                                                |
     |                                                |
del x (y ++ f) i ------------------------------> x ∷ (y ++ f)
                    del x (y ++ f) (i ∧ ~ j)

j = 0                                                j = 1

-}
=====================================================

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190217/f87502a5/attachment.sig>