Identity types and weak factorization systems in Cauchy complete categories

TL;DR

This paper characterizes when a weak factorization system in a Cauchy complete category can interpret dependent type theory with Sigma- and Id-types, reducing the problem to a specific display map category.

Contribution

It provides a necessary and sufficient condition for a weak factorization system to support dependent type theory interpretations in Cauchy complete categories.

Findings

Characterizes when (C, R) forms a display map category for Sigma- and Id-types

Reduces the search for suitable classes D to a unique candidate

Establishes a criterion linking weak factorization systems and type-theoretic models

Abstract

It has been known that categorical interpretations of dependent type theory with Sigma- and Id-types induce weak factorization systems. When one has a weak factorization system (L, R) on a category C in hand, it is then natural to ask whether or not (L, R) harbors an interpretation of dependent type theory with Sigma- and Id- (and possibly Pi-) types. Using the framework of display map categories to phrase this question more precisely, one would ask whether or not there exists a class D of morphisms of C such that the retract closure of D is the class R and the pair (C, D) forms a display map category modeling Sigma- and Id- (and possibly Pi-) types. In this paper, we show, with the hypothesis that C is Cauchy complete, that there exists such a class D if and only if (C,R) itself forms a display map category modeling Sigma- and Id- (and possibly Pi-) types. Thus, we reduce the search space of our original question from a potentially proper class to a singleton.

Equations

$$\mathbb{C}/Y(y,{\Pi }_{f}g)\cong \mathbb{C}/X(f^{\ast }y,g)$$

$$X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\alpha }^{\ast }\mathtt{Id}(f)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\frac{\text{vbox}\Gamma ⊢a,b:A\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢{\mathtt{Id}}_A(a,b)}$$

$$\frac{\text{vbox}\Gamma ,x:T,\Theta ⊢a,b:A\Gamma ,\Delta ⊢t:T\text{vbox}}{\text{vbox}\text{vbox}\Gamma ,\Delta ,\Theta [t/x]⊢{\mathtt{Id}}_A(a,b)[t/x]={\mathtt{Id}}_{A[t/x]}(a[t/x],b[t/x])}$$

$$\frac{\text{vbox}\Gamma ,x:T,\Theta ⊢a:A\Gamma ,\Delta ⊢t:T\text{vbox}}{\text{vbox}\text{vbox}\Gamma ,\Delta ,\Theta [t/x]⊢r_a[t/x]=r_{a[t/x]}:{\mathtt{Id}}_A(a,b)[t/x]}$$

$$\frac{\text{vbox}\Gamma ,a,b:A,p:{\mathtt{Id}}_A(a,b)⊢E(a,b,p)\Gamma ,a:A⊢e(a):E(a,a,r_a)\text{vbox}}{\text{vbox}\text{vbox}\Gamma ,a,b:A,p:{\mathtt{Id}}_A(a,b)⊢j(e,a,b,p):E(a,b,p)\Gamma ,a:A⊢e(a)=j(e,a,a,r_a):E(a,a,r_a)}$$

$$\frac{\text{vbox}\Gamma ,a,b:A,p:{\mathtt{Id}}_A(a,b),\Theta (a,b,p)⊢E(a,b,p)\Gamma ,a:A,\Theta (a,a,r_a)⊢e(a):E(a,a,r_a)\text{vbox}}{\text{vbox}\text{vbox}\text{vbox}\Gamma ,a,b:A,p:{\mathtt{Id}}_A(a,b),\Theta (a,b,p)⊢j(e,a,b,p):E(a,b,p)\Gamma ,a:A,\Theta (a,a,r_a)⊢e(a)=j(e,a,a,r_a):E(a,a,r_a)}$$

$$\frac{\text{vbox}\Gamma ⊢a:A\Gamma ,b:A,p:{\mathtt{Id}}_A(a,b)⊢E(b,p)\Gamma ⊢e:E(a,r_a)\text{vbox}}{\text{vbox}\text{vbox}\Gamma ,b:A,p:{\mathtt{Id}}_A(a,b)⊢j(e,b,p):E(b,p)\Gamma ⊢e=j(e,a,r_a):E(a,r_a)}$$

$$\frac{\text{vbox}\Gamma ⊢a:A\Gamma ,b:A,p:{\mathtt{Id}}_A(b,a)⊢E(b,p)\Gamma ⊢e:E(a,r_a)\text{vbox}}{\text{vbox}\text{vbox}\Gamma ,b:A,p:{\mathtt{Id}}_A(b,a)⊢j(e,b,p):E(b,p)\Gamma ⊢e=j(e,a,r_a):E(a,r_a)}$$

$$\frac{\text{vbox}\Gamma ⊢a:A\Gamma ,b:A,p:{\mathtt{Id}}_A(a,b),\Theta (b,p)⊢E(b,p)\Gamma ,\Theta (a,r_a)⊢e:E(a,r_a)\text{vbox}}{\text{vbox}\text{vbox}\Gamma ,b:A,p:{\mathtt{Id}}_A(a,b),\Theta (b,p)⊢j(e,b,p):E(b,p)\Gamma ,\Theta (a,r_a)⊢e=j(e,a,r_a):E(a,r_a)}$$

$$A\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\sigma }^{\ast }\mathtt{Id}(d)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$Y\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$X\stackrel{1\times r_{Y}f}{\to }X{\times }_Y\mathtt{Id}(Y)\stackrel{{\pi }_1{ϵ}_Y}{\to }Y$$

$$X{\times }_Y\mathtt{Id}(Y)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\lambda (f):=1\times r_{Y}f:X\to X{\times }_Y\mathtt{Id}(Y)$$

$$f^{\ast }\mathtt{Id}(Y)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\rho (f):={\pi }_1{ϵ}_Y:X{\times }_Y\mathtt{Id}(Y)\to Y$$

$$X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.53471pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&\crcr}}}\ignorespaces{\hbox{\kern-7.53471pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 20.98082pt\raise-25.31943pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 51.78944pt\raise-33.8412pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 15.68053pt\raise-6.5pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\lambda(f)}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.53471pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.53471pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\times_{Y}\mathtt{Id}(Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 93.43132pt\raise-4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{s}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 110.07195pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 58.80333pt\raise-19.20833pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\rho(f)}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 58.80333pt\raise-28.58334pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 110.07195pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 86.43533pt\raise-25.31943pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 65.81723pt\raise-33.83434pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-3.0pt\raise-38.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 51.78944pt\raise-38.41666pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{Y}$}}}}}}}\ignorespaces\ignorespaces}}}}}\qed$$

