Yeah…

]]>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 $\infty$-case.

Maybe first though some detail nees to be given at Kripke-Joyal semantics.

]]>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 $B$ 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.

]]>I’ve heard both terms used for the operation $M \mapsto \mathrm{B} M$, where $M$ is a monoidal category and $\mathrm{B} M$ is the corresponding one-object bicategory. (I usually say delooping for that.) Perhaps the difference should be explained somewhere.

]]>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.

]]>added a bunch of hyperlinks and cross-linked with relevant entries

]]>New page: n-types cover

]]>