[Agda] Stuck on a cubical example

[Guillaume Allais]

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


-------------- 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/20190306/87c53899/attachment.sig>