Consider the problem of defining models of type theory inside HoTT. In particular, we want an internal definition of a *category with families* (CwF). A bit of work has been done on this:

*Shallow embedding of type theory is morally correct*[KKK18]*Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT*[Kr20]

and in the paper which introduces CwFs:

It seems natural to consider two particular varieties of CwF internal to type theory: the set-truncated and “∞-” (i.e. with all higher coherences) versions. For the references listed above, the first is formulated in an extensional metatheory and is automatically truncated, while the second is ∞-.

For this note we’ll focus on the set-truncated version.

# Strict CwFs in HoTT

A category with families may be defined somewhat succinctly as a category \mathscr{C} of “contexts” and “substitutions” with a terminal object \langle\rangle, together with a presheaf (\mathrm{Ty}, \mathrm{Tm}) \colon \mathscr{C}^{op} → \mathrm{Fam} valued over the category of families of sets, along with a comprehension for each \sigma \in \mathrm{Ty}\,\Gamma for arbitrary \Gamma \in \mathscr{C}. (I’ll probably write a short note explaining what all these terms mean in the near future.)

By expanding the above out in full as a generalized algebraic theory we can define a CwF type theoretically as a Σ-type consisting of the usual structures and equations. Since we’re considering the set-truncated version we want the contexts and substitutions to be h-sets, and so the underlying category of contexts is strict in the HoTT book sense.

Functoriality of \mathrm{Ty} and \mathrm{Tm} means that the equations \sigma [id_{\Gamma}] = \sigma \qquad \sigma [g \circ f] = \sigma [g] [f] t [id_{\Gamma}] = t \qquad t [g \circ f] = t [g] [f] hold for types \sigma and terms t, but note that the equations for terms only typecheck subject to the equations for types. Type theoretically, this means we need to formulate the latter two equations as *dependent* paths over the former two.

(Work in progress)

I might write some code in this note itself at some point; for now the notions mentioned here are formalized in Agda and available at this GitHub repo.