<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>