$$R\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$C\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$R\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$e\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$d\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$e\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$a\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

Full text

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-16-1-0212.

1. 1 Introduction

2. 2 Display map categories and quantifiers

3. 3 Identity types in display map categories

4. 3.1 Comparison with other identity types

5. 4 Weak factorization systems from display map categories

6. 5 Cauchy complete categories

7. 5.1 Preliminaries

8. 5.2 Display map categories

9. 5.3 $\Sigma$-types

10. 5.4 $\mathtt{Id}$-types

11. 5.5 $\Pi$-types

12. 5.6 Summary

13. 6 Display map categories reflected in weak factorization systems

14. 7 Outlook

1. Introduction

In this paper, we study categorical interpretations of dependent type theory [NPS00]. It has long been known that dependent type theory with $\Sigma$- and $\mathtt{Id}$-types can be interpreted in certain weak factorization systems [War08, AW09] and that such interpretations induce weak factorization systems [GG08]. Thus, a search for such interpretations could comprise two steps: first, identify a weak factorization system $(\mathcal{L},\mathcal{R})$ on a category $\mathbb{C}$, and second, decide if $(\mathcal{L},\mathcal{R})$ harbors an interpretation of dependent type theory with $\Sigma$- and $\mathtt{Id}$-types. Since we are interested in the connection between dependent type theory and familiar weak factorization systems of homotopy theory, we are interested primarily in the second step.

The present paper is the first in a series of papers which develop a theorem for recognizing whether a given weak factorization system $(\mathcal{L},\mathcal{R})$ harbors a model of dependent type theory with $\Sigma$- and $\mathtt{Id}$- (and possibly $\Pi$-) types. The content of this series can already be found in the author’s thesis [Nor17]. This paper is a streamlined account of the second chapter of [Nor17].

In this and following papers, we choose display map categories from the various categorical frameworks which can interpret dependent type theory. This is because the data of a display map category, which consists of a category $\mathbb{C}$ and a class of maps of $\mathbb{C}$, is directly comparable to the data underlying a weak factorization system, which consists of a category $\mathbb{C}$ and two classes of maps of $\mathbb{C}$ (each of which determine the other).

Not only do we choose the simplest categorical framework for interpreting dependent type theory, but we have also chosen the simplest variant of weak factorization system (compared to, for example, algebraic weak factorization systems). We make these choices in order to reveal the most fundamental connection between these two notions.

In this paper, we study display map categories $(\mathbb{C},\mathcal{D})$ which model $\Sigma$- and $\mathtt{Id}$- (and possibly $\Pi$-) types. As mentioned above, such a structure generates a weak factorization system $(^{\boxslash}\mathcal{D},\overline{\mathcal{D}})$ on the category $\mathbb{C}$ where $\overline{\mathcal{D}}$ is the retract closure of $\mathcal{D}$. In this framework, for any weak factorization system $(\mathcal{L},\mathcal{R})$ on a category $\mathbb{C}$, our original question,

Question 1.1**.**

Does $(\mathcal{L},\mathcal{R})$ harbor an interpretation of dependent type theory with $\Sigma$- and $\mathtt{Id}$- (and possibly $\Pi$-) types?

can be phrased more precisely as the following question.

Question 1.2**.**

Does there exist a subclass $\mathcal{D}\subseteq\mathcal{R}$ such that $\mathcal{R}$ is the retract closure of $\mathcal{D}$ and $(\mathbb{C},\mathcal{D})$ is a display map category which models $\Sigma$- and $\mathtt{Id}$- (and possibly $\Pi$-) types?

The original contribution of this paper is the following theorem.

Theorem 5.12.

Consider a Cauchy complete category $\mathbb{C}$ and a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and functorial $\mathtt{Id}$-types. Then $(\mathbb{C},\overline{\mathcal{D}})$ is again a display map category modeling $\Sigma$- and functorial $\mathtt{Id}$-types. If $(\mathbb{C},\mathcal{D})$ also models $\Pi$-types, then $(\mathbb{C},\overline{\mathcal{D}})$ also models $\Pi$-types.

With this theorem, Question 1.2 is equivalent to the following question.

Question 1.3**.**

Is $(\mathbb{C},\mathcal{R})$ a display map category with $\Sigma$- and $\mathtt{Id}$- (and possibly $\Pi$-) types?

Thus, to decide whether or not $(\mathcal{L},\mathcal{R})$ harbors an interpretation, we do not have to analyze the pair $(\mathbb{C},\mathcal{D})$ for all classes $\mathcal{D}$ whose retract closure is $\mathcal{R}$, which likely constitute a proper class. Rather, we only need to analyze the one pair $(\mathbb{C},\mathcal{R})$. Indeed, this will be the subject of the next paper of this series.

2. Display map categories and quantifiers

In this section, we fix definitions of display map categories and of $\Sigma$- and $\Pi$-types in display map categories.

Definition 2.1**.**

A display map category $(\mathbb{C},\mathcal{D})$ consists of a category $\mathbb{C}$ with a terminal object and a class $\mathcal{D}$ of morphisms of $\mathbb{C}$ such that:

1. (1)

$\mathcal{D}$ contains every isomorphism; 2. (2)

$\mathcal{D}$ contains every morphism whose codomain is a terminal object; 3. (3)

every pullback of every morphism of $\mathcal{D}$ exists; and 4. (4)

$\mathcal{D}$ is stable under pullback.

We call the elements of $\mathcal{D}$ display maps.

In such a display map category, the objects of $\mathbb{C}$ are meant to represent contexts, and the morphisms of $\mathbb{C}$ represent context morphisms. A morphism $p:E\to B$ of $\mathcal{D}$ represents a type family $E$ dependent on $B$. The empty context is represented by the terminal object of $\mathbb{C}$, so condition (2) says that every object of $\mathbb{C}$ may also be viewed as a type dependent on the empty context. The pullback of a morphism $p$ of $\mathcal{D}$ along a morphism $f$ of $\mathbb{C}$ represents the substitution of $f$ into the type family $p$.

Definition 2.2**.**

A display map category $(\mathbb{C},\mathcal{D})$ models $\Sigma$-types if $\mathcal{D}$ is closed under composition. We call a composition $gf$ of display maps a $\Sigma$-type and sometimes denote it by $\Sigma_{g}f$.

