David Roberts
weak equivalence of internal categories

If $J$ is a pretopology on a category with pullbacks, a $J$-equivalence $f:X\to Y$ between categories internal to $S$ is a functor that is fully faithful? and essentially $J$-surjective. This last means that the map

$$X_0{\times }_{f,Y_0,s}{Y}_1\to Y_1\stackrel{t}{\to }{Y}_0$$X_0 \times_{f,Y_0,s} Y_1 \to Y_1 \stackrel{t}{\to} Y_0

admits local sections with respect to $J$.

When no reference to a particular pretopology is mentioned, such maps will be called weak eqivalences