Categorical structures for type theory in univalent foundations

A category with families (à la Fiore) consists of:

1. a category {\mathcal{C}}, together with

2. presheaves \ensuremath{\mathsf{Ty}}, \ensuremath{\mathsf{Tm}} : {\mathcal{C}}^{\mathrm{op}} \to \ensuremath{\ensuremath{\mathsf{Set}}}\xspace;

3. a natural transformation \ensuremath{\mathsf{p}} : \ensuremath{\mathsf{Tm}} \to \ensuremath{\mathsf{Ty}}; and

4. for each object \Gamma : {\mathcal{C}} and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, a representation of the fiber of \ensuremath{\mathsf{p}} over A, i.e.

   1. an object \ensuremath{{\Gamma}.{A}} : {\mathcal{C}} and map \ensuremath{\mathsf{\pi}}_{A} : \ensuremath{{\Gamma}.{A}} \to \Gamma,

   2. an element \ensuremath{\ensuremath{\mathsf{te}}}_A:\ensuremath{\ensuremath{\mathsf{Tm}}({\ensuremath{{\Gamma}.{A}}})}, such that \ensuremath{\mathsf{p}}_{\ensuremath{{\Gamma}.{A}}}(\ensuremath{\ensuremath{\mathsf{te}}}_A) = \ensuremath{\ensuremath{\mathsf{\pi}}_{A}^*{A}} : \ensuremath{\ensuremath{\mathsf{Ty}}({\ensuremath{{\Gamma}.{A}}})},

   3. and such that the induced commutative square

      \begin{xy} \xymatrix{ **[l]\ensuremath{\mathsf{y}}_{}(\ensuremath{{\Gamma}.{A}}) \ar[r]^-{\widehat{\ensuremath{\ensuremath{\mathsf{te}}}_A}} \ar[d]_{\ensuremath{\mathsf{y}}_{}(\ensuremath{\mathsf{\pi}}_{A})} \ar@{}[dr]|<<{\text{\pigpenfont A}} & \ensuremath{\mathsf{Tm}} \ar[d]^{\ensuremath{\mathsf{p}}}\\ **[l]\ensuremath{\mathsf{y}}_{}(\Gamma) \ar[r]_{\widehat{A}}& \ensuremath{\mathsf{Ty}} } \end{xy}

      is a pullback.

      (Here e.g. \widehat{A} denotes the Yoneda transpose of an element of a presheaf.)

By a CwF structure on a category {\mathcal{C}}, we mean the data of items ?–? above.

Let {\mathcal{C}} be a CwF, \Gamma : {\mathcal{C}} an object, and e : A = B an equality of elements of \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}.

We write \Delta_{e} : \ensuremath{{\Gamma}.{A}} \cong \ensuremath{{\Gamma}.{B}} for the induced isomorphism \ensuremath{\mathsf{idtoiso}}\xspace(\ensuremath{\mathsf{ap}_{x\mapsto \ensuremath{{\Gamma}.{x}}}}\xspace(e)).

A type-category consists of:

1. a category {\mathcal{C}}, together with

2. for each object \Gamma : {\mathcal{C}}, a type \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})},

3. for each \Gamma : {\mathcal{C}} and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, an object \ensuremath{{\Gamma}.{A}} : {\mathcal{C}},

4. for each such \Gamma, A, a morphism \ensuremath{\mathsf{\pi}}_{A} : \ensuremath{{\Gamma}.{A}} \to \Gamma,

5. for each map f : \Gamma' \to \Gamma, a ‘reindexing’ function \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})} \to \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma'})}, denoted A \mapsto \ensuremath{f^*{A}},

6. for each \Gamma, A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, and f : \Gamma' \to \Gamma, a morphism \ensuremath{\ensuremath{\mathsf{q}}({f},{A})} : \ensuremath{{\Gamma'}.{\ensuremath{f^*{A}}}} \to \ensuremath{{\Gamma}.{A}},

7. such that for each such \Gamma, A, \Gamma', f, the following square commutes and is a pullback:

   \xymatrix@C=5pc{ \ensuremath{{\Gamma'}.{\ensuremath{f^*{A}}}} \ar[r]^{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}} \ar[d]_{\ensuremath{\mathsf{\pi}}_{\ensuremath{f^*{A}}}} \ar@{}[dr]|<<{\text{\pigpenfont A}} & \ensuremath{{\Gamma}.{A}} \ar[d]^{\ensuremath{\mathsf{\pi}}_{A}} \\ \Gamma' \ar[r]_{f}& \Gamma }

A type-category is split if:

1. for each \Gamma, the type \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})} is a set;