Definition 2.3**.**

A display map category $(\mathbb{C},\mathcal{D})$ models $\Pi$-types if for every pair of composable display maps $g:W\to X$ and $f:X\to Y$, there exists a display map $\Pi_{f}g$ with codomain $Y$ and the universal property

[TABLE]

natural in $y$. The term $\Pi$-type will refer to such a display map $\Pi_{f}g$.

Remark 2.4*.*

The definitions in this section are relatively standard in the literature. A display map category which models $\Sigma$-types coincides with Joyal’s notion of clan, and a display map category which models $\Sigma$- and $\Pi$-types coincides with his notion of $\pi$-clan [Joy17]. A class $\mathcal{D}$ of displays in $\mathbb{C}$, in the sense of Taylor [Tay99], where all identities and morphisms to the terminal object are in $\mathcal{D}$ is a display map category $(\mathbb{C},\mathcal{D})$. His strong sums and dependent products coincide with our $\Sigma$-types and $\Pi$-types. Criteria (1)-(4) of Shulman’s definition of type-theoretic fibration category constitute a display map category with $\Sigma$- and $\Pi$-types [Shu15].

3. Identity types in display map categories

Now we define $\mathtt{Id}$-types in a display map category. This definition is more convoluted and less standard than the definitions of $\Sigma$- and $\Pi$-types, but in Section 3.1 below, we justify this choice of definition by comparing it with others.

First we fix some notation.

Notation 3.1**.**

For a class $\mathcal{M}$ of morphisms of a category $\mathbb{C}$, let ${}^{\boxslash}\mathcal{M}$ denote the class of morphisms of $\mathbb{C}$ which have the left lifting property against $\mathcal{M}$. Similarly, let $\mathcal{M}^{\boxslash}$ denote the class of morphisms of $\mathbb{C}$ which have the right lifting property against $\mathcal{M}$.

Definition 3.2**.**

Consider a display map category ($\mathbb{C},\mathcal{D}$) which models $\Sigma$-types. We say that it models $\mathtt{Id}$-types if for every $f:X\to Y$ in $\mathcal{D}$,

1. (1)

the diagonal $\Delta_{f}:f\to f\times f$ in the slice $\mathbb{C}/Y$ has a factorization $\Delta_{f}=\epsilon_{f}r_{f}$ in $\mathbb{C}/Y$

[TABLE]

such that

1. (2)

$\epsilon_{f}$ is in $\mathcal{D}$ and 2. (3)

for every morphism $\alpha:A\to X$ in $\mathbb{C}$, the pullback $\alpha^{*}r_{f}$, as shown below, is in ${}^{\boxslash}\mathcal{D}$ for $i=0,1$.

[TABLE]

We will call the morphism $\iota_{f}:\mathtt{Id}(f)\to Y$ in Diagram (3.1) the $\mathtt{Id}$-type of $f$ in $\mathbb{C}/Y$.

Note that since $(\mathbb{C},\mathcal{D})$ models $\Sigma$-types in this definition, $\mathcal{D}$ is closed under composition and stable under pullback. Thus, for any $f\in\mathcal{D}$, $f\times f$ is in $\mathcal{D}$ as it is the composition of a pullback of $f$ with $f$, and $\iota_{f}$ is in $\mathcal{D}$ since it is the composition of $\epsilon_{f}$ and $f\times f$.

Definition 3.3**.**

Consider a display map category ($\mathbb{C},\mathcal{D}$) which models $\Sigma$-types and $\mathtt{Id}$-types. For any object $Y$, let $\mathcal{D}/Y$ denote the full subcategory of the slice category $\mathbb{C}/Y$ spanned by those objects which are display maps. Let $\mathcal{F}$ denote the category $\bullet\to\bullet\to\bullet$ so that $(\mathcal{D}/Y)^{\mathcal{F}}$ is the category of composable pairs of morphisms of $\mathcal{D}/Y$.

We say that $(\mathbb{C},\mathcal{D})$ functorially models $\mathtt{Id}$-types if for each object $Y$ of $\mathbb{C}$, there is a functor $\mathcal{D}/Y\to(\mathcal{D}/Y)^{\mathcal{F}}$ which provides the factorization required by part (1) of Definition 3.2 above.

3.1. Comparison with other identity types

Our definition of identity types is not completely standard, so we pause here to compare it to others in the literature. The unconcerned reader can safely skip this section.

The identity types given above correspond to one of several ways in which identity types may be defined in the syntax of dependent type theory. All the variants that we will discuss here start with the standard formation and introduction rules.

[TABLE]

These must respect substitution: that is, we have the following meta-theoretic rules which Warren [War08] calls coherence rules.

[TABLE]

[TABLE]

Then the elimination and computation rules may be given in one of several ways:

1. (1)

The (non-parametrized) elimination and computation rules à la Martin-Löf

[TABLE]

together with the appropriate coherence rule.

In the absence of $\Pi$-types, these rules are not strong enough to prove many important properties of the identity type. The following two variants of the elimination and computation rules build some of the flexibility that $\Pi$-types provide directly into the identity types:

1. (2)

The parametrized elimination and computation rules à la Martin-Löf

[TABLE]

together with the appropriate coherence rule; 2. (3)

The elimination and computation rules à la Paulin-Mohring

[TABLE]

[TABLE]

together with the appropriate coherence rule.

Remark 3.4*.*

One might also consider parametrized elimination and computation rules à la Paulin-Mohring, by combining the variants (2) and (3).

[TABLE]

However, we do not find it necessary to consider such strong $\mathtt{Id}$-types.

In the presence of $\Pi$-types, these three variants (1)-(3) of the rules are all equivalent. The fact that (1) is equivalent to (3) was first shown by Martin Hofmann, and can be found in [Str93, Addendum, pp. 142-143]. We show below in Proposition 3.6 that the two strengthened variants, (2) and (3), are equivalent in the absence of $\Pi$-types at least in our categorical interpretation with the hypothesis that ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$.

Now, we define interpretations of these three variants of the identity type in a display map category. Note that we only model the coherence rules weakly, in the sense of [LW15].

Definition 3.5**.**

Consider a category with display maps $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types. It models the formation and introduction rule of $\mathtt{Id}$-types if for every $d:A\to\Gamma$ in $\mathcal{D}$, the diagonal $\Delta_{d}:d\to d\times d$ has a factorization $\Delta_{d}=\epsilon_{d}r_{d}$ in the slice $\mathbb{C}/\Gamma$ such that $\epsilon_{d}$ is in $\mathcal{D}$.

