Category with Families

A category with families is a category of ‘contexts’ and ‘substitutions’ with:

• A terminal object $\bullet :\mathrm{Ctx}$ representing the empty context.
• A set of ‘types’ $\mathrm{Ty}\Gamma$ for each context $\Gamma$.
• A set of ‘terms’ $\mathrm{Tm}(\Gamma ,A)$ for each $\Gamma :\mathrm{Ctx};A:\mathrm{Ty}\Gamma$.
• A map for each substitution between types
• A map for each substitution between terms

This can be expressed as a presheaf into $\mathrm{Fam}$ where $\mathrm{Fam}$ denotes a category of sets of terms in a context. TODO: Check & finish both definitions.

Sources

https://ncatlab.org/nlab/show/categorical+semantics+of+dependent+type+theory