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,
remark This is Definition 3.15 of (Ahrens & Lumsdaine, 2019), formulated using total categories. todo
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.)
References
- Hofmann, M. (1997). Syntax and Semantics of Dependent Types. Semantics and Logics of Computation, 79–130.
- Ahrens, B., & Lumsdaine, P. L. F. (2019). Displayed Categories. Logical Methods in Computer Science, Volume 15, Issue 1. https://doi.org/10.23638/LMCS-15(1:20)2019
- Capriotti, P. (2013). Families and fibrations. https://www.paolocapriotti.com/blog/2013/02/20/families-and-fibrations/index.html