I agree with @varkor, trying to make the nlab fully compatible with homotopy-theoretic foundations is not easy or desirable. Many pages on the nlab freely use the law of excluded middle and axiom of choice and have special comments on how to adapt them to constructive mathematics, so the idea of changing basic notions to homotopy-based ones doesn’t make sense.

]]>I personally really don’t like this trend of “correcting” usages of “category” to say “strict category” instead. Most of the readers of the nLab do not care about formalising category theory in Homotopy Type Theory: for them, a category has a class of objects and a class of morphisms. What you are calling a “strict category” is by definition a “category” for the vast majority of readers. I think this change serves little purpose other than obfuscation. If you really want to mention strictness issues, I think they would be better placed in their own new section.

]]>this factorization only holds for strict categories, for univalent categories one needs to replace bijective-on-objects functors with essentially surjective functors, and with general precategories one needs to replace them with equivalent-on-objects functors, which generalize both bijective-on-objects functors and essentially surjective functors.

Anonymous

]]>