# 7.7 Modalities

Our first thought regarding generalizing the theory of $n$-types might be to take \autorefthm:trunc-reflective as a definition.

###### Definition 7.7.1.

A reflective subuniverse is a predicate  $P:\mathcal{U}\to\mathsf{Prop}$ such that for every $A:\mathcal{U}$ we have a type $\ocircle A$ such that $P(\ocircle A)$ and a map $\eta_{A}:A\to\ocircle A$, with the property that for every $B:\mathcal{U}$ with $P(B)$, the following map is an equivalence:

 $\left\{\begin{array}[]{rcl}(\ocircle A\to{}B)&\longrightarrow&(A\to{}B)\\ f&\longmapsto&f\circ\eta_{A}\end{array}\right..$

We write $\P:\!\!\equiv\setof{A:\mathcal{U}|P(A)}$, so $A:\P$ means that $A:\mathcal{U}$ and we have $P(A)$. We also write $\mathsf{rec}_{\ocircle}$ for the quasi-inverse of the above map. The notation $\ocircle$ may seem slightly odd, but it will make more sense soon.

###### Theorem 7.7.2.

If $B:A\to\P$ is any family of types in a reflective subuniverse ¶, then $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$ is also in ¶.

###### Proof.

For any $x:A$, consider the function $\mathsf{ev}_{x}:(\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A% )}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x))% \to B(x)$ defined by $\mathsf{ev}_{x}(f):\!\!\equiv f(x)$. Since $B(x)$ lies in $P$, this extends to a function

 $\mathsf{rec}_{\ocircle}(\mathsf{ev}_{x}):\ocircle\Bigl{(}\mathchoice{\prod_{x:% A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}B(x)\Bigr{)}\to B(x).$

Thus we can define $h:\ocircle(\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x))\to% \mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$ by $h(z)(x):\!\!\equiv\mathsf{rec}_{\ocircle}(\mathsf{ev}_{x})(z)$. Then $h$ is a retraction of $\eta_{\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_% {(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}% {\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(% x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)}$, so that ${\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A% )}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)}$ is in $\P$. ∎

In particular, if $B:\P$ and $A$ is any type, then $(A\to B)$ is in ¶. In categorical language  , this means that any reflective subuniverse is an exponential ideal. This, in turn, implies by a standard argument that the reflector preserves finite products.

###### Corollary 7.7.3.

For any types $A$ and $B$ and any reflective subuniverse, the induced map $\ocircle(A\times B)\to\ocircle(A)\times\ocircle(B)$ is an equivalence.

###### Proof.

It suffices to show that $\ocircle(A)\times\ocircle(B)$ has the same universal property  as $\ocircle(A\times B)$. Thus, let $C:\P$; we have

 $\displaystyle(\ocircle(A)\times\ocircle(B)\to C)$ $\displaystyle=(\ocircle(A)\to(\ocircle(B)\to C))$ $\displaystyle=(\ocircle(A)\to(B\to C))$ $\displaystyle=(A\to(B\to C))$ $\displaystyle=(A\times B\to C)$

using the universal properties of $\ocircle(B)$ and $\ocircle(A)$, along with the fact that $B\to C$ is in ¶since $C$ is. It is straightforward to verify that this equivalence is given by composing with $\eta_{A}\times\eta_{B}$, as needed. ∎

It may seem odd that every reflective subcategory of types is automatically an exponential ideal, with a product-preserving reflector. However, this is also the case classically in the category  of sets, for the same reasons. It’s just that this fact is not usually remarked on, since the classical category of sets—in contrast to the category of homotopy types  —does not have many interesting reflective subcategories.

###### Theorem 7.7.4.

For a reflective subuniverse ¶, the following are logically equivalent.

1. 1.

If $A:\P$ and $B:A\to\P$, then $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)$ is in ¶.

2. 2.

for every $A:\mathcal{U}$, type family $B:\ocircle A\to\P$, and map $g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(\eta(a))$, there exists $f:\mathchoice{\prod_{z:\ocircle A}\,}{\mathchoice{{\textstyle\prod_{(z:% \ocircle A)}}}{\prod_{(z:\ocircle A)}}{\prod_{(z:\ocircle A)}}{\prod_{(z:% \ocircle A)}}}{\mathchoice{{\textstyle\prod_{(z:\ocircle A)}}}{\prod_{(z:% \ocircle A)}}{\prod_{(z:\ocircle A)}}{\prod_{(z:\ocircle A)}}}{\mathchoice{{% \textstyle\prod_{(z:\ocircle A)}}}{\prod_{(z:\ocircle A)}}{\prod_{(z:\ocircle A% )}}{\prod_{(z:\ocircle A)}}}B(z)$ such that $f(\eta(a))=g(a)$ for all $a:A$.