[TABLE]

If $(\mathbb{C},\mathcal{D})$ models the formation and introduction rules of $\mathtt{Id}$-types and if for every display map $d:A\to\Gamma$ and every morphism $\sigma:\Delta\to\Gamma$, the pullback of $\sigma^{*}r_{d}$ (illustrated in the following diagram) is in ${}^{\boxslash}\mathcal{D}$, we say that $(\mathbb{C},\mathcal{D})$ models Martin-Löf $\mathtt{Id}$-types.

[TABLE]

If $(\mathbb{C},\mathcal{D})$ models Martin-Löf $\mathtt{Id}$-types and if for every display map $d:A\to\Gamma$, every morphism $\alpha:\Delta\to\Gamma$, and every display map $\theta:\Theta\to\sigma^{*}\mathtt{Id}(d)$, we have that $\theta^{*}(\sigma^{*}r_{d})$ is in ${}^{\boxslash}\mathcal{D}$, then we say that $(\mathbb{C},\mathcal{D})$ models parametrized Martin-Löf $\mathtt{Id}$-types.

Now suppose that $(\mathbb{C},\mathcal{D})$ models the formation and introduction rule of $\mathtt{Id}$-types. Suppose also that for all display maps $d:A\to\Gamma$, objects $\Delta$ of $\mathbb{C}$, morphisms $\sigma:\Delta\to A$, and $i\in\{0,1\}$, the pullback $\sigma^{*}r_{d}$ of $r_{d}$ shown below is in ${}^{\boxslash}\mathcal{D}$. Then we say that $(\mathbb{C},\mathcal{D})$ models Paulin-Mohring $\mathtt{Id}$-types.

[TABLE]

The parametrized Martin-Löf $\mathtt{Id}$-types correspond to the strong $\mathtt{Id}$-types of [vdBG12]. The Paulin-Mohring $\mathtt{Id}$-types are what we just call identity types in Definition 3.2 and in the rest of this paper.

Proposition 3.6**.**

Consider a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and the formation and introduction rules of $\mathtt{Id}$-types. Then

1. (1)

if $(\mathbb{C},\mathcal{D})$ models parametrized Martin-Löf $\mathtt{Id}$-types, it models Paulin-Mohring $\mathtt{Id}$-types, and 2. (2)

if $(\mathbb{C},\mathcal{D})$ models Paulin-Mohring $\mathtt{Id}$-types and ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$, then it models parametrized Martin-Löf $\mathtt{Id}$-types.

Proof.

Suppose that $(\mathbb{C},\mathcal{D})$ models parametrized Martin-Löf $\mathtt{Id}$-types. We need to verify that the map $\sigma^{*}r_{d}$ in Diagram (3.3) is in ${}^{\boxslash}\mathcal{D}$. This follows from Lemma 2.4 of [Shu15]. That $(\mathbb{C},\mathcal{D})$ models Martin-Löf $\mathtt{Id}$-types corresponds to Shulman’s conditions ($5^{\prime}$) and ($6^{\prime}$) which he shows entail condition (6). Then, the fact that $\sigma^{*}r_{d}$ is in ${}^{\boxslash}\mathcal{D}$ is an instance of (6). Note that Shulman’s stated hypotheses are stronger than ours, though ours suffice to prove this result. In particular, he assumes that ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$, but our weaker hypothesis that the $\mathtt{Id}$-types are parametrized can be used instead.

Now suppose that $(\mathbb{C},\mathcal{D})$ models Paulin-Mohring $\mathtt{Id}$-types and ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$. Consider a morphism $\theta^{*}(\sigma^{*}r_{d})$ as in the definition (3.5) of parametrized Martin-Löf $\mathtt{Id}$-types. Since $\theta\in\mathcal{D}$ and $\sigma^{*}r_{d}\in{{}^{\boxslash}\mathcal{D}}$, we have that $\theta^{*}(\sigma^{*}r_{d})\in{{}^{\boxslash}\mathcal{D}}$. ∎

Thus, modulo the hypothesis that ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$, the conditions that a display map category $(\mathbb{C},\mathcal{D})$ model parametrized Martin-Löf $\mathtt{Id}$-types and that it model Paulin-Mohring $\mathtt{Id}$-types are equivalent. In the next paper of this series, we will show that if a display map category $(\mathbb{C},\mathcal{D})$ models $\Sigma$-types and the formation and introduction rules of $\mathtt{Id}$-types, then it models Paulin-Mohring $\mathtt{Id}$-types if and only if ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$ (which already appears as Theorem 3.5.2 of [Nor17]). Thus this hypothesis that ${}^{\boxslash}\mathcal{D}$ is stable under pullback along $\mathcal{D}$ is not necessary, but this is not the focus of the present paper.

The conditions (1), (2), (5), (6) of Shulman’s type-theoretic fibration categories [Shu15, Def. 2.1] constitute a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and Paulin-Mohring $\mathtt{Id}$-types. A tribe in the sense of Joyal [Joy17] is a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and Paulin-Mohring $\mathtt{Id}$-types, given this equivalence between Paulin-Mohring $\mathtt{Id}$-types and the stability of ${}^{\boxslash}\mathcal{D}$ under pullback along $\mathcal{D}$.

In summary, the $\mathtt{Id}$-types that we consider, the Paulin-Mohring $\mathtt{Id}$-types, are comparable to other categorical $\mathtt{Id}$-types that have appeared in the literature, and they are an appropriate version to study in the absence of $\Pi$-types. In what follows, we will return to calling Paulin-Mohring $\mathtt{Id}$-types just $\mathtt{Id}$-types.

4. Weak factorization systems from display map categories

In this section, we recall how any display map category $(\mathbb{C},\mathcal{D})$ with $\Sigma$-types and $\mathtt{Id}$-types generates a weak factorization system $({{}^{\boxslash}\mathcal{D}},\overline{\mathcal{D}})$ with a factorization $(\lambda,\rho)$ where $\overline{\mathcal{D}}$ is the retract closure of $\mathcal{D}$ and the image of $\rho$ lies in $\mathcal{D}$. This will give us a good enough handle on the relationship between $\mathcal{D}$ and $\overline{\mathcal{D}}$ to prove our main theorem in the following section, where we extend an interpretation of type theory in $(\mathbb{C},\mathcal{D})$ to one in $(\mathbb{C},\overline{\mathcal{D}})$.

