category object in an (∞,1)-category, groupoid object
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
The naive 2-category of internal categories in a category does not have enough equivalences in general, due to the failure of the axiom of choice in . The functors which should be equivalences are called weak equivalences, and one often works with the localisation of at the weak equivalences. Roughly speaking, a weak equivalence is a functor which is ‘fully faithful’ and ‘essentially surjective’, but these terms need to be interpreted appropriately.
The concept of weak equivalences first arose in work of Bunge and Paré on stack completions of internal categories.
Let be a functor between categories internal to some category . is fully faithful if the following diagram is a pullback
To discuss the analogue of essential surjectivity, we need a notion of ‘surjectivity’, as this does not generalise cleanly from . If we are working in a topos, a natural choice is to take epimorphisms, but weaker ambient categories are sometimes needed. A natural choice is to work in a unary site, where the covers are taken as the ‘surjective’ maps.
Given a functor internal to a unary site , is essentially -surjective if the map is a -cover.
We then define an internal functor to be a -equivalence if it is fully faithful and essentially -surjective.