2. for each \Gamma and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, we have equalities

   1. e : \ensuremath{1_{\Gamma}^*{A}} = A, and

   2. \ensuremath{\ensuremath{\mathsf{q}}({1_{\Gamma}},{A})} = \Delta_{e}\ :\ \ensuremath{{\Gamma}.{\ensuremath{1_\Gamma^*{A}}}} \to \ensuremath{{\Gamma}.{A}}; and

3. for f' : \Gamma'' \to \Gamma'), f : \Gamma' \to \Gamma, and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, we have equalities

   1. e' : \ensuremath{(\ensuremath{{f'}\cdot{f}})^*{A}} = \ensuremath{f'^*{\ensuremath{f^*{A}}}}, and

   2. \ensuremath{\ensuremath{\mathsf{q}}({\ensuremath{{f'}\cdot{f}}},{A})} = \ensuremath{{\ensuremath{{\Delta_{e'}}\cdot{\ensuremath{\ensuremath{\mathsf{q}}({f'},{\ensuremath{f^*{A}}})}}}}\cdot{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}}} \ :\ \ensuremath{{\Gamma''}.{\ensuremath{(\ensuremath{{f'}\cdot{f}})^*{A}}}} \to \ensuremath{{\Gamma}.{A}}.

A (split) object extension structure on a category {\mathcal{C}} consists of:

1. a functor \ensuremath{\mathsf{Ty}} : {\mathcal{C}}^{\mathrm{op}} \to \ensuremath{\ensuremath{\mathsf{Set}}}\xspace;

2. for each \Gamma : {\mathcal{C}} and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})},

   1. an object \ensuremath{{\Gamma}.{A}}, and

   2. a projection morphism \ensuremath{\mathsf{\pi}}_{A} : {\mathcal{C}}(\ensuremath{{\Gamma}.{A}}, \Gamma).

In general, one might want to loosen the setness and functoriality conditions on \ensuremath{\mathsf{Ty}}, and hence distinguish the present definition as the split version of a more general notion.

In this paper, however, we do not consider the non-split case, so take object extension structures to mean the split ones throughout.

Let {\mathcal{C}} be a category equipped with an object extension structure X = (\ensuremath{\mathsf{Ty}},\ensuremath{{-}.{-}},\pi).

A (functional) term-structure over X consists of:

1. a presheaf \ensuremath{\mathsf{Tm}} : {\mathcal{C}}^{\mathrm{op}} \to \ensuremath{\ensuremath{\mathsf{Set}}}\xspace, and natural transformation \ensuremath{\mathsf{p}} : \ensuremath{\mathsf{Tm}} \to \ensuremath{\mathsf{Ty}};

2. for each object \Gamma : {\mathcal{C}} and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, an element \ensuremath{\ensuremath{\mathsf{te}}}_A:\ensuremath{\ensuremath{\mathsf{Tm}}({\ensuremath{{\Gamma}.{A}}})}, such that (\ensuremath{{\Gamma}.{A}}, \ensuremath{\mathsf{\pi}}_{A}, \ensuremath{\ensuremath{\mathsf{te}}}_A) form a representation of the fiber of \ensuremath{\mathsf{p}} over A as in item ? of Def. 3.1.

One might say functional to distinguish these from familial term-structures, which would correspond analogously to CwF’s in the sense of Dybjer, with \ensuremath{\ensuremath{\mathsf{Tm}}({\Gamma})} a family indexed by \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}.

For the present paper, however, we work only with the functional ones, so call these simply term-structures.

constr:weq-cwf-regrouped Mathematically, this is essentially trivial, as is visibly evident from the definitions: just a matter of reordering and reassociating \Sigma-types, and distributing \Pi-types over \Sigma-types.

It is perhaps worth noting however that this distributivity requires functional extensionality.

Let {\mathcal{C}} be a category equipped with an object extension structure X = (\ensuremath{\mathsf{Ty}},\ensuremath{{-}.{-}},\pi).

A (split) \ensuremath{\mathsf{q}}-morphism structure over X consists of:

