Just for the record, a trivial but nice observation: = the unknot is the representation of S3 as the join of S1 with itself:
=

=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 p2
S1 x S1 ------> S1
=C2=A0=C2=A0 |=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 |
=C2=A0=C2=A0 | p1=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 |
=C2=A0=C2=A0 V=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 V
=C2=A0 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 inducti= ve types.

Best,
Egbert
=

On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.=