nLab
weak equivalence of internal categories
Context
Internal categories
Equality and Equivalence
equivalence

equality (definitional , propositional , computational , judgemental , extensional , intensional , decidable )

identity type , equivalence in homotopy type theory

isomorphism , weak equivalence , homotopy equivalence , weak homotopy equivalence , equivalence in an (∞,1)-category

natural equivalence , natural isomorphism

gauge equivalence

Examples.

principle of equivalence

equation

fiber product , pullback

homotopy pullback

Examples.

linear equation , differential equation , ordinary differential equation , critical locus

Euler-Lagrange equation , Einstein equation , wave equation

Schrödinger equation , Knizhnik-Zamolodchikov equation , Maurer-Cartan equation , quantum master equation , Euler-Arnold equation , Fuchsian equation , Fokker-Planck equation , Lax equation

Contents
Idea
The naive 2-category $Cat(S)$ of internal categories in an ambient category $S$ does in general not have enough equivalences of categories , due to the failure of the axiom of choice in $S$ . Those internal functors which should but may not have inverses up to internal natural isomorphism , namely those which are suitably fully faithful and essentially surjective , may be regarded as weak equivalences of internal categories (Bunge & Paré 1979 ). The 2-category theoretic localisation of $Cat(S)$ at this class of 1-morphisms then serves as a more natural 2-category of internal categories .

Definition
Let $f:X\to Y$ be a functor between categories internal to some category $S$ . $f$ is fully faithful if the following diagram is a pullback

$\begin{matrix}
X_1& \stackrel{f_1}{\to} & Y_1 \\
\downarrow&& \downarrow \\
X_0\times X_0 &\underset{f_0\times f_0}{\to} & Y_0\times Y_0
\end{matrix}$

To discuss the analogue of essential surjectivity, we need a notion of ‘surjectivity’, as this does not generalise cleanly from $Set$ . 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 $f:X\to Y$ internal to a unary site $(S,J)$ , $f$ is essentially $J$ -surjective if the map $t\circ pr_2:X_0 \times_{f_0,Y_0,s}Y_1 \to Y_0$ is a $J$ -cover.

We then define an internal functor to be a $J$ -equivalence if it is fully faithful and essentially $J$ -surjective.

References
Marta Bunge , Robert Paré , Stacks and equivalence of indexed categories , Cahiers de Topologie et Géométrie Différentielle Catégoriques, 20 no. 4 (1979), p. 373-399 (numdam:CTGDC_1979__20_4_373_0 )

Tomas Everaert , R.W.Kieboom and Tim Van der Linden , Model structures for homotopy of internal categories , Theory and Applications of Categories 15 (2005), no. 3, 66-94. (journal )

David Roberts , Internal categories, anafunctors and localisation , Theory and Applications of Categories, 26 (2012) No. 29, pp 788-829. (journal )