[Agda] Simple(?) cubical agda isomorphism

[Tom Jack]

Hello, below is one way.

This "csq" is a slight generalization (to two paths p,q) of the
construction used for rotLoop for S1 in the Cubical library
<https://github.com/agda/cubical/blob/ff1c817e35182dedc703ab5a8614d1eb181d265c/Cubical/HITs/S1/Base.agda#L389-L395>
.

Up to homotopy, there is not really any choice for the squares, since c2 is
equivalent to S1 and so is a 1-type. I expect we should have that the
"evaluation at the basepoint" map (λ (h : ∀ y → g y ≡ y) → h b0) is an
equivalence, by analogy with S1.

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"

module _ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) where
  csq-faces : (i j : I) → I → Partial (~ i ∨ i ∨ ~ j ∨ j) A
  csq-faces i j k (i = i0) = p (j ∨ ~ k)
  csq-faces i j k (i = i1) = q (j ∧ k)
  csq-faces i j k (j = i0) = p (i ∨ ~ k)
  csq-faces i j k (j = i1) = q (i ∧ k)

  csq : Path (y ≡ y) refl refl → PathP (λ i → p i ≡ q i) p q
  csq r i j = hcomp (csq-faces i j) (r i j)

  -- note: csq should be equal to transport over this path (but it is
simpler)
  csq-path : Path (Type ℓ) (Path (y ≡ y) refl refl) (PathP (λ i → p i ≡ q
i) p q)
  csq-path k = PathP (λ i → p (i ∨ ~ k) ≡ q (i ∧ k)) (λ j → p (j ∨ ~ k)) (λ
j → q (j ∧ k))

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 : c2) → f (g y) ≡ y
  fgid b0 i = p1 i
  fgid b1 i = p0 i
  fgid (p0 i) j = csq p1 p0 refl i j
  fgid (p1 i) j = csq p0 p1 refl i j

  gfid : (x : c2) → g (f x) ≡ x
  gfid b0 i = p0 (~ i)
  gfid b1 i = p1 (~ i)
  gfid (p0 i) j = csq p0 p1 refl i (~ j)
  gfid (p1 i) j = csq p1 p0 refl i (~ j)

On Mon, Apr 11, 2022 at 2:22 PM Dan Krejsa <dan.krejsa at gmail.com> wrote:

> 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 = {!!}
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220411/bbbea435/attachment-0001.html>