Encoding CwFs in homotopy type theory

16 Oct 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

__  : (Γ : Con) (σ : Ty Γ)  Con
p    :  {Γ} {σ : Ty Γ}  Sub (Γ ∷ σ) Γ
ν    :  {Γ} {σ : Ty Γ}  Tm (σ [ p ])
_,,_ :  {Γ Δ} {σ : Ty Γ} (f : Sub Δ Γ) (t : Tm (σ [ f ]))  Sub Δ (Γ ∷ σ)

together with beta and eta rules expressing the universal property they satisfy.

We can then define the usual operations on dependent terms like substitution of variables by terms etc.

Additional structure

The bare notion of a CwF can be extended with constructions interpreting Π and Σ types. Alongside the type formers, constructors and eliminators, we also need equations saying how substitution behaves. For instance, the rule \Pi(A, B)[t/x] = \Pi(A[t/x], B[t/x]) for \Gamma; x \vdash A and \Gamma; x; y \colon A \vdash B is an instance of the general rule on substitutions \Pi(A, B)[f] = \Pi(A[f], B[\hat{f}]), where \hat{f} is the weakening of the substitution f by y \colon A. The substitution rule for lambdas is similar.

Formulating the Σ-type former, constructor (pair) and eliminators (first and second projections) is straightforward enough. However when we try to write down the equation for substitution in pairs we have to transport along an equality expressing the condition that weakening and explicit term substitution commute. This turns out to be essentially the universal property of comprehensions, which is provable from the beta and eta rules mentioned earlier but quite involved in our setting due to all the transports involved.

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.

Updated 23 Dec 2020. This is a note on work in progress. The concepts mentioned here and more are formalized in Agda and available on GitHub.