# Categories with families

## Indexed presentation

definitionCategory with families A category with families (CwF) consists of the following data:

• $\mathcal C$, a category of contexts and substitutions
• $\mathbf 1 \in \mathcal C$, a choice of terminal object
• • • where the actions of and on morphisms $f$ are both denoted $-[f]$.

The terminal object is simply a categorical packaging-up of the context extension operation, consisting of a context $\Gamma.A$, projection morphism $p_A \colon \Gamma.A \rightarrow \Gamma$ and term , such that the usual universal property is satisfied (see e.g. (Hofmann, 1997)).

The structure of a CwF can be (and is frequently) presented as an essentially/generalized algebraic theory. Via the usual definition of a morphism of models of EATs/GATs, one has the notion of a CwF morphism. Here we state this more explicitly for our more categorical formulation. We use the following proposition, easily checked:

proposition Let be a presheaf on $\mathcal D$. Then any functor induces a functor $\int_{\mathcal C} P \circ F \xrightarrow{F^\ast} \int_{\mathcal D} P$ on the categories of elements, given by “reindexing”. todo That is, definitionMorphism of CwFs A morphism of CwFs consists of the following data:

• $F \colon \mathcal C \rightarrow \mathcal C^\prime$ preserving the chosen terminal objects $\mathbf 1, \mathbf 1^\prime$
• , a natural transformation on presheaves • , a natural transformation on presheaves such that for every $\Gamma \in \mathcal C$ and the canonically induced map (strictly) preserves the terminal objects chosen by , .

Spelling out this last part above, this means in particular that and a similar equation for weakening of substitutions.

remark From the data of a CwF we can form a (strict) functor into the category of pullbacks of $\mathcal C$, sending $(\Gamma, A)$ to the projection $\Gamma.A \xrightarrow{p_A} \Gamma$ and $f \colon (\Delta, A[f]) \rightarrow (\Gamma, A)$ to the unique pullback of $p_A$ along $f$. Uniqueness is by terminality, which also gives strictness of this functor.

## Fibered presentation

definitionCategory of families of sets is the category whose objects are set-indexed families of sets, and whose arrows consist of pairs $\big(f \colon I \rightarrow J, (f_i \colon A_i \rightarrow B_{f(i)})_{i \in I}\big),$ i.e. maps respecting the fibers of the family. Composition of arrows is fiberwise. is equivalent to (where $I$ is the walking arrow) via the usual family-fibration correspondence (see e.g. (Capriotti, 2013) for a nice quick introduction): objects of are diagrams $A \rightarrow I$ of sets, and arrows from $A \rightarrow I$ to $B \rightarrow J$ are fiber-preserving maps on the total spaces $A$, $B$.

(To be continued.)

1. Hofmann, M. (1997). Syntax and Semantics of Dependent Types. Semantics and Logics of Computation, 79–130.
2. Capriotti, P. (2013). Families and fibrations. https://www.paolocapriotti.com/blog/2013/02/20/families-and-fibrations/index.html