[Agda] Stuck on a cubical example

[Anders Mortberg]

Very nice and pedagogic post Guillaume!

Maybe a link should be added to the documentation so that beginners
easily can find it? I think having such a detailed presentation of
what needs to be satisfied for functions on HITs to be well-defined
could be very helpful. The documentation is a bit terse about this at
the moment.

--
Anders


On Wed, Mar 6, 2019 at 11:38 AM Guillaume Allais
<guillaume.allais at ens-lyon.org> wrote:
>
> Thanks Anders,
>
> I have spent some more time working on my example following your advice
> and managed to come up with a solution (in the end there was no need to
> use hcomp).
>
> Now that the cubical doc has been made available on readthedocs, I have
> uploaded a little write-up explaining the solution & discussing why these
> constraints are necessary. Hopefully I haven't said too many stupid things.
> https://gallais.github.io/blog/first-cubical-experiment
>
> Cheers,
> --
> gallais
>
> On 18/02/2019 04:29, Anders Mortberg wrote:
> > 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
>
>