Categories with families

Indexed presentation

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

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:

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.)

References

  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