Just for the record, a trivial but nice observation: the unknot is the representation of S3 as the join of S1 with itself: p2 S1 x S1 ------> S1 | | | p1 | V V S1 ---------> S3 Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Although a trival way to obtain them is through cohesive HoTT would be nice if it were possible to define these spaces directly as higher inductive types. Best, Egbert On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson < danielrichardgrayson@gmail.com> wrote: > Quillen identified the complement of the trefoil knot with > SL(2,R)/SL(2,Z), and the proof is > on page 84 of Milnor's book "Introduction to algebraic K-theory". > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- egbertrijke.com -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.