homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
A weak inverse is like an inverse, but weakened to work in situations where being an inverse on the nose would be evil.
Given a functor , a weak inverse of is a functor with natural isomorphisms
If it exists, a weak inverse is unique up to natural isomorphism, and furthermore can be improved to form an adjoint equivalence, where and sastisfy the triangle identities.
More generally, given a -category and a morphisms in , a weak inverse of is a morphism with -isomorphisms
Weak inverses give the proper notion of equivalence of categories and equivalence in a -category. Note that you must use anafunctors to get the weak notion of equivalence of categories here without using the axiom of choice.
Given the geometric realization of categories functor , weak inverses are sent to homotopy inverses. This is because the product with the interval groupoid is sent to the product with the topological interval . In fact, less is needed for this to be true, because the classifying space of the interval category is also the topological interval. If we define a lax inverse to be given by the same data as a weak inverse, but with and replaced by natural transformations, then the classifying space functor sends lax inverses to homotopy inverses. An example of a lax inverse is an adjunction, but not all lax inverses arise this way, as we do not require the triangle identities to hold.
(David Roberts: I’m just throwing this up here quickly, it probably needs better layout or even its own page.)