###### Proof.

Suppose 1. Then in the situation of 2, the type $\mathchoice{\sum_{z:\ocircle A}\,}{\mathchoice{{\textstyle\sum_{(z:\ocircle A)% }}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}}{% \mathchoice{{\textstyle\sum_{(z:\ocircle A)}}}{\sum_{(z:\ocircle A)}}{\sum_{(z% :\ocircle A)}}{\sum_{(z:\ocircle A)}}}{\mathchoice{{\textstyle\sum_{(z:% \ocircle A)}}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A% )}}}B(z)$ lies in $\P$, and we have $g^{\prime}:A\to\mathchoice{\sum_{z:\ocircle A}\,}{\mathchoice{{\textstyle\sum_% {(z:\ocircle A)}}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}{\sum_{(z:% \ocircle A)}}}{\mathchoice{{\textstyle\sum_{(z:\ocircle A)}}}{\sum_{(z:% \ocircle A)}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}}{\mathchoice{{% \textstyle\sum_{(z:\ocircle A)}}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}% }{\sum_{(z:\ocircle A)}}}B(z)$ defined by $g^{\prime}(a):\!\!\equiv(\eta(a),g(a))$. Thus, we have $\mathsf{rec}_{\ocircle}(g^{\prime}):\ocircle A\to\mathchoice{\sum_{z:\ocircle A% }\,}{\mathchoice{{\textstyle\sum_{(z:\ocircle A)}}}{\sum_{(z:\ocircle A)}}{% \sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}}{\mathchoice{{\textstyle\sum_{(z% :\ocircle A)}}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}{\sum_{(z:% \ocircle A)}}}{\mathchoice{{\textstyle\sum_{(z:\ocircle A)}}}{\sum_{(z:% \ocircle A)}}{\sum_{(z:\ocircle A)}}{\sum_{(z:\ocircle A)}}}B(z)$ such that $\mathsf{rec}_{\ocircle}(g^{\prime})(\eta(a))=(\eta(a),g(a))$.

Now consider the functions $\mathsf{pr}_{2}\circ\mathsf{rec}_{\ocircle}(g^{\prime}):\ocircle A\to\ocircle A$ and $\mathsf{id}_{\ocircle A}$. By assumption  , these become equal when precomposed with $\eta$. Thus, by the universal property of $\ocircle$, they are equal already, i.e. we have $p_{z}:\mathsf{pr}_{2}(\mathsf{rec}_{\ocircle}(g^{\prime})(z))=z$ for all $z$. Now we can define $f(z):\!\!\equiv{p_{z}}_{*}\mathopen{}\left({\mathsf{pr}_{2}(\mathsf{rec}_{% \ocircle}(g^{\prime})(z))}\right)\mathclose{},$ and the second component of $\mathsf{rec}_{\ocircle}(g^{\prime})(\eta(a))=(\eta(a),g(a))$ yields $f(\eta(a))=g(a)$.

Conversely, suppose 2, and that $A:\P$ and $B:A\to\P$. Let $h$ be the composite

 $\ocircle\Bigl{(}\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}% }{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)\Bigr{)}\xrightarrow{% \ocircle(\mathsf{pr}_{1})}\ocircle A\xrightarrow{\mathord{{(\eta_{A})}^{-1}}}A.$

Then for $z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}% }{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:% A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{% (x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)$ we have

 $\displaystyle h(\eta(z))$ $\displaystyle=\mathord{{\eta}^{-1}}(\ocircle(\mathsf{pr}_{1})(\eta(z)))$ $\displaystyle=\mathord{{\eta}^{-1}}(\eta(\mathsf{pr}_{1}(z)))$ $\displaystyle=\mathsf{pr}_{1}(z).$

Denote this path by $p_{z}$. Now if we define $C:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))\to\mathcal{U}$ by $C(w):\!\!\equiv B(h(w))$, we have

 $g:\!\!\equiv{\lambda}z.\,{p_{z}}_{*}\mathopen{}\left({\mathsf{pr}_{2}(z)}% \right)\mathclose{}\;:\;\mathchoice{\prod_{z:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x)}\,}{\mathchoice{{\textstyle\prod_{(z:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x))}}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{% (x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{\prod_{(z:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\mathchoice{{\textstyle\prod_{(z:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}% {\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)% }}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x% :A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_% {(x:A)}}}B(x))}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{% (x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\mathchoice{% {\textstyle\prod_{(z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\prod_{(z:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x))}}{\prod_{(z:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}}C(\eta(z)).$

Thus, the assumption yields $f:\mathchoice{\prod_{w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x))}\,}{\mathchoice{{\textstyle\prod_{(w:\ocircle(\mathchoice{\sum_{x:A% }\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(% x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum% _{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}B(x)))}}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x)))}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x)))}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x)))}}}{\mathchoice{{\textstyle\prod_{(w:\ocircle(\mathchoice{\sum_{x:A% }\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(% x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum% _{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}B(x)))}}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x)))}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x)))}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x)))}}}{\mathchoice{{\textstyle\prod_{(w:\ocircle(\mathchoice{\sum_{x:A% }\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(% x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum% _{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}B(x)))}}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x)))}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x)))}}{\prod_{(w:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x)))}}}C(w)$ such that $f(\eta(z))=g(z)$. Together, $h$ and $f$ give a function $k:\ocircle(\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:% A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))\to\mathchoice{\sum_{x:A}% \,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x% :A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_% {(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{% \sum_{(x:A)}}}B(x)$ defined by $k(w):\!\!\equiv(h(w),f(w))$, while $p_{z}$ and the equality $f(\eta(z))=g(z)$ show that $k$ is a retraction of $\eta_{\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)}$. Therefore, $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)$ is in ¶. ∎

