[Agda] Simple(?) cubical agda isomorphism
Tom Jack
tom at tomjack.co
Tue Apr 12 01:53:59 CEST 2022
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>
More information about the Agda
mailing list