[Agda] Simple(?) cubical agda isomorphism

[Dan Krejsa]

Hi,

I'm a cubical Agda beginner and I'm trying to do something that seems
like it ought to be simple.  I figure I must be missing some technical
trick.

Consider this HIT, which looks like a circle broken into two halves. b0 is
at noon,
and b1 is at 6 o'clock.

data c2 : Type where
  b0 : c2
  b1 : c2
  p0 : b0 ≡ b1 -- moving from b0 to b1 along p0 is "clockwise"
  p1 : b1 ≡ b0 -- moving from b1 to b0 along p1 is also "clockwise"

I want to define an isomorphism from c2 to itself, with function f and
inverse
g as below.  Note that f is the identity, but g maps each point of the
circle
to the opposite point 180 degrees away.  Then I want to define
fgid to show that g is a section of f, and gfid to show that g is a retract
of f.
(Note that f ∘ g  and  g ∘ f  are definitionally both g, but g should be
homotopic
to the identity on c2, with various choices for the homotopy.)

For y : c2, I want (fgid y) to be a path that goes clockwise 180 degrees
from
f (g y) to y.  For x : c2, I want (gfid x) to be a path that goes
counterclockwise
180 degrees from g (f x) to x.  Intuitively, it seems to me that it should
be possible
to define both of these continuously on the whole of c2.

I'm a little stuck defining fgid (and assume I'll have the same trouble with
gfid).  Note that since f (g (p0 i)) = p1 i,  fgid (p0 i) ought to be a
path from
p1 i  clockwise to p0 i.   For example, (λ j → p1 (i ∨ j)) ∙ (λ j → p0 (i ∧
j)).
Likewise, fgid (p1 i) ought to be a path from (p0 i) to (p1 i), moving
clockwise,
e.g. (λ j → p0 (i ∨ j)) ∙ (λ j → p1 (i ∧ j)).   However, these won't be
accepted
because they are not definitionally equal paths in the vicinity of b0 or b1.

For instance, with the above choices,

fgid (p0 i0) = p1 ∙ refl
but
fgid (p1 i1) = refl ∙ p1

and p1 ∙ refl   is definitionally different from  refl ∙ p1.

What is the best way around this?

- Dan

module c2f where
  f : c2 → c2
  f x = x

  g : c2 → c2
  g b0 = b1
  g b1 = b0
  g (p0 i) = p1 i
  g (p1 i) = p0 i

  -- fgid y moves clockwise 90 degrees from f (g y) to y.
  fgid : (y : c2) → f (g y) ≡ y
  fgid b0 = {!!}
  fgid b1 = {!!}
  fgid (p0 i) = (λ j → p1 (i ∨ j)) ∙ (λ j → p0 (i ∧ j))
  fgid (p1 i) = {!(λ j → p0 (i ∨ j)) ∙ (λ j → p1 (i ∧ j))!}

  gfid : (x : c2) → g (f x) ≡ x
  gfid x = {!!}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220411/56304aa9/attachment.html>