In the following proposition, we construct this weak factorization system. The proof uses ideas from the proof of Theorem 10 of [GG08], where a weak factorization system is constructed in the syntactic category of a dependent type theory. A categorical version appears as Theorem 2.8 in [Emm14].

Notation 4.1**.**

Let $\overline{\mathcal{D}}$ denote $(^{\boxslash}\mathcal{D})^{\boxslash}$.

Proposition 4.2** ([Emm14, Thm. 2.8]).**

Consider a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and $\mathtt{Id}$-types. There exists a weak factorization system $({{}^{\boxslash}\mathcal{D}},\overline{\mathcal{D}})$ in $\mathbb{C}$ with a factorization $(\lambda,\rho)$ where the image of $\rho$ is contained in $\mathcal{D}$. Furthermore, if the $\mathtt{Id}$-types are functorial, then this weak factorization system is functorial.

Proof.

We just describe here the factorization since it will be used later. The full proof of this statement can be found in [Emm14].

The factorization is defined in the following way for any $f:X\to Y$ in $\mathbb{C}$. We have a factorization

[TABLE]

of the diagonal $\Delta:Y\to Y\times Y$. Now we define the factorization of $f$ to be

[TABLE]

where the middle object is obtained in the following pullback.

[TABLE]

The left factor

[TABLE]

is obtained as the following pullback of $r_{Y}$.

[TABLE]

Thus, it is in ${}^{\boxslash}\mathcal{D}$.

The right factor

[TABLE]

is in $\mathcal{D}$ because it is the composition of a pullback of $\epsilon_{Y}$ with a pullback of $X\to*$. ∎

The class $\overline{\mathcal{D}}$, which was defined to be $(^{\boxslash}\mathcal{D})^{\boxslash}$ in Notation 4.1, is the retract closure of $\mathcal{D}$, justifying its notation.

Lemma 4.3** ([MP12, Prop. 14.1.8]).**

Consider a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and $\mathtt{Id}$-types. The class $\overline{\mathcal{D}}$ contains all isomorphisms, is closed under composition and retracts, and is stable under pullback.

Proposition 4.4**.**

Consider a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and $\mathtt{Id}$-types. The class $\overline{\mathcal{D}}$ is the retract-closure (in $\mathbb{C}^{\mathbb{2}}$, the category of morphisms of $\mathbb{C}$) of $\mathcal{D}$. Moreover, every morphism $f:X\to Y$ of $\overline{\mathcal{D}}$ is a retract in $\mathbb{C}/Y$ of the display map $\rho(f)$ defined in Proposition 4.2.

Proof.

That $\overline{\mathcal{D}}$ is the retract closure of $\mathcal{D}$ follows from Lemma 4.3.

Consider any morphism $f:X\to Y$ of $\overline{\mathcal{D}}$. That $f$ is a retract of $\rho(f)$ follows from Lemma 1.1.9 of [Hov99], the argument of which we recount here. Consider the following lifting problem.

[TABLE]

It has a solution $s:X\times_{Y}\mathtt{Id}(Y)\to X$ since $\lambda(f)\in{{}^{\boxslash}\mathcal{D}}$ and $f\in(^{\boxslash}\mathcal{D})^{\boxslash}$. Then we can rearrange the lifting problem diagram into the following commutative diagram where $f$ appears as a retract of $\rho(f)$ in $\mathbb{C}/Y$.

[TABLE]

5. Cauchy complete categories

In this section, we prove our main theorem: if a category $\mathbb{C}$ is Cauchy complete and $(\mathbb{C},\mathcal{D})$ is a display map category which models $\Sigma$-types and $\mathtt{Id}$-types, then $(\mathbb{C},\overline{\mathcal{D}})$ is also a display map category which models $\Sigma$-types and $\mathtt{Id}$-types. Moreover, if $(\mathbb{C},\mathcal{D})$ also models $\Pi$-types, then $(\mathbb{C},\overline{\mathcal{D}})$ models $\Pi$-types as well.

The proofs in this section use the following idea. We need to prove that a certain functor, built out of elements of $\overline{\mathcal{D}}$, is representable while we hypothesize that the same functor, if built only out of elements of $\mathcal{D}$, is representable. In a Cauchy complete category, retracts of representable functors are themselves representable (Lemma 5.7). Thus, using the fact that every element of $\overline{\mathcal{D}}$ is a retract of an element of $\mathcal{D}$, we aim to show that those functors we want to be representable are retracts of functors we know to be representable.

5.1. Preliminaries

In this section, we recall the basic definitions and results that are necessary for our narrative.

Definition 5.1** ([Bor94, Def. 6.5.1,3,8]).**

A morphism $e:C\to C$ in a category $\mathbb{C}$ is an idempotent if $e^{2}=e$. A splitting of such an idempotent $e$ is a retract of $C$

[TABLE]

such that $ir=e$, and we say an idempotent splits if it has a splitting. The category $\mathbb{C}$ is Cauchy complete if every idempotent splits.

Every splitting of an idempotent $e:C\to C$ arises as a coequalizer (and also an equalizer). We will make extensive use of the following corollaries of this fact so we record them here.

Proposition 5.2** ([Bor94, Prop. 6.5.4]).**

Consider an idempotent $e:C\to C$ in a category $\mathbb{C}$. If $e$ splits as $ir=e$, then $r$ is the coequalizer of the diagram $e,1_{C}:C\rightrightarrows C$. Conversely, any coequalizer of the diagram $e,1_{C}:C\rightrightarrows C$ gives a splitting of $e$.

Corollary 5.3**.**

Consider a category $\mathbb{C}$, idempotents $e:C\to C$ and $f:D\to D$ in $\mathbb{C}$, and a morphism $c:C\to D$ making the following diagram commute.

[TABLE]

Then splittings of both $e:C\to C$ and $f:D\to D$ extend uniquely to a splitting of the idempotent $\langle e,f\rangle$ in $\mathbb{C}^{\mathbb{2}}$. In particular, given a splitting $R\xrightarrow{i}C\xrightarrow{r}R$ of $e$ and a splitting $S\xrightarrow{j}D\xrightarrow{s}S$ of $f$, the following diagram displays the unique splitting of $\langle e,f\rangle$ in $\mathbb{C}^{\mathbb{2}}$.

[TABLE]

