[Agda] Stuck on a cubical example

[Anders Mortberg]

Hi Guillaume,

The reason your solution is not working is that you're only making a
line along j, while in fact you need a square depending on both i and
j with the correct boundary. Whatever you write as RHS of

collapse (del x y i) f j = ...

must also agree with the cases of collapse when i=i0 and i=i1, so you
need your solution to satisfy:

collape (del x y i0) f j = collape (x :: y) f j = del x (collapse e f j) j

and

collapse (del x y i1) f j = del y f j

I haven't tried to define collapse myself, but you will need to add (i
= i0) and (i = i1) faces to the hcomp and potentially change the other
faces so that it all matches up. I actually tried to explain exactly
this with the "c2t_bad" example in the documentation of Cubical Agda:

https://github.com/mortberg/agda/blob/cubicaldoc/doc/user-manual/language/cubical.lagda.rst#higher-inductive-types

Suggestions for how to improve the explanations are very welcome!


I also wish Cubical Agda would show you the constraints on the faces
when you're trying to fill in this hole. At the moment I usually solve
this kind of hole by figuring out what I need on paper (by evaluating
the faces by hand) and then trying to fill it in, having editor
support would be very cool and helpful!

--
Anders


Anders
On Sun, Feb 17, 2019 at 10:48 AM Guillaume Allais
<guillaume.allais at ens-lyon.org> wrote:
>
> 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
>
> -}
> =====================================================
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda