[Agda] Stuck on a cubical example

[Wolfram Kahl]

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