Encoding CwFs in Homotopy Type Theory

18 Nov 2020

Consider the problem of defining models of dependent type theory inside dependent type theory. To be concrete, suppose we want an internal definition of a category with families (CwF). This and similar problems have been considered before in various settings, and in this note we’ll think about encoding CwFs in the setting of book HoTT. Agda code accompanies, using the HoTT-Agda library (on a 2.6.1-compatible fork).

Wildcats and their families

A category with families may be defined succinctly as a category \mathscr{C} of “contexts” and “substitutions” with a terminal object ◆, 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 might write a short note explaining what all these terms mean in the 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. As is usually the case for categorical constructions in HoTT, to make things well behaved we have two options: either set-truncate as needed, or “insert all required coherences”, of which there may be infinitely many. If we were to go the first route and require the contexts and substitutions to be h-sets, the underlying category of contexts would be strict in the HoTT book sense. Going the second route would eventually result in some kind of “∞-CwF”, whatever this might turn out to mean. But for now it’s possible to just ignore the issue and formulate the basic CwF structures on top of so-called wild categories without truncation or coherences. I’ll call such structures wild CwFs.

Functoriality of \mathrm{Ty} and \mathrm{Tm} means that the equations [Eqs. 1] \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, where · [f] denotes substitution along the morphism f. The important thing to note is that the equations for terms only typecheck up to the equations for types. This means that in book HoTT we need to formulate the latter two equations as dependent paths over the former two, and insert the required transports into terms as needed.

With this in mind, and assuming we already have the notion of a category of contexts and substitutions

Con : Type i
Sub : Con  Con  Type i
id  : {Γ : Con}  Sub Γ Γ
: {Γ Δ Ε : Con}  Sub Δ Ε  Sub Γ Δ  Sub Γ Ε
: Con
◆-t : is-terminal ◆

with the usual laws, we can define the type and term structure of a CwF as a record with, among other things, the following fields for types, terms, and substitutions thereupon,

Ty    : Con  Type i
Tm    : {Γ : Con}  Ty Γ  Type i

_[_]  : {Γ Δ : Con}  Ty Δ  Sub Γ Δ  Ty Γ
_[_]ₜ : {Γ Δ : Con} {σ : Ty Δ}  Tm σ  (f : Sub Γ Δ)  Tm (σ [ f ])

equations for substitution as in [Eqs. 1],

[]-id : {Γ : Con} {σ : Ty Γ}  σ [ id ] == σ
[]-◦  : {Γ Δ Ε : Con} {f : Sub Γ Δ} {g : Sub Δ Ε} {σ : Ty Ε}
       σ [ g ◦ f ] == σ [ g ] [ f ]
[]ₜ-id : {Γ : Con} {σ : Ty Γ} {t : Tm σ}  tr Tm []-id (t [ id ]ₜ) == t
[]ₜ-◦  : {Γ Δ Ε : Con} {f : Sub Γ Δ} {g : Sub Δ Ε} {σ} {t : Tm σ}
        tr Tm []-◦ (t [ g ◦ f ]ₜ) == t [ g ]ₜ [ f ]ₜ

and context extension and projections.

(To be continued…)

Related work

Previous work on internal formulations of models of type theory includes

and the paper which introduces CwFs:

The exact settings of these papers vary, in particular with respect to the equality of the theory along two axes: extensional–intensional and homogeneous–heterogeneous. As far as I can see, [Ch08] is intensional but heterogeneous, [KKK18] extensional, [Kr20] intensional homogeneous.

This is a note on work in progress. The concepts mentioned here are formalized in Agda and available on GitHub.