<div dir="ltr">Hello, below is one way.<div><br></div><div>This "csq" is a slight generalization (to two paths p,q) of the construction used for <a href="https://github.com/agda/cubical/blob/ff1c817e35182dedc703ab5a8614d1eb181d265c/Cubical/HITs/S1/Base.agda#L389-L395">rotLoop for S1 in the Cubical library</a>.</div><div><br></div><div>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.</div><div><br></div><div><font face="monospace">data c2 : Type where<br> b0 : c2<br> b1 : c2<br> p0 : b0 ≡ b1 -- moving from b0 to b1 along p0 is "clockwise"<br> p1 : b1 ≡ b0 -- moving from b1 to b0 along p1 is also "clockwise"<br></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">module _ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) where<br> csq-faces : (i j : I) → I → Partial (~ i ∨ i ∨ ~ j ∨ j) A<br> csq-faces i j k (i = i0) = p (j ∨ ~ k)<br> csq-faces i j k (i = i1) = q (j ∧ k)<br> csq-faces i j k (j = i0) = p (i ∨ ~ k)<br> csq-faces i j k (j = i1) = q (i ∧ k)<br><br> csq : Path (y ≡ y) refl refl → PathP (λ i → p i ≡ q i) p q<br> csq r i j = hcomp (csq-faces i j) (r i j)<br><br> -- note: csq should be equal to transport over this path (but it is simpler)<br> csq-path : Path (Type ℓ) (Path (y ≡ y) refl refl) (PathP (λ i → p i ≡ q i) p q)<br> csq-path k = PathP (λ i → p (i ∨ ~ k) ≡ q (i ∧ k)) (λ j → p (j ∨ ~ k)) (λ j → q (j ∧ k))<br><br>module c2f where<br> f : c2 → c2<br> f x = x<br><br> g : c2 → c2<br> g b0 = b1<br> g b1 = b0<br> g (p0 i) = p1 i<br> g (p1 i) = p0 i<br><br> fgid : (y : c2) → f (g y) ≡ y<br> fgid b0 i = p1 i<br> fgid b1 i = p0 i<br> fgid (p0 i) j = csq p1 p0 refl i j<br> fgid (p1 i) j = csq p0 p1 refl i j<br><br> gfid : (x : c2) → g (f x) ≡ x<br> gfid b0 i = p0 (~ i)<br> gfid b1 i = p1 (~ i)<br> gfid (p0 i) j = csq p0 p1 refl i (~ j)<br> gfid (p1 i) j = csq p1 p0 refl i (~ j)</font><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Apr 11, 2022 at 2:22 PM Dan Krejsa <<a href="mailto:dan.krejsa@gmail.com">dan.krejsa@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi,</div><div><br></div><div>I'm a cubical Agda beginner and I'm trying to do something that seems</div><div>like it ought to be simple. I figure I must be missing some technical trick.</div><div><br></div><div>Consider this HIT, which looks like a circle broken into two halves. b0 is at noon,</div><div>and b1 is at 6 o'clock.<br></div><div><br></div><div>data c2 : Type where<br> b0 : c2<br> b1 : c2<br> p0 : b0 ≡ b1 -- moving from b0 to b1 along p0 is "clockwise"<br> p1 : b1 ≡ b0 -- moving from b1 to b0 along p1 is also "clockwise"<br></div><div><br></div><div>I want to define an isomorphism from c2 to itself, with function f and inverse</div><div>g as below. Note that f is the identity, but g maps each point of the circle</div><div>to the opposite point 180 degrees away. Then I want to define</div><div>fgid to show that g is a section of f, and gfid to show that g is a retract of f.</div><div>(Note that f ∘ g and g ∘ f are definitionally both g, but g should be homotopic</div><div>to the identity on c2, with various choices for the homotopy.)<br></div><div><br></div><div>For y : c2, I want (fgid y) to be a path that goes clockwise 180 degrees from</div><div>f (g y) to y. For x : c2, I want (gfid x) to be a path that goes counterclockwise</div><div>180 degrees from g (f x) to x. Intuitively, it seems to me that it should be possible</div><div>to define both of these continuously on the whole of c2.<br></div><div><br></div><div>I'm a little stuck defining fgid (and assume I'll have the same trouble with</div><div>gfid). Note that since f (g (p0 i)) = p1 i, fgid (p0 i) ought to be a path from</div><div>p1 i clockwise to p0 i. For example, (λ j → p1 (i ∨ j)) ∙ (λ j → p0 (i ∧ j)).</div><div>Likewise, fgid (p1 i) ought to be a path from (p0 i) to (p1 i), moving clockwise,</div><div>e.g. (λ j → p0 (i ∨ j)) ∙ (λ j → p1 (i ∧ j)). However, these won't be accepted</div><div>because they are not definitionally equal paths in the vicinity of b0 or b1.</div><div><br></div><div>For instance, with the above choices,</div><div><br></div><div>fgid (p0 i0) = p1 ∙ refl</div><div>but</div><div>fgid (p1 i1) = refl ∙ p1</div><div><br></div><div>and p1 ∙ refl is definitionally different from refl ∙ p1.</div><div><br></div><div>What is the best way around this?</div><div><br></div><div>- Dan<br></div><div><br></div><div>module c2f where<br> f : c2 → c2<br> f x = x<br><br> g : c2 → c2<br> g b0 = b1<br> g b1 = b0<br> g (p0 i) = p1 i<br> g (p1 i) = p0 i<br><br> -- fgid y moves clockwise 90 degrees from f (g y) to y.<br> fgid : (y : c2) → f (g y) ≡ y<br> fgid b0 = {!!}<br> fgid b1 = {!!}<br> fgid (p0 i) = (λ j → p1 (i ∨ j)) ∙ (λ j → p0 (i ∧ j))<br> fgid (p1 i) = {!(λ j → p0 (i ∨ j)) ∙ (λ j → p1 (i ∧ j))!}<br><br> gfid : (x : c2) → g (f x) ≡ x<br> gfid x = {!!}<br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>