There is a wonderful paper by Rijke=C2=A0detailing an interesting construction c=
alled the "join construction". I would argue that interesting is =
a vast understatement because it details how to construct images of maps in=
HoTT. This encapsulates many interesting constructions in HoTT: set quotie=
nts, propositional truncation and Rezk completion.

-- Now s=
uppose we have a "oo-group" which can be taken as a pointed connt=
ected type BG with map pt : 1 --> BG. The iterated join construction on =
pt gives the classical Milnor-construction. In the case where BG =3D K(Z/2,=
1) the real projective spaces are obtained (synthetic homotopically mind yo=
u) which is expanded on elsewhere=C2=A0with Buchholtz. When BG =3D K(Z,2) we obtain a definition =
for the complex projectve spaces.

It is hinted at =
that this construction may be modified to obtiain grassmannians, I would li=
ke to know some more details about this. But it would seem to me that BO(n)=
would need to be known which is kindof circular if one defines it as an in=
finite grassmannian.

Mike has said on Mathoverflow=C2=A0that SU(n) wo=
uld probably be constructed as BSU(n) in HoTT and obiously loop spaced to g=
et an automatic group structure. If we are to define BSU(n) as a complex gr=
assmannian then I don't see how we can do it the Rijke-Buchholtz way. B=
ecause then it seems we would have to know BSU(n) anyway.

I would like to hear the communities thoughts on this problem a=
nd whether there is any proposed solution.

- Ali C=
aglayan

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.

For more options, visit http= s://groups.google.com/d/optout.

------=_Part_1409_2021303900.1537143621922-- ------=_Part_1408_1630523090.1537143621922--