[Agda] Stuck on a cubical example

[Guillaume Allais]

Hi Wolfram,

I have updated the post to change 0/1 to i0/i1. Thanks for the suggestion.

I agree that this datatype is useless. This started as an attempt to make
the example as simple as possible and as I mention in the conclusion it
still took me a lot of time to figure out to prove the more complex result.

Tonight I have experimented a bit with a list + swap (with and without an
additional path for truncation). Thanks to the List⁰ experiment, I now
understand enough to quickly define _++_ and prove a right identity & an
associativity lemma but `swaps : ∀ x xs → x ∷ xs ≡ xs ++ x ∷ []` still
escapes me.

Lessons learned with the List⁰ experiment are evidently not enough to tackle
interesting problems. But they're a start.

Cheers,
--
gallais


On 06/03/2019 22:02, Wolfram Kahl wrote:
> Hi Guillaume,
>
>> https://gallais.github.io/blog/first-cubical-experiment
> Nice, thanks!
>
> I just find it confusing that you refer to ``0'' and ``1'',
> while the cubical Agda documentation appears to make it clear
> that in Agda these are called ``i0'' and ``i1''.
>
> (I am consciously staying a cubical outsider who, as Agda user,
>  wants to see what cubical Agda has to offer.
>  I am therefore especially interested in documentation
>  that assumes familiarity with Agda, but no familiarity
>  with cubical type theory.
>  (I guess there are (still) more Agda users
>   than cubical insiders...  ;-)
>  )
>
>  Your ``del'' is, IMO, not very convincing:
>  Why would I want to have a list type where all lists are equal?
>  (And why don't you even explain that?)
>
>  An actual application could possibly be had by constructing
>  multisets via:
>
>    swap : ∀ x y e → x ∷ y ∷ e ≡ y ∷ x ∷ e
>
>  Or am I missing something?
> )
>
>
> Wolfram
>


-------------- 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/bfeb8829/attachment.sig>