Moreover, if $c$ is an isomorphism, then so is $sci$.

Corollary 5.4**.**

If $\mathbb{C}$ is Cauchy complete, then $\mathbb{C}^{\mathbb{2}}$ is Cauchy complete.

Corollary 5.5**.**

If $\mathbb{C}$ is Cauchy complete, then any slice $\mathbb{C}/Y$ of $\mathbb{C}$ is Cauchy complete.

Corollary 5.6**.**

Splittings of idempotents are unique up to unique isomorphism.

The following lemma will be our main tool in establishing the results of this section.

Lemma 5.7** ([Bor94, Lem. 6.5.6]).**

If $\mathbb{C}$ is Cauchy complete, then any retract of any representable functor $\mathbb{C}^{\text{op}}\to\mathcal{S}et$ is representable.

5.2. Display map categories

Proposition 5.8**.**

Consider a Cauchy complete category $\mathbb{C}$. If $(\mathbb{C},\mathcal{D})$ is a display map category, then $(\mathbb{C},\overline{\mathcal{D}})$ is one as well.

Proof.

Since $\mathcal{D}\subseteq\overline{\mathcal{D}}$ and $\mathcal{D}$ contains all isomorphisms and morphisms to the terminal object, then $\overline{\mathcal{D}}$ does as well. Since $\overline{\mathcal{D}}$ is the right class of a lifting pair, it is stable under pullback (Lemma 4.3). It only remains to show that pullbacks of morphisms of $\overline{\mathcal{D}}$ exist.

Consider a morphism $d:X\to Y$ of $\overline{\mathcal{D}}$ and a morphism $\alpha:A\to Y$ of $\mathbb{C}$. By Proposition 4.4, $d$ is a retract in $\mathbb{C}/Y$ of some $d^{\prime}:X^{\prime}\to Y$ in $\mathcal{D}$. Let $P$ denote the pullback diagram category, and let $D,D^{\prime}:P\to\mathbb{C}$ denote the following two pullback diagrams in $\mathbb{C}$.

[TABLE]

Let $c$ denote the functor $\mathbb{C}\to[P,\mathbb{C}]$ which sends an object $m$ of $\mathbb{C}$ to the constant functor $c_{m}:P\to\mathbb{C}$ at $m$.

Then since $d$ is a retract of $d^{\prime}$ in $\mathbb{C}/Y$, the functor $D$ is a retract of $D^{\prime}$ in $[P,\mathbb{C}]$, and thus the functor $\text{Nat}(c(-),D):\mathbb{C}\to\mathcal{S}et$ is a retract of $\text{Nat}(c(-),D^{\prime}):\mathbb{C}\to\mathcal{S}et$. Now since we assume that there is a limit of the pullback diagram $D^{\prime}$, the functor $\text{Nat}(c(-),D^{\prime})$ is representable. Therefore, by Lemma 5.7, the functor $\text{Nat}(c(-),D)$ is also representable, and we conclude that $D$ has a limit.

Therefore, assuming that pullbacks of morphisms of $\mathcal{D}$ exist, pullbacks of morphisms of $\overline{\mathcal{D}}$ exist. ∎

5.3. $\Sigma$-types

Since $\overline{\mathcal{D}}$ is closed under composition, we immediately find that $(\mathbb{C},\overline{\mathcal{D}})$ models $\Sigma$-types. Note that for this result, we only use the hypothesis that $\mathbb{C}$ is Cauchy complete to ensure, by Proposition 5.8, that $(\mathbb{C},\overline{\mathcal{D}})$ is a display map category.

Proposition 5.9**.**

Consider a Cauchy complete category $\mathbb{C}$ and a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$- and $\mathtt{Id}$-types. Then $(\mathbb{C},\overline{\mathcal{D}})$ is a display map category which models $\Sigma$-types.

Proof.

$\overline{\mathcal{D}}$ is closed under composition by Lemma 4.3, and this means that $(\mathbb{C},\overline{\mathcal{D}})$ models $\Sigma$-types. ∎

5.4. $\mathtt{Id}$-types

Proposition 5.10**.**

Consider a Cauchy complete category $\mathbb{C}$. Suppose that $(\mathbb{C},\mathcal{D})$ is a display map category which models $\Sigma$-types and functorial $\mathtt{Id}$-types. Then $(\mathbb{C},\overline{\mathcal{D}})$ is a display map category which models functorial $\mathtt{Id}$-types.

Proof.

Fix a slice $\mathbb{C}/Y$ and an object $e\in\overline{\mathcal{D}}$ in this slice. We want to construct an $\mathtt{Id}$-type for $e$. There is a $d\in\mathcal{D}$ such that $e$ is a retract of $d$ (Proposition 4.4). Since we have an $\mathtt{Id}$-type on $d$, we have the following diagram in $\mathbb{C}/Y$ (where $i$, $s$ form the retraction and $r_{d},\epsilon_{d}$ form the $\mathtt{Id}$-type on $d$).

[TABLE]

Since the $\mathtt{Id}$ type is functorial, there is a morphism $\iota_{\langle is,is\times is\rangle}:\iota_{d}\to\iota_{d}$ making the following diagram commute.

[TABLE]

Since $\langle is,is\times is\rangle$ is an idempotent and this factorization is given functorially, the morphism $\iota_{\langle is,is\times is\rangle}$ is also an idempotent. By Lemma 5.5, $\mathbb{C}/Y$ is Cauchy complete, so we can split the idempotent $\iota_{\langle is,is\times is\rangle}$. Then by Corollary 5.3, this extends to splittings of the rectangles in diagram ($*$) above. This gives us the following commutative diagram.

[TABLE]

Now we see that the morphism $\epsilon_{e}$ is in $\overline{\mathcal{D}}$ since it is a retract of $\epsilon_{d}\in\mathcal{D}$.

Now, we need to show that for any $\alpha:a\to e$, the pullback $\alpha^{*}r_{e}$ is in ${}^{\boxslash}\overline{\mathcal{D}}$. Let $\epsilon_{xi}$ denote the composition $\pi_{i}\epsilon_{x}$ for $x=d,e$ and $i=0,1$. Since $r_{e}$ is a retract of $r_{d}$, as shown in the following diagram, $\alpha^{*}r_{e}$ is a retract of $\alpha^{*}r_{d}$.

[TABLE]