Note the similarity to the discussion in \autorefsec:htpy-inductive. The universal property of the reflector of a reflective subuniverse is like a recursion principle with its uniqueness property, while \autorefthm:modal-char2 is like the corresponding induction principle. Unlike in \autorefsec:htpy-inductive, the two are not equivalent here, because of the restriction   that we can only eliminate into types that lie in $\P$. Condition 1 of \autorefthm:modal-char is what fixes the disconnect.

Unsurprisingly, of course, if we have the induction principle, then we can derive the recursion principle. We can also derive its uniqueness property, as long as we allow ourselves to eliminate into path types. This suggests the following definition. Note that any reflective subuniverse can be characterized by the operation $\ocircle:\mathcal{U}\to\mathcal{U}$ and the functions $\eta_{A}:A\to\ocircle A$, since we have $P(A)=\mathsf{isequiv}(\eta_{A})$.

###### Definition 7.7.5.

A modality is an operation $\ocircle:\mathcal{U}\to\mathcal{U}$ for which there are

1. 1.

functions $\eta^{\ocircle}_{A}:A\to\ocircle(A)$ for every type $A$.

2. 2.

for every $A:\mathcal{U}$ and every type family $B:\ocircle(A)\to\mathcal{U}$, a function

 $\mathsf{ind}_{\ocircle}:\Bigl{(}\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}\ocircle(B(\eta^{\ocircle}_{A}(a)))\Bigr{)}\to\mathchoice{\prod% _{z:\ocircle(A)}\,}{\mathchoice{{\textstyle\prod_{(z:\ocircle(A))}}}{\prod_{(z% :\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}}{\mathchoice% {{\textstyle\prod_{(z:\ocircle(A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:% \ocircle(A))}}{\prod_{(z:\ocircle(A))}}}{\mathchoice{{\textstyle\prod_{(z:% \ocircle(A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:% \ocircle(A))}}}\ocircle(B(z)).$
3. 3.

A path $\mathsf{ind}_{\ocircle}(f)(\eta^{\ocircle}_{A}(a))=f(a)$ for each $f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\ocircle(B(\eta^{\ocircle}% _{A}(a)))$.

4. 4.

For any $z,z^{\prime}:\ocircle(A)$, the function $\eta^{\ocircle}_{z=z^{\prime}}:(z=z^{\prime})\to\ocircle(z=z^{\prime})$ is an equivalence.

We say that $A$ is modal for $\ocircle$ if $\eta^{\ocircle}_{A}:A\to\ocircle(A)$ is an equivalence, and we write

 $\mathcal{U}_{\ocircle}:\!\!\equiv\setof{X:\mathcal{U}|X\text{ is \ocircle-% modal}}$ (7.7.5)

for the type of modal types.

Conditions 2 and 3 are very similar to \autorefthm:modal-char2, but phrased using $\ocircle B(z)$ rather than assuming $B$ to be valued in $\P$. This allows us to state the condition purely in terms of the operation $\ocircle$, rather than requiring the predicate $P:\mathcal{U}\to\mathsf{Prop}$ to be given in advance. (It is not entirely satisfactory, since we still have to refer to $P$ not-so-subtly in clause 4. We do not know whether 4 follows from 13.) However, the stronger-looking property of \autorefthm:modal-char2 follows from \autorefdefn:modality2 and 3, since for any $C:\ocircle A\to\mathcal{U}_{\ocircle}$ we have $C(z)\simeq\ocircle C(z)$, and we can pass back across this equivalence.

As with other induction principles, this implies a universal property.

###### Theorem 7.7.7.

Let $A$ be a type and let $B:\ocircle(A)\to\mathcal{U}_{\ocircle}$. Then the function

 $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\eta^{\ocircle}_{A}):\Bigl{(}% \mathchoice{\prod_{z:\ocircle(A)}\,}{\mathchoice{{\textstyle\prod_{(z:\ocircle% (A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A% ))}}}{\mathchoice{{\textstyle\prod_{(z:\ocircle(A))}}}{\prod_{(z:\ocircle(A))}% }{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}}{\mathchoice{{\textstyle% \prod_{(z:\ocircle(A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{% \prod_{(z:\ocircle(A))}}}B(z)\Bigr{)}\to\Bigl{(}\mathchoice{\prod_{a:A}\,}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(% a:A)}}{\prod_{(a:A)}}}B(\eta^{\ocircle}_{A}(a))\Bigr{)}$

is an equivalence.

###### Proof.

By definition, the operation $\mathsf{ind}_{\ocircle}$ is a right inverse  to $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\eta^{\ocircle}_{A})$. Thus, we only need to find a homotopy   $\mathchoice{\prod_{z:\ocircle(A)}\,}{\mathchoice{{\textstyle\prod_{(z:\ocircle% (A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A% ))}}}{\mathchoice{{\textstyle\prod_{(z:\ocircle(A))}}}{\prod_{(z:\ocircle(A))}% }{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}}{\mathchoice{{\textstyle% \prod_{(z:\ocircle(A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{% \prod_{(z:\ocircle(A))}}}s(z)=\mathsf{ind}_{\ocircle}(s\circ\eta^{\ocircle}_{A% })(z)$

for each $s:\mathchoice{\prod_{z:\ocircle(A)}\,}{\mathchoice{{\textstyle\prod_{(z:% \ocircle(A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:% \ocircle(A))}}}{\mathchoice{{\textstyle\prod_{(z:\ocircle(A))}}}{\prod_{(z:% \ocircle(A))}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:\ocircle(A))}}}{\mathchoice{% {\textstyle\prod_{(z:\ocircle(A))}}}{\prod_{(z:\ocircle(A))}}{\prod_{(z:% \ocircle(A))}}{\prod_{(z:\ocircle(A))}}}B(z)$, exhibiting it as a left inverse as well. By assumption, each $B(z)$ is modal, and hence each type $s(z)=R^{\ocircle}_{X}(s\circ\eta^{\ocircle}_{A})(z)$ is also modal. Thus, it suffices to find a function of type

 $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}s(\eta^{\ocircle}_{A}(a))=% \mathsf{ind}_{\ocircle}(s\circ\eta^{\ocircle}_{A})(\eta^{\ocircle}_{A}(a)).$

which follows from \autorefdefn:modality3. ∎

In particular, for every type $A$ and every modal type $B$, we have an equivalence $(\ocircle A\to B)\simeq(A\to B)$.

###### Corollary 7.7.8.

For any modality $\ocircle$, the $\ocircle$-modal types form a reflective subuniverse satisfying the equivalent conditions of \autorefthm:modal-char.

Thus, modalities can be identified with reflective subuniverses closed under $\Sigma$-types. The name modality comes, of course, from modal logic, which studies logic where we can form statements such as “possibly $A$” (usually written $\diamond A$) or “necessarily $A$” (usually written $\Box A$). The symbol $\ocircle$ is somewhat common for an arbitrary modal operator. Under the propositions-as-types principle, a modality in the sense of modal logic corresponds to an operation on types, and \autorefdefn:modality seems a reasonable candidate for how such an operation should be defined. (More precisely, we should perhaps call these idempotent   , monadic modalities; see the Notes.) As mentioned in \autorefsubsec:when-trunc, we may in general use adverbs to speak informally about such modalities, such as “merely” for the propositional truncation and “purely” for the identity   modality (i.e. the one defined by $\ocircle A:\!\!\equiv A$).

For any modality $\ocircle$, we define a map $f:A\to B$ to be $\ocircle$ if $\ocircle({\mathsf{fib}}_{f}(b))$ is contractible  for all $b:B$, and to be $\ocircle$-truncated if ${\mathsf{fib}}_{f}(b)$ is modal for all $b:B$. All of the theory of \autorefsec:connectivity,\autorefsec:image-factorization which doesn’t involve relating $n$-types for different values of $n$ applies verbatim in this generality. In particular, we have an orthogonal factorization system.

An important class of modalities which does not include the $n$-truncations is the left exact modalities: those for which the functor $\ocircle$ preserves pullbacks as well as finite products. These are a categorification of “Lawvere-Tierney topologies” in elementary topos theory, and correspond in higher-categorical semantics to sub-$(\infty,1)$-toposes. However, this is beyond the scope of this book.

Some particular examples of modalities other than $n$-truncation can be found in the exercises.

Title 7.7 Modalities
\metatable