1. for each f : \Gamma' \to \Gamma and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, a map \ensuremath{\ensuremath{\mathsf{q}}({f},{A})} : \ensuremath{{\Gamma'}.{\ensuremath{f^*{A}}}} \to \ensuremath{{\Gamma}.{A}}, such that following square commutes and is a pullback

   \xymatrix@C=5pc{ \ensuremath{{\Gamma'}.{\ensuremath{f^*{A}}}} \ar[r]^{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}} \ar[d]_{\ensuremath{\mathsf{\pi}}_{\ensuremath{f^*{A}}}} \ar@{}[dr]|<<{\text{\pigpenfont A}} & \ensuremath{{\Gamma}.{A}} \ar[d]^{\ensuremath{\mathsf{\pi}}_{A}} \\ \Gamma' \ar[r]_{f}& \Gamma }

   and such that

2. for each \Gamma and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, \ensuremath{\ensuremath{\mathsf{q}}({1_{\Gamma}},{A})} = \Delta_{\ensuremath{1_\Gamma^*{A}},A}\ :\ \ensuremath{{\Gamma}.{\ensuremath{1_\Gamma^*{A}}}} \to \ensuremath{{\Gamma}.{A}}; and

3. for each f' : \Gamma'' \to \Gamma', f : \Gamma' \to \Gamma, and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})},

   \ensuremath{\ensuremath{\mathsf{q}}({\ensuremath{{f'}\cdot{f}}},{A})} = \ensuremath{{\ensuremath{{\Delta_{\ensuremath{(\ensuremath{{f'}\cdot{f}})^*{A}},\ensuremath{f'^*{\ensuremath{f^*{A}}}}}}\cdot{\ensuremath{\ensuremath{\mathsf{q}}({f'},{\ensuremath{f^*{A}}})}}}}\cdot{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}}} \ :\ \ensuremath{{\Gamma''}.{\ensuremath{(\ensuremath{{f'}\cdot{f}})^*{A}}}} \to \ensuremath{{\Gamma}.{A}}.

Here the suppressed equalities on the \Delta_{} terms come from the functoriality axioms of \ensuremath{\mathsf{Ty}}.

constr:weq-typecat-regrouped Much like Construction ?, simply a matter of wrangling \Pi- and \Sigma-types.

Let Y=(\ensuremath{\mathsf{Tm}},\ensuremath{\mathsf{p}},\ensuremath{\ensuremath{\mathsf{te}}}) be a term-structure and Z=(\ensuremath{\mathsf{q}}) a \ensuremath{\mathsf{q}}-morphism structure over X.

Say Y and Z are compatible if for all f : \Gamma \to \Gamma' and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})},

\ensuremath{\ensuremath{\mathsf{te}}}_{\ensuremath{f^*{A}}} = \ensuremath{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}^*{\ensuremath{\ensuremath{\mathsf{te}}}_A}}.

iven Y and f : \Gamma \to \Gamma' and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, the term-structure axioms give a pullback square

So we may take \ensuremath{\ensuremath{\mathsf{q}}({f},{A})} to be the unique map \ensuremath{{\Gamma'}.{\ensuremath{f^*{A}}}} \to \ensuremath{{\Gamma}.{A}} such that \ensuremath{{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}}\cdot{\ensuremath{\mathsf{\pi}}_{A}}} = \ensuremath{{\ensuremath{\mathsf{\pi}}_{\ensuremath{f^*{A}}}}\cdot{f}} and \ensuremath{\ensuremath{\ensuremath{\mathsf{q}}({f},{A})}^*{\ensuremath{\ensuremath{\mathsf{te}}}_A}} = \ensuremath{\ensuremath{\mathsf{te}}}_{\ensuremath{f^*{A}}}.

Verification that this forms a compatible \ensuremath{\mathsf{q}}-morphism structure is essentially routine calculation.

his construction is rather more involved; we only sketch it here, and refer to the formalization for full details.

Briefly, \ensuremath{\ensuremath{\mathsf{Tm}}({\Gamma})} is the set of pairs (A,s), where A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, and s : \Gamma \to \ensuremath{{\Gamma}.{A}} is a section of \ensuremath{\mathsf{\pi}}_{A}.

Its functorial action \ensuremath{f^*{}} involves pulling back sections along the pullback squares given by the \ensuremath{\mathsf{q}}-morphism structure.

Finally, the universal element \ensuremath{\ensuremath{\mathsf{te}}}_A : \ensuremath{\ensuremath{\mathsf{Tm}}({\Gamma})} is the pair (\ensuremath{\ensuremath{\mathsf{\pi}}_{A}^*{A}}, \delta_{\ensuremath{\mathsf{\pi}}_{A}}), where \delta_{\ensuremath{\mathsf{\pi}}_{A}} : \ensuremath{{\Gamma}.{A}} \to \ensuremath{{\ensuremath{{\Gamma}.{A}}}.{\ensuremath{\ensuremath{\mathsf{\pi}}_{A}^*{A}}}} is the diagonal map of the pullback square for A and \ensuremath{\mathsf{\pi}}_{A} given by the \ensuremath{\mathsf{q}}-morphism structure.

construction:weq-term-qmor As intimated above, we proceed by showing that for each term-structure, the compatible \ensuremath{\mathsf{q}}-morphism structure constructed above is in fact the unique compatible such structure, and vice versa.

This equivalence immediately induces an equivalence of pair types, which is the identity on the first component carrying the object extension structure.

Note in particular that for this result—unlike in the constructions above—we rely essentially on the univalence axiom.

y composing the equivalences of Constructions ?, ?, and ?:

Let J : {\mathcal{C}}\to{\mathcal{D}} be a functor, and \ensuremath{\mathsf{p}} : \ensuremath{\mathsf{\tilde{U}}} \to \ensuremath{\mathsf{U}} a morphism of {\mathcal{D}}.

Given an object X of {\mathcal{C}} and morphism f: J(X) \to \ensuremath{\mathsf{U}} in {\mathcal{D}}, a J-pullback of \ensuremath{\mathsf{p}} along f consists of an object X' of {\mathcal{C}} and morphisms p' : X' \to X and Q : J(X') \to \ensuremath{\mathsf{\tilde{U}}}, such that the following square commutes and is a pullback:

Let J : {\mathcal{C}} \to {\mathcal{D}} be a fully faithful functor.

A J-universe structure on a map \ensuremath{\mathsf{p}} : \ensuremath{\mathsf{\tilde{U}}} \to \ensuremath{\mathsf{U}} of {\mathcal{D}} is a function giving, for each object X in {\mathcal{C}} and map f: J(X) \to \ensuremath{\mathsf{U}}, a J-pullback (\ensuremath{{X}.{f}}, \ensuremath{\ensuremath{\mathsf{p}}_{f}}, \ensuremath{\ensuremath{\mathsf{Q}}({X},{f})}) of \ensuremath{\mathsf{p}} along f.

A universe relative to J, or briefly a J-universe, is a map \ensuremath{\mathsf{p}} equipped with a J-universe structure.

A weak universe relative to J is a map \ensuremath{\mathsf{p}} : \ensuremath{\mathsf{\tilde{U}}} \to \ensuremath{\mathsf{U}} such that for all suitable X, f, there exists some J-pullback of \ensuremath{\mathsf{p}} along f.

constr:universe.transfer.concrete Given X in {\mathcal{C}}' and f : J'(X) \to S\ensuremath{\mathsf{U}}, we need to construct a J'-pullback of S(\ensuremath{\mathsf{p}}) along f.

Split essential surjectivity of R gives some \bar{X} : {\mathcal{C}} and isomorphism i : R(\bar{X}) \cong X.

We therefore have \ensuremath{{\alpha_{\bar{X}}}\cdot{\ensuremath{{J'i}\cdot{f}}}} : SJ\bar{X} \to S\ensuremath{\mathsf{U}}; so split fullness of S gives us some \bar{f} : J\bar{X} \to \ensuremath{\mathsf{U}} with S \bar{f} = \ensuremath{{\alpha_{\bar{X}}}\cdot{\ensuremath{{J'i}\cdot{f}}}}.

Taking the given J-pullback of \ensuremath{\mathsf{p}} along \bar{f} and mapping it forward under S, we get a pullback square in {\mathcal{D}}':

The maps \ensuremath{{R(\ensuremath{\ensuremath{\mathsf{p}}_{\bar{f}}})}\cdot{i}} : R(\ensuremath{{\bar{X}}.{\bar{f}}}) \to X and \ensuremath{{\alpha_{\ensuremath{{\bar{X}}.{\bar{f}}}}^{-1}}\cdot{S(\ensuremath{\ensuremath{\mathsf{Q}}({\bar{X}},{\bar{f}})})}} : J'R(\ensuremath{{\bar{X}}.{\bar{f}}}) \to S \ensuremath{\mathsf{\tilde{U}}} now give the desired J'-pullback of S\ensuremath{\mathsf{p}} along f, since the square they give—the right-hand square below—is isomorphic to the pullback obtained above.

constr:universe.struct.on Mostly the same as Construction ?.

The only problematic steps are finding (\bar{X},i) and \bar{f} as above, since the hypotheses which provided them there have now been weakened to existence properties.

However, our new hypotheses that {\mathcal{C}}' is univalent and J' fully faithful allow us to apply Lemma 4.3 to see that the goal of a J'-pullback is a proposition; so the existence properties do in fact suffice.

constr:weq.wkrelu.transfer The equivalence S of univalent categories induces an equivalence between morphisms in {\mathcal{D}} and in {\mathcal{D}}'.

Lemma 4.10 implies that this restricts to an equivalence between weak relative universes as desired.

A map \ensuremath{\mathsf{p}} : \ensuremath{\mathsf{Tm}} \to \ensuremath{\mathsf{Ty}} of presheaves on a category {\mathcal{C}} is representable if for each for each \Gamma : {\mathcal{C}} and A : \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, there exists some representation of the fiber of \ensuremath{\mathsf{p}} over A, i.e. some \ensuremath{\mathsf{\pi}}_{A} : \ensuremath{{\Gamma}.{A}} \to \Gamma and \ensuremath{\ensuremath{\mathsf{te}}}_A \in \ensuremath{\ensuremath{\mathsf{Tm}}({\ensuremath{{\Gamma}.{A}}})} satisfying the conditions of Definition 3.1, item ?.

(Note that in [awodey_natural_published], Awodey takes representable map to mean what we call a CwF structure, i.e. to include choices of representations of the fibers; cf. [awodey_natural_published, 1.1, Algebraic character].)

In other words, a representable map of presheaves on {\mathcal{C}} is just like a CwF structure, except that the representations are merely assumed to exist, not included as chosen data.

construction:equiv_cwf_relu This is a matter of reassociating components, and replacing two quantifications over elements of a presheaf—once over \ensuremath{\ensuremath{\mathsf{Ty}}({\Gamma})}, once over \ensuremath{\ensuremath{\mathsf{Tm}}({\ensuremath{{\Gamma}.{A}}})}—by quantification over the respective isomorphic sets of natural transformations into \ensuremath{\mathsf{Ty}} and \ensuremath{\mathsf{Tm}}.

construction:equiv_rep_relwku Similar to Construction ?.

construction:transfer_cwf We construct a map \ensuremath{\mathsf{relu}}(\ensuremath{\mathsf{y}}_{{\mathcal{C}}}) \to \ensuremath{\mathsf{relu}}(\ensuremath{\mathsf{y}}_{{\mathcal{D}}}) as an instance of Construction ? and obtain the desired map by composition with the equivalence to CwF structures of Construction ?. Consider the diagram

Here, the functor F^{\circ} given by precomposition with F^{\mathrm{op}} is a weak equivalence between univalent categories, and hence a strong equivalence with inverse \mathcal{S}. The isomorphism \alpha is constructed as follows: Note that fully faithful functors reflect isomorphisms; we apply this for the functor F^{\circ} of precomposition with F^{\mathrm{op}}. It hence suffices to construct a natural isomorphism from \ensuremath{{\ensuremath{\mathsf{y}}_{{\mathcal{C}}}}\cdot{\ensuremath{{\mathcal{S}}\cdot{F^{\circ}}}}} \simeq \ensuremath{\mathsf{y}}_{{\mathcal{C}}} to \ensuremath{{F}\cdot{\ensuremath{{\ensuremath{\mathsf{y}}_{{\mathcal{D}}}}\cdot{F^{\circ}}}}}. But this is an instance of a general isomorphism: indeed, for any functor G : {\mathcal{A}} \to {\mathcal{X}}, we have natural transformation from \ensuremath{\mathsf{y}}_{{\mathcal{A}}} to \ensuremath{{G}\cdot{\ensuremath{{\ensuremath{\mathsf{y}}_{{\mathcal{X}}}}\cdot{G^{\circ}}}}}, and this natural transformation is an isomorphism when G is fully faithful. This ends the construction of the natural isomorphism \alpha. The functor \mathcal{S} preserves pullbacks since it is fully faithful and essentially surjective. The hypotheses of Problem 4.7 are easily checked, hence Construction ? applies.

construction:transfer_rep A direct instance of Construction ?.

onstruction ?, applied to \eta_{{\mathcal{C}}}, gives us an equivalence \ensuremath{\mathsf{rep}}({\mathcal{C}}) \simeq \ensuremath{\mathsf{rep}}(\ensuremath{\ensuremath{\mathsf{RC}}({{\mathcal{C}}})}).

On the other hand, Lemma 5.2 tells us that \ensuremath{\mathsf{cwf}}(\ensuremath{\ensuremath{\mathsf{RC}}({{\mathcal{C}}})}) \simeq \ensuremath{\mathsf{rep}}(\ensuremath{\ensuremath{\mathsf{RC}}({{\mathcal{C}}})}).

Composing the first of these with the inverse of the second yields the desired equivalence.