Since $\alpha^{*}r_{d}$ is in ${}^{\boxslash}\mathcal{D}$ by hypothesis, and ${}^{\boxslash}\mathcal{D}$ is closed under retracts, we find that $\alpha^{*}r_{e}$ is in ${}^{\boxslash}\overline{\mathcal{D}}$.

Therefore, $(\mathbb{C},\overline{\mathcal{D}})$ models functorial $\mathtt{Id}$-types. ∎

5.5. $\Pi$-types

Proposition 5.11**.**

Consider a Cauchy complete category of display maps $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types, $\mathtt{Id}$-types, and $\Pi$-types. Then the display map category $(\mathbb{C},\overline{\mathcal{D}})$ also models $\Pi$-types.

Proof.

Consider morphisms $f:X\to Y$ and $g:W\to X$ which are both in $\overline{\mathcal{D}}$. We aim to obtain a $\Pi$-type $\Pi_{f}g$.

Note that because

[TABLE]

is a pullback of $\rho(g)$, it is in $\mathcal{D}$.

[TABLE]

For any morphism $x$, let $M(x)$ denote the middle object of the factorization given in Proposition 4.2. We will also denote the morphism $\rho(g)\times_{Y}\mathtt{Id}(Y)$ as

[TABLE]

when it improves readability. (Note that the domain and codomain are indeed the middle objects of the factorizations of $f\circ\rho g$ and $f$, respectively.)

Since $M(\rho g)$ and $\rho f$ are in $\mathcal{D}$, we can form the $\Pi$-type $\Pi_{\rho f}M(\rho g)$ with the following bijection for any $y:A\to Y$ in $\mathbb{C}$.

[TABLE]

This means that $\Pi_{\rho(f)}M(\rho g)$ represents the functor

[TABLE]

We now show that $\mathbb{C}/X(f^{*}-,g)$ is a retract of this functor, so by Lemma 5.7, it will itself be representable.

Let $i$ denote the natural transformation

[TABLE]

which at a morphism $z:Z\to Y$ in $\mathbb{C}$, takes a morphism $m:f^{*}z\to g$ in $\mathbb{C}/X$

[TABLE]

to the following morphism in $\mathbb{C}/{Mf}$

[TABLE]

where $a$ and $b$ are given by solutions to the following lifting problems.

[TABLE]

(The morphism $\epsilon_{0}\times f\epsilon_{1}$ is in $\overline{\mathcal{D}}$ because it is the composition of $\epsilon_{0}\times\epsilon_{1}:\mathtt{Id}(X)\to X\times X$ with $1\times f:X\times X\to X\times Y$. The morphism $rg\times 1$ is in ${}^{\boxslash}\mathcal{D}$ because it is one of the pullbacks of $r:X\to\mathtt{Id}(X)$ ensured to be in ${}^{\boxslash}\mathcal{D}$ by the definition of $\mathtt{Id}$-types.)

Then let $r$ denote the natural transformation

[TABLE]

which at a morphism $z:Z\to Y$ in $\mathbb{C}$, takes a morphism $n:\rho f^{*}z\to M(\rho g)$ in $\mathbb{C}/{Mf}$

[TABLE]

to the following composition in $\mathbb{C}/{X}$

[TABLE]

where $c$ is a solution to the following lifting problem.

[TABLE]

Now we claim that

[TABLE]

is a retract diagram. To that end, consider a morphism $m$ of $\mathbb{C}/X(f^{*}z,g)$. Then $ri(m)$ is the following composition.

[TABLE]

The composition $a\circ(1_{X}\times r_{Y}):X\to\mathtt{Id}(X)$ is $r_{X}$. Thus, the composite of the first three vertical morphisms in the above diagram is

[TABLE]

Moreover, $b\circ(r_{X}\times 1_{W}):W\to W{\times_{\epsilon_{0}}}\mathtt{Id}(X)$ is $1_{W}\times r_{X}$ so the composite of the first four morphisms above is

[TABLE]

The composite $c\circ(1_{W}\times r_{X}):W\to W$ is the identity, so the vertical composite above is $m$. Therefore, $ri(m)=m$, and $i$ and $r$ form a retract.

Now by Lemma 5.7, we can conclude that $\mathbb{C}/X(f^{*}-,g):\mathbb{C}/Y\to\mathcal{S}et$ is representable by an object which we will denote by $\Pi_{f}g$. Furthermore, $\Pi_{f}g$ is a retract of $\Pi_{\rho f}M(\rho g)$. Since $\Pi_{\rho f}M(\rho g)$ is in $\mathcal{D}$, we can conclude that $\Pi_{f}g$ is in $\overline{\mathcal{D}}$, the retract closure of $\mathcal{D}$. Therefore, $(\mathbb{C},\overline{\mathcal{D}})$ does in fact model $\Pi$-types. ∎

5.6. Summary

Putting together Propositions 5.8, 5.9, 5.10, and 5.11, we get the following theorem.

Theorem 5.12**.**

Consider a Cauchy complete category $\mathbb{C}$ and a display map category $(\mathbb{C},\mathcal{D})$ which models $\Sigma$-types and functorial $\mathtt{Id}$-types. Then $(\mathbb{C},\overline{\mathcal{D}})$ is again a display map category modeling $\Sigma$- and functorial $\mathtt{Id}$-types. If $(\mathbb{C},\mathcal{D})$ also models $\Pi$-types, then $(\mathbb{C},\overline{\mathcal{D}})$ also models $\Pi$-types.

Proof.

By Proposition 5.8, $(\mathbb{C},\overline{\mathcal{D}})$ is a category with display maps. By Proposition 5.9, it models $\Sigma$-types. By Proposition 5.10, it models functorial $\mathtt{Id}$-types. By Proposition 5.11, it models $\Pi$-types. ∎

Corollary 5.13**.**

Consider a weak factorization system $(\mathcal{L},\mathcal{R})$ on a Cauchy complete category $\mathbb{C}$. The following are equivalent:

1. (1)

There is a subclass $\mathcal{D}\subseteq\mathcal{R}$ such that $\overline{\mathcal{D}}=\mathcal{R}$ and $(\mathbb{C},\mathcal{D})$ is a display map category which models $\Sigma$- and functorial $\mathtt{Id}$-types. 2. (2)

$(\mathbb{C},\mathcal{R})$* is a display map category which models $\Sigma$- and functorial $\mathtt{Id}$-types.*

The following are also equivalent:

1. (1)

