Categories fibred in groupoids over a site

Let $\mathcal{C}$ be a category (Category, object, morphism, domain, codomain, identity, composition, and hom-collection). A functor $p:\mathcal{S}\to \mathcal{C}$ (Covariant functor, identity functor, composite functor, and contravariant functor) is a category fibred in groupoids over $\mathcal{C}$ if every arrow $f:V\to U$ of $\mathcal{C}$ and every object $x$ of $\mathcal{S}$ over $U$ admit a cartesian arrow $\phi :y\to x$ over $f$, and every fibre category ${\mathcal{S}}_U$ is a groupoid (Isomorphism, groupoid, and connected category).

Cartesian means: for every $g:W\to V$, every object $z$ of $\mathcal{S}$ over $W$ and every arrow $\psi :z\to x$ with $p(\psi )=fg$, there is a unique arrow $\chi :z\to y$ over $g$ with $\phi \circ \chi =\psi$. The fibre ${\mathcal{S}}_U$ is the subcategory of objects over $U$ and morphisms over ${\mathrm{i}\mathrm{d}}_U$. The condition is equivalent to: every arrow of $\mathcal{S}$ is cartesian, and for every $f:V\to U$ and every object $x$ over $U$ there is an arrow $y\to x$ over $f$. Since an arrow over an identity is an isomorphism exactly when it is cartesian, this is a genuine condition on $p$ and not a matter of choosing arrows.

A 1-morphism $F:(p:\mathcal{S}\to \mathcal{C})\to (q:\mathcal{T}\to \mathcal{C})$ is a functor over $\mathcal{C}$, i.e. $qF=p$ (such a functor automatically preserves cartesian arrows). A 2-morphism is a natural transformation $F\Rightarrow G$ over $\mathcal{C}$, i.e. one whose components lie in the fibres (Natural transformation and its components). An equivalence is a 1-morphism admitting an inverse over the base up to natural isomorphisms over the base. It induces fully faithful, essentially surjective functors on all fibres. Conversely, fibrewise full faithfulness and essential surjectivity imply equivalence when choices of preimages and vertical isomorphisms are supplied for all target objects; for set-sized total categories these choices follow from AC (The Axiom of Choice). Indeed cartesian factorization turns fibrewise full faithfulness into full faithfulness on arrows over each base arrow. For each target object x choose y over the same base object and an isomorphism F(y) to x; full faithfulness lifts the conjugated target arrows uniquely to define the inverse functor and its two natural isomorphisms (Vistoli, Proposition 3.36 and Lemma 3.37). These objects, 1-morphisms and 2-morphisms form a strict 2-category: composition of 1-morphisms is strictly associative and the identity 1-morphisms act strictly; the coherence isomorphisms familiar from a pseudofunctor description appear only after choosing pullbacks.

The definition requires neither a cleavage nor a simultaneous choice of pullbacks. If one does choose, for every arrow $f$, a single cartesian lift of each object $x$, then the chosen lifts compose only up to the canonical isomorphism supplied by cartesian uniqueness, and this global choice may use AC; the fibred-in-groupoids definition requires no such choice. The equivalence criterion above has its separately stated choice hypothesis. In particular the empty category is fibred in groupoids over $\mathcal{C}$ vacuously, and if $\mathcal{S}$ is empty then the fibre categories are empty groupoids.