Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
New page: n-types cover
added a bunch of hyperlinks and cross-linked with relevant entries
Thanks! I moved the link to h-set to the section “In homotopy type theory”, and removed the link to suspension since it is not the same as delooping.
I’ve heard both terms used for the operation , where is a monoidal category and is the corresponding one-object bicategory. (I usually say delooping for that.) Perhaps the difference should be explained somewhere.
Hm, I don’t remember having linked to suspension…
It’s a bad habit of some category theorists to say “suspension” for delooping. A related bad habit is to write for geometric realization of a category.
While we do have looping and delooping with a fair bit detail, I suppose the entry suspension is lacking some homotopy theoretic discussion. It’s scattered at stable (infinity,1)-category and elsewhere I suppose.
I have no time to do much at all on the nLab right now, though.
The page has
By the Kripke-Joyal semantics of homotopy type theory,
following which link we see only
Kripke–Joyal semantics is a natural semantics in a topos.
Presumably the latter should say something about extending to the -case.
Maybe first though some detail nees to be given at Kripke-Joyal semantics.
Yeah…
1 to 7 of 7