There is a subclass $\mathcal{D}\subseteq\mathcal{R}$ such that $\overline{\mathcal{D}}=\mathcal{R}$ and $(\mathbb{C},\mathcal{D})$ is a display map category which models $\Sigma$-, functorial $\mathtt{Id}$-, and $\Pi$-types. 2. (2)

$(\mathbb{C},\mathcal{R})$* is a display map category which models $\Sigma$-, functorial $\mathtt{Id}$-, and $\Pi$-types.*

6. Display map categories reflected in weak factorization systems

In this last section, we remark that our main theorem (5.12) can be phrased more categorically as Theorem 6.1 below. Here, we consider various categories of display map categories on a fixed category $\mathbb{C}$. One might want to consider categories of display map categories with more structure, but we give here a simplified account of the situation to just expose a more categorical version of our result without being encumbered by technicalities.

Let $\mathbb{C}$ be a Cauchy complete category. Let $\mathcal{S}(\mathbb{C})$ denote the category whose objects are subclasses $\mathcal{M}$ of morphisms of $\mathbb{C}$ and whose morphisms $\mathcal{M}\to\mathcal{N}$ are inclusions $\mathcal{M}\subseteq\mathcal{N}$. Then we can identify the following four full subcategories of $\mathcal{S}(\mathbb{C})$:

• •

$\mathsf{DMC}_{\Sigma,\mathtt{Id}}(\mathbb{C})$, the full subcategory of $\mathcal{S}(\mathbb{C})$ spanned by those $\mathcal{M}$ such that $(\mathbb{C},\mathcal{M})$ is a display map category with $\Sigma$- and functorial $\mathtt{Id}$-types;

• •

$\mathsf{DMC}_{\Sigma,\mathtt{Id},\Pi}(\mathbb{C})$, the full subcategory of $\mathcal{S}(\mathbb{C})$ spanned by those $\mathcal{M}$ such that $(\mathbb{C},\mathcal{M})$ is a display map category with $\Sigma$-, functorial $\mathtt{Id}$-, and $\Pi$-types;

• •

$\mathsf{WFS}_{\Sigma,\mathtt{Id}}(\mathbb{C})$, the full subcategory of $\mathsf{DMC}_{\Sigma,\mathtt{Id}}(\mathbb{C})$ spanned by those $\mathcal{M}$ such that $(^{\boxslash}\mathcal{M},\mathcal{M})$ is a weak factorization system; and

• •

$\mathsf{WFS}_{\Sigma,\mathtt{Id},\Pi}(\mathbb{C})$, the full subcategory of $\mathsf{DMC}_{\Sigma,\mathtt{Id},\Pi}(\mathbb{C})$ spanned by those $\mathcal{M}$ such that $(^{\boxslash}\mathcal{M},\mathcal{M})$ is a weak factorization system.

Now we can state our main theorem as the existence of a reflector.

Theorem 6.1**.**

Consider a Cauchy complete category $\mathbb{C}$. The category $\mathsf{WFS}_{\Sigma,\mathtt{Id}}(\mathbb{C})$ is a reflective subcategory of $\mathsf{DMC}_{\Sigma,\mathtt{Id}}(\mathbb{C})$, and $\mathsf{WFS}_{\Sigma,\mathtt{Id},\Pi}(\mathbb{C})$ is a reflective subcategory of $\mathsf{DMC}_{\Sigma,\mathtt{Id},\Pi}(\mathbb{C})$. That is, there are left adjoints $L$ in the diagram below.

[TABLE]

Proof.

Consider the endofunctor on $\mathcal{S}(\mathbb{C})$ given on objects by $L(\mathcal{M}):=\overline{\mathcal{M}}$. By Theorem 5.12, this functor can be restricted to functors

[TABLE]

[TABLE]

To see that these are the left adjoints shown in the statement, we need to show for any $\mathcal{D}$ in $\mathsf{DMC}_{\Sigma,\mathtt{Id}}(\mathbb{C})$ and any $\mathcal{R}$ in $\mathsf{WFS}_{\Sigma,\mathtt{Id}}(\mathbb{C})$ that

[TABLE]

or, equivalently, that there is an inclusion $\overline{\mathcal{D}}\subseteq\mathcal{R}$ if and only if there is an inclusion $\mathcal{D}\subseteq\mathcal{R}$. If $\overline{\mathcal{D}}\subseteq\mathcal{R}$, then since $\mathcal{D}\subseteq\overline{\mathcal{D}}$, we have that $\mathcal{D}\subseteq\mathcal{R}$. If $\mathcal{D}\subseteq\mathcal{R}$, then $\overline{\mathcal{D}}\subseteq\overline{\mathcal{R}}$. Since $\overline{\mathcal{R}}=\mathcal{R}$ by Lemma 4.3, we have that $\overline{\mathcal{D}}\subseteq{\mathcal{R}}$. ∎

7. Outlook

In conclusion, we mention ways in which these results can be extended.

In Section 5.4, we showed that if $\mathbb{C}$ is a Cauchy complete category and $(\mathbb{C},\mathcal{D})$ is a display map category which models functorial $\mathtt{Id}$-types, then $(\mathbb{C},\overline{\mathcal{D}})$ also models functorial $\mathtt{Id}$-types. We needed the hypothesis that the $\mathtt{Id}$-types were functorial in order to use the hypothesis that $\mathbb{C}$ was Cauchy complete. However, this was not strictly necessary. In the next paper in this series, we will develop results which imply the following: if $\mathbb{C}$ is a Cauchy complete category and $(\mathbb{C},\mathcal{D})$ is a display map category which models $\mathtt{Id}$-types, then $(\mathbb{C},\overline{\mathcal{D}})$ also models $\mathtt{Id}$-types. This already appears as Proposition 2.5.9 in [Nor17].

In this paper, we have described a relationship between display map categories and weak factorization systems. We hope to upgrade this to a description of the relationship between comprehension categories and more structured weak factorization systems. In particular, the perspective taken in Theorem 6.1 will be the one appropriate for strengthening our results in that direction. This will build upon work done by Moss in [Mos18] in which he makes clear the relationship between Cauchy completion and comprehension categories.

Acknowledgements

I thank my PhD supervisor Martin Hyland for his guidance and many useful discussions regarding this work. I would also like to thank Benedikt Ahrens and Peter LeFanu Lumsdaine for reading and commenting on drafts of this paper. Thanks also go to the editor, Richard Garner, and the anonymous referees whose insightful comments were very helpful in forming the present paper.