* Eckmann-Hilton for triple loop space
@ 2018-05-05 22:05 Jamie Vicary
0 siblings, 0 replies; only message in thread
From: Jamie Vicary @ 2018-05-05 22:05 UTC (permalink / raw)
To: Homotopy Type Theory
Dear all,
The formalization of the Eckmann-Hilton argument is given in Chapter
2.1 of the HoTT book. Just to fix notation, let me recall the
statement: for any type A, and for any paths a,b:id_A->id_A, there is
a path sigma_{a,b}:a.b->b.a which reverses the order of composition.
If A is itself a loop space, it is then expected that
sigma_{a,b}.sigma_{b,a} = id. (For this to be interesting, I suppose
the sigma_{a,b} would have to be chosen as a natural family, rather
than arbitrarily.) My question is whether this standard observation
has been formalized in homotopy type theory, and if so, where.
Best wishes,
Jamie
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2018-05-05 22:06 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-05-05 22:05 Eckmann-Hilton for triple loop space Jamie Vicary
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).