[Agda] Simple(?) cubical agda isomorphism
Dan Krejsa
dan.krejsa at gmail.com
Mon Apr 11 21:23:51 CEST 2022
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>
More information about the Agda
mailing list