[Agda] Simple(?) cubical agda isomorphism

[Dan Krejsa]

Thank you, Tom,
I'll take some time to digest that.
- Dan

On Mon, Apr 11, 2022, 16:54 Tom Jack <tom at tomjack.co> wrote:

> 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/0b1d1946/attachment.html>