Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids.
It is being developed as a new foundation for mathematics and as an
internal language for (elementary) higher toposes.
We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a “localization” higher inductive type.
This produces in particular the ($n$-connected, $n$-truncated)
factorization system as well as internal presentations of subtoposes,
through lex modalities.
We also develop the semantics of these constructions.

§ INTRODUCTION

In traditional modal logic, a modality is a unary operation on propositions.
The classical examples are $\Box$ (“it is necessary that”) and $\lozenge$ (“it is possible that”).
In type theory and particularly dependent type theory, such as homotopy type theory, where propositions are regarded as certain types, it is natural to extend the notion of modality to a unary operation on types.
For emphasis we may call this a “typal modality”, or a “higher modality” since it acts on the “higher types” available in homotopy type theory (not just “sets” but types containing higher homotopy).

There are many kinds of propositional modalities, but many of them are either monads or comonads.
Monads and comonads on a poset (such as the poset of propositions) are also automatically idempotent, but this is no longer true for more general monads and comonads.
Thus there are many possible varieties of typal and higher modalities.

Typal modalities in non-dependent type theory have a wide range of applications in computer science.
In particular, following the pioneering work of [30], monadic typal modalities are commonly used to model effects in programming languages.
Non-dependent modal type theory is now a flourishing field with this and many other applications; see [15] for an overview.

In this paper we take a first step towards the study of higher modalities in homotopy type theory, restricting our attention to idempotent, monadic ones.
These are especially convenient for a number of reasons.
One is that in homotopy type theory, as in higher category theory, we expect a general monad (or comonad) to require infinitely many higher coherence conditions, which we don't know how to express in the finite syntax of type theory; whereas an idempotent one can instead be described using the universal property of a reflector into a subcategory.
(We can still use particular non-idempotent monadic modalities, such as the “partial elements” monad of [1, 17], without making all this coherence explicit, but it is harder to develop a general theory of them.)

Another is that in good situations, an idempotent monad can be extended to all slice categories consistently, and thereby represented “fully internally” in type theory as an operation $\modal : \UU\to\UU$ on a type universe.
Idempotent comonadic modalities have also been considered in dependent type theory and homotopy type theory (see for instance [31, 16, 34, 38]), but they generally require modifying the judgmental structure of type theory.
By contrast, our theory of modalities can be (and has been) formalized in existing proof assistants without modifying the underlying type theory.

Idempotent monadic modalities also include many very important
examples. The $(-1)$-truncation in homotopy type theory is a
higher-dimensional version of the bracket modality, which in 1-category theory
characterizes regular categories [4]. More
generally, the $n$-truncation modalities are prominent examples of modalities; indeed almost all of the theory of truncation and connectedness in <cit.> is just a specialization of the theory of a general modality.
More generally, we can produce idempotent monadic modalities by localization or nullification at small families, using a higher inductive type.
Finally, among idempotent monadic modalities we also find the left exact ones, which correspond semantically to subtoposes.

For the rest of this paper we will say simply modality to mean an idempotent monadic modality.
However, this should be regarded as only a local definition; in more general contexts the word “modality” should continue to encompass comonadic modalities and other sorts.

In fact, our use of the word “modality” will be a little more specific even than this.
If we express internally the most naïve notion of “idempotent monad on $\UU$”, we obtain a notion that we call a reflective subuniverse.
However, many reflective subuniverses that arise in practice, including truncation and left exact modalities (and, in fact, all concrete examples we will consider in this paper), satisfy the further property of being closed under $\Sigma$-types; it is these that we will call modalities.
We emphasize this property not just because it holds in many examples, but because it can be equivalently expressed by giving the modal operator a dependent elimination principle analogous to that of an inductive type.
This is a very natural thing to ask for when generalizing propositional modalities to typal operations.

The naturalness of this notion of modality is further supported by the fact that it has many equivalent characterizations.
In addition to a reflective subuniverse closed under $\Sigma$-types and a modal operator with a dependent eliminator, a modality can be defined using a “dependent universal property”, and more interestingly as a stable orthogonal factorization system.
The right class of maps in the factorization system consists of those whose fibers belong to the subuniverse (“modal maps”), while the left class consists of those whose fibers have contractible reflection into the subuniverse (“connected maps”).
The internal nature of the definition means that a stable factorization system is entirely determined by the fibers of its right class, which form a modality.[Non-stable factorization systems are not so determined, although they do have an underlying reflective subuniverse, and most reflective subuniverses can be extended to factorization systems.]
We prove the equivalence of all these definitions in <ref>, developing along the way some basic theory of reflective subuniverses, connected maps, and factorization systems.

In unaugmented Martin-Löf type theory we can define a few particular modalities, such as the double-negation modality, and the “open modality” associated to any mere proposition.
However, most interesting modalities require higher inductive types for their construction, including the $n$-truncations and the dual “closed modality” associated to a proposition.
In <ref> we give a general construction of modalities using a higher inductive localization type: given a family of maps $F:\prd{a:A} B(a) \to C(a)$, a type $X$ is $F$-local if the precomposition map $(C(a)\to X) \to (B(a)\to X)$ is an equivalence for all $a:A$, and the $F$-localization $\localization{F} X$ is the universal $F$-local type admitting a map from $X$.
We call a modality accessible if it can be generated by localization; this is inspired by the corresponding notion in category theory.
Accessible modalities include the $n$-truncation and open and closed modalities, as well as many examples from homotopy theory, where localization is a standard technique; thus we expect them to be a useful tool in the synthetic development of homotopy theory inside type theory.[Our notion of localization, being internal, is a little stronger than the standard sort of localization in homotopy theory; but in many cases it is equivalent.
The higher inductive construction of localization, when interpreted model-categorically according to the semantics of [26], also appears to be new and may be of independent interest in homotopy theory.]

In general, localization at a family of maps produces a reflective subuniverse (and, in fact, an orthogonal factorization system), but not necessarily a modality.
However, there is a simple condition which ensures that we do get a modality, namely that $C(a)=\unit$ for all $a:A$.
In this case the local types are those for which “every map $B(a)\to X$ is uniquely constant”; following standard terminology in homotopy theory we call them $B$-null and the corresponding localization $B$-nullification.
Any accessible modality can be presented as a nullification.

A very important class of modalities that excludes the $n$-truncations are the left exact, or lex, ones, which we study in <ref>.
These have many equivalent characterizations, but the most intuitive is simply that the reflector preserves finite limits.
When homotopy type theory is regarded as an internal language for higher toposes, lex modalities correspond to subtoposes.
In the traditional internal logic of 1-toposes, subtoposes are
represented by Lawvere-Tierney operators on the subobject
classifier, which generate a subtopos by internal
sheafification. Goldblatt [20] provides an overview
of the modal logic perspective on these operators on propositions.
Dependent type theory allows us to speak directly about the subtopos as an operation on a type universe (the lex modality), and show internally that any Lawvere-Tierney operator on the universe of propositions gives rise to a lex modality.

There is an additional subtlety here that only arises for $\infty$-toposes and homotopy type theory.
In 1-topos theory, and indeed in $n$-topos theory for any $n<\infty$, every lex modality (subtopos) arises from a Lawvere-Tierney operator; but in $\infty$-topos theory this is no longer true.
The subtoposes that are determined by their behavior on propositions are called topological in [28], and we appropriate this name for lex modalities of this sort as well.
The dual cotopological sort of lex modalities, including the hypercompletion, are harder to construct in type theory, but we can at least show that insofar as they exist they behave like their $\infty$-categorical analogues.

When this paper was written, we did not know any condition on a type family $B$ that ensured that $B$-nullification is lex and such that any accessible lex modality can be presented by such a $B$.
But as we were preparing it for final publication, [2] found such a condition: that $B$ is closed under taking path spaces.
In this case we may refer to $B$-nullification as a lex nullification.

<ref> displays in a Venn diagram all the different structures discussed above.
Lex modalities are a subclass of modalities, which are a subclass of reflective subuniverses.
In principle all three structures can be either accessible or non-accessible, although in practice non-accessible ones are very hard to come by; with topological modalities a subclass of the accessible lex ones.
Individual examples are displayed in single boxes, while general classes of examples (obtained by localization and restricted classes thereof) are displayed in double boxes.

(0,0.7) ellipse (6 and 3.8);
at (0,4.2) reflective subuniverses;
(-1.3,.5) ellipse (4.3 and 3.2);
at (-1.3,3.4) accessible;
(1.2,.3) ellipse (4.2 and 3.1);
at (2.8,2.7) modalities;
(1.3,-.5) ellipse (3.7 and 2);
at (3.5,.8) lex;
(0,-.8) ellipse (2 and 1.3);
at (0,0.2) topological;
[rectangle,draw] at (0,2.5) $n$-truncation;
[rectangle,draw,double] at (0,2) nullifications;
[rectangle,draw,double] at (1.5,1) lex nullifications;
[rectangle,draw,double] at (-4.3,1) localizations;
[rectangle,draw] at (3.8,1.7) double neg.;
[rectangle,draw] at (-.5,-.5) open;
[rectangle,draw] at (.5,-.5) closed;
[rectangle,draw,double] at (0,-1) prop. nullifications;
[rectangle,draw] at (3,0) hypercompletion?;

Modalities and related structures

Viewing accessible lex modalities as subtoposes, we naturally expect that the subtopos should support its own internal language.
This is true, although we do not prove it precisely; we simply observe that the universe of modal types is closed under many type constructors and admits its own versions of all the others.
In particular, the universe of modal types for an accessible lex modality is itself a modal type for the same modality (in fact, this characterizes lex modalities among accessible ones).
Since any $\infty$-topos arises as a subtopos of a presheaf $\infty$-topos, we can essentially reduce the problem of finding univalent internal languages for $\infty$-toposes to that of finding them for presheaf $\infty$-toposes (and of finding universes closed under accessible lex modalities; see <ref>).
A similar argument, using judgementally strict idempotent monads, has already been used in the so-called “cubical stack” models of type theory [14, 13] (which do not actually in general lie in $\infty$-stack toposes) to prove independence results for homotopy type theory.

We end the main part of the paper with a general “fracture and gluing” theorem about modalities: if $\modal$ is any modality and $\lozenge$ is a lex modality that is “strongly disjoint” from $\modal$, then the join $\lozenge\lor\modal$ in the poset of modalities can be constructed using a “pullback fracture square”.
When applied to the open and closed modalities associated to a proposition, this specializes to an internal viewpoint on Artin gluing.
We call it a “fracture theorem” since the pullback squares appear formally analogous to the fracture squares in the classical theory of localization and completion at primes, though we do not know of a precise relationship.

In the final part of the paper, <ref>, we sketch a semantic interpretation of our theory in terms of comprehension categories and $(\infty,1)$-toposes.
In particular, we show that well-behaved reflective subcategories of $(\infty,1)$-toposes give rise to modalities in their internal languages, while dually modalities give rise to reflective subcategories of syntactic $(\infty,1)$-categories.
In this discussion we ignore the issue of universes, which it is not known how to model semantically in general $(\infty,1)$-toposes (except in a weak sense).

We will freely use the results and the notations from [40].
In fact, parts of this work have already appeared as <cit.>.
We generalize much of this section 7.6 to general modalities in our <ref>, which also sharpens the results in <cit.>.
In particular, we will freely use function extensionality and the univalence axiom, often without comment.

Finally, we note that many of the results in this paper have been formalized in the Coq proof assistant [5].
However, the organization of results in the library is rather different than in this paper.
A rough correspondence is as follows; unless otherwise noted all files are in the  directory.

Sections     Library files
<ref>      and

Examples (<ref>)     , , , ,

<ref>      and

<ref>      and

There are also some differences in the proof techniques used in the library and in this paper.
In the library, localizations are constructed using “$\infty$-extendability” as a characterization of equivalences to avoid function extensionality hypotheses, as described in [35].
In addition, much attention is paid to ensuring appropriate universe polymorphism with parametrized modules; this is described in <cit.>.
We will not discuss these issues further here; see the cited references and the comments in the library for more information.

§ MODALITIES, REFLECTIVE SUBUNIVERSES AND FACTORIZATION SYSTEMS

In this section we will introduce the following four notions of modality
and prove that they are all equivalent:

* Higher modalities

* Uniquely eliminating modalities

* $\Sigma$-closed reflective subuniverses

* Stable orthogonal factorization systems

After their equivalence has been established, we will call all of them simply modalities.

The first three definitions have the following data in common: by a modal operator we mean a function $\modal:\UU\to\UU$, and by a modal unit we mean a family of functions $\modalunit^\modal:\prd*{A:\UU}A\to\modal A$.[In general we write $f:\prd*{x:A} B(x)$ instead of $f:\prd{x:A} B(x)$ to indicate that the argument $x$ of $f$ is implicit.]
Given these data, we say a type $X$ is modal if $\modalunit[X]:X\to\modal X$ is an equivalence, and we write $\UU_\modal \defeq \sm{X:\UU} \ismodal(X)$ for the subuniverse of modal types.
More generally, if $\mathcal{M}:\UU\to\prop$ is any predicate on the universe, we write $\UU_{\mathcal{M}} \defeq \sm{X:\UU} \mathcal{M}(X)$.

A higher modality consists of a modal operator and modal unit together with

* for every $A:\UU$ and every dependent type $P:\modal A\to\UU$, a

\begin{equation*}
\mathsf{ind}^\modal_A:\big(\prd{a:A}\modal(P(\eta(a)))\big)\to\prd{z:\modal A}\modal(P(z)).
\end{equation*}

* An identification

\begin{equation*}
\mathsf{comp}^\modal_A(f,x):\id{\mathsf{ind}^\modal_A(f)(\eta(x))}{f(x)}
\end{equation*}

for each $f:\prd{x:A}\modal(P(\eta(x)))$ and $x:A$.

* For any $x,y:\modal A$ the modal unit $\modalunit[(\id{x}{y})]:\id{x}{y}\to \modal(\id{x}{y})$ is an equivalence.

One might think of eliminating into a $P:\modal A\to \UU_\modal$ directly rather than into $\modal\circ P$ for a $P:\modal A\to \UU$, but in that case we would be unable to show that $\modal A$ is a modal type (<ref>).

A uniquely eliminating modality consists of
a modal operator and modal unit such that the function

\begin{equation*}
\lam{f} f\circ\modalunit[A] : (\prd{z:\modal A}\modal(P(z)))\to(\prd{x:A}\modal(P(\modalunit[A](x))))
\end{equation*}

is an equivalence for any $A$ and any $P:\modal A\to\UU$.

A reflective subuniverse is a family $\ismodal:\UU\to\prop$, together with a
modal operator and modal unit such that $\ismodal(\modal A)$ for
every $A:\UU$, and for every $B:\UU$ satisfying
$\ismodal(B)$, the function

\begin{equation*}
\lam{f} f\circ \modalunit[A]:(\modal A\to B)\to (A\to B)
\end{equation*}

is an equivalence.
A reflective subuniverse is $\Sigma$-closed if whenever $\ismodal(X)$ and $\ismodal(P(x))$ for all $x:X$, we have $\ismodal(\sm{x:X}P(x))$.

Note that unlike <ref>, in <ref> the notion of “modal type” is part of the data.
However, we will show in <ref> that $\ismodal(A)$ if and only if $\modalunit[A]$ is an equivalence.

An orthogonal factorization system consists of
predicates $\mathcal{L},\mathcal{R}:\prd*{A,B:\UU} (A\to B)\to\prop$ such that

* $\mathcal{L}$ and $\mathcal{R}$ are closed under composition and contain all identities (i.e. they are subcategories of the category of types that contain all the objects), and

* the type $\fact_{\mathcal{L},\mathcal{R}}(f)$ of factorizations

\begin{equation*}
\begin{tikzcd}
A \arrow[rr,"f"] \arrow[dr,swap,"f_{\mathcal{L}}"] & & B \\
& \im_{\mathcal{L},\mathcal{R}}(f) \arrow[ur,swap,"f_{\mathcal{R}}"]
\end{tikzcd}
\end{equation*}

of $f$, with $f_{\mathcal{L}}$ in $\mathcal{L}$ and $f_{\mathcal{R}}$ in $\mathcal{R}$, is contractible.

More precisely, the type $\fact_{\mathcal{L},\mathcal{R}}(f)$ is defined to
be the type of

\begin{equation*}
\end{equation*}

consisting of a type $\im_{\mathcal{L},\mathcal{R}}(f)$, a function $f_{\mathcal{L}}:A\to \im_{\mathcal{L},\mathcal{R}}(f)$ with
$p:\mathcal{L}(f_{\mathcal{L}})$, a function $f_{\mathcal{R}}:\im_{\mathcal{L},\mathcal{R}}(f)\to B$ with $q:\mathcal{R}(f_{\mathcal{R}})$, and an identification $h:\id{f}{f_{\mathcal{R}}\circ f_{\mathcal{L}}}$. The type $\im_{\mathcal{L},\mathcal{R}}(f)$ is called
the $(\mathcal{L},\mathcal{R})$-image of $f$.

A type $X$ is said to be $(\mathcal{L},\mathcal{R})$-modal if
the map $!:X\to\unit$ is in $\mathcal{R}$ (and hence $!_\mathcal{L}$
is an equivalence).

An orthogonal factorization system is said to be stable if the class
$\mathcal{L}$ is stable under pullbacks (By
<ref>, $\mathcal{R}$ is always stable under pullbacks).

By univalence, the fact that $\mathcal{L}$ and $\mathcal{R}$ contain all identities implies that they each contain all equivalences.
Conversely, if $f\in \mathcal{L}\cap\mathcal{R}$, then $(\idfunc,f)$ and $(f,\idfunc)$ are both $(\mathcal{L},\mathcal{R})$-factorizations of $f$, and hence equal; which implies that $f$ is an equivalence.
Thus, $\mathcal{L}\cap\mathcal{R}$ consists exactly of the equivalences.

We now consider a few examples.
Since we will eventually prove all the definitions to be equivalent, we can use any one of them to describe any particular example.

The prime example is the $n$-truncation modality $\truncf n$ as studied in <cit.>, which we also denote $\truncmod{n}$.
This can be given as a higher modality, using its induction principle and the fact that $\trunc n A$ is an $n$-type and the identity types of an $n$-type are again $n$-types (indeed, $(n-1)$-types).
The corresponding stable orthogonal factorization system, consisting of $n$-connected and $n$-truncated maps, is also constructed in <cit.>; our construction in <ref> will be a generalization of this.

Let $Q$ be a mere proposition.
The open modality determined by $Q$ is defined by $\open Q A = (Q\to A)$, with unit $\modalunit[A](x) = \lam{\nameless}x : A \to (Q \to A)$.
(We call it “open” because semantically, it generalizes the open subtopos associated to a subterminal object of a topos, which in turn is so named because in the case of sheaves on a topological space $X$ it specializes to the open subspaces of $X$.)
To show that this is a higher modality, suppose we have $P: (Q\to A) \to \UU$ and $f:\prd{a:A} Q \to P(\lam{\nameless} a)$.
Then for any $z:Q\to A$ and $q:Q$ we have $f(z(q),q) : P(\lam{\nameless} z(q))$.
And since $Q$ is a mere proposition, we have $z(q) = z(q')$ for any $q':Q$, hence $e(z,q) : (\lam{\nameless} z(q)) = z$ by function extensionality.
This gives

\[ \lam{z}{q} \trans{e(z,q)}{(f(z(q),q))} : \prd{z:Q\to A} Q \to P(z). \]

For the computation rule, we have

\begin{align*}
(\lam{z}{q} \trans{e(z,q)}{(f(z(q),q))})(\lam{\nameless} a) &= \lam{q} \trans{e(\lam{\nameless} a,q)}{(f(a,q))}\\
&= \lam{q} f(a,q) = f(a)
\end{align*}

by function extensionality, since $e(\lam{\nameless} a,q) = \refl{}$.
Finally, if $x,y:Q\to A$, then $(x=y) \simeq \prd{q:Q} x(q) = y(q)$, and the map

\[ \Big(\prd{q:Q} x(q) = y(q)\Big) \to \Big( Q \to \prd{q:Q} x(q) = y(q)\Big) \]

is (by currying) essentially precomposition with a product projection $Q\times Q\to Q$, and that is an equivalence since $Q$ is a mere proposition.

Again, let $Q$ be a mere proposition.
The closed modality determined by $Q$ is defined by $\closed Q A = Q \ast A$, the join of $Q$ and $A$ (the pushout of $Q$ and $A$ under $Q\times A$).
(As for open modalities, closed modalities generalize closed subtoposes, which in turn generalize closed subspaces of topological spaces.)
We show that this is a $\Sigma$-closed reflective subuniverse.
Define a type $B$ to be modal if $Q \to \iscontr(B)$, and note that it is indeed the case that $Q\to\iscontr(Q\ast A)$, for any type $A$.
By the universal property of pushouts, a map $Q \ast A \to B$ consists of a map $f:A\to B$ and a map $g:Q\to B$ and for any $a:A$ and $q:Q$ an identification $p:f(a)=g(q)$.
But if $Q \to \iscontr(B)$, then $g$ and $p$ are uniquely determined, so this is just a map $A\to B$.
Thus $(\closed Q A \to B) \to (A\to B)$ is an equivalence, so we have a reflective subuniverse.
It is $\Sigma$-closed since the dependent sum of a contractible family of types over a contractible base is contractible.

The double negation modality is defined by $A\mapsto \neg\neg A$, i.e. $(A\to \emptyt)\to \emptyt$, with $\modalunit(a) = \lam{g} g(a)$.
We show that this is a uniquely eliminating modality.
Since the map $\lam{f}f\circ \modalunit[A]$ that must be an equivalence has mere propositions as domain and codomain, it suffices to give a map in the other direction.
Thus, let $P: \neg\neg A \to \UU$ and $f:\prd{a:A} \neg \neg P(\lam{g} g(a))$; given $z:\neg\neg A$ we must derive a contradiction from $g:\neg P(z)$.
Since we are proving a contradiction, we can strip the double negation from $z$ and assume given an $a:A$.
And since $\neg\neg A$ is a mere proposition, we have $z = \lam{g} g(a)$, so that we can transport $f(a)$ to get an element of $\neg\neg P(z)$, contradicting $g$.

The trivial modality is the identity function on $\UU$.
It coincides with $\open \top$ and with $\closed\bot$.

Dually, the zero modality sends all types to $\unit$.
It is equivalently the $(-2)$-truncation, and coincides with $\open\bot$ and with $\closed \top$.

In each of <ref>
we have defined what it means for a type to be modal. In each case, being
modal is a family of mere propositions indexed by the universe, i.e. a subuniverse.
We will show in <ref> that each kind of structure is completely determined by this subuniverse.
(<ref> is more general, not requiring $\Sigma$-closedness.)

It follows that the type of all modalities of each
kind is a subset of the set $\UU\to\prop$ of all subuniverses, and in particular is a set.
This makes it easier to establish
the equivalences of the different kinds of modalities.
It suffices
to show that any modality of one kind determines a modality of the next kind
with the same modal types, which we will do as follows:

higher modality [dr,bend left,"<ref>"]

3cmstable factorization system [ur,bend left,"<ref>"]
3cmuniquely eliminating modality [dl,bend left,"<ref>"]

3cm$\Sigma$-closed reflective subuniverse [ul,bend left,"<ref>"]

Before <ref> we take the opportunity to develop a bit more theory of reflective subuniverses, including closure under identity types (<ref>) and dependent products
(<ref>), along with several equivalent characterizations of $\Sigma$-closedness (<ref>).

Of these equivalences, the most surprising is that a stable factorization system is uniquely determined by its underlying reflective subuniverse of types.
This is false for stable factorization systems on arbitrary categories. However, an analogous fact is true in classical set-based mathematics for stable factorization systems on the category of sets (although in that case there are much fewer interesting examples). It is this fact about the category of sets which is analogous to the statement we prove in type theory about factorization systems on the category of types.

We will also see in <ref> that when type theory is interpreted in a higher category, the data of a reflective subuniverse or modality has to be interpreted “fiberwise”, giving a richer structure than a single reflective subcategory.

§.§ Higher modalities

We start by showing that a higher modality is determined by its modal types, and gives rise to a uniquely eliminating modality.

If $\modal$ is a higher modality, then any type of the form $\modal X$ is modal.

We want to show that the modal unit $\modalunit[\modal X]:\modal X\to\modal\modal X$
is an equivalence. By the induction principle and the computation rule for
higher modalities, we find a function $f:\modal \modal X\to\modal X$ with
the property that $f\circ \modalunit[\modal X]\htpy\idfunc[\modal X]$. We wish to
show that we also have $\modalunit[\modal X]\circ f\htpy\idfunc$. Since identity
types of types of the form $\modal Y$ are declared to be modal, it is
equivalent to find a term of type

\begin{equation*}
\prd{z:\modal \modal X}\modal(\modalunit[\modal X](f(z))=z).
\end{equation*}

Now we are in the position to use the induction principle of higher modalites
again, so it suffices to show that $\modalunit(f(\modalunit(z)))=\modalunit(z)$
for any $z:\modal X$. This follows from the fact that $f\circ\modalunit=\idfunc$.

The data of two higher modalites $\modal$ and $\modal'$
are identical if and only if they have the same modal types.

Another way of stating this is that the function from the type of all
modalities on $\UU$ to the type $\UU\to\prop$ of predicates on $\UU$, given
by mapping a modality to the predicate $\ismodal$, is an embedding. Thus, we
need to show that for any predicate $\mathcal{M}:\UU\to\prop$, we can find at
most one modality for which $\mathcal{M}$ is the class of modal types.

To be precise, consider for any $\mathcal{M}:\UU\to\prop$ and $X:\UU$, the type

of tuples $(Y,p,\pi,I,C)$ such that

* $Y$ is a type.

* $p:\mathcal{M}(Y)$.

* $\pi:X\to Y$.

* $I_P:(\prd{x:X} P(\pi(x)))\to(\prd{y:Y} P(y))$ for any $P:Y\to\UU_{\mathcal{M}}$.

* $C$ witnesses that each $I_P$ is a right inverse of precomposing with $\pi$.

We will show that this type is a mere proposition.
First, we show that the
type of pairs $(I,C)$, with $I$ and $C$ of the indicated types, is a mere
proposition for any $(Y,p,\pi)$. After that, we show that the type of triples
$(Y,p,\pi)$ is also a mere proposition. These two facts combined prove the

Consider a type $Y$ satisfying $\mathcal{M}$, and a function $\pi:X\to Y$, and
let $(I,C)$ and $(I',C')$ be two terms witnessing that $Y$ satisfies an induction
principle with a computation rule. We want to show that $(I,C)=(I',C')$, and of
course it suffices to show that $(I(s),C(s))=(I'(s),C(s))$ for any
$P:Y\to\UU_{\mathcal{M}}$ and $s:\prd{x:X}P(\pi(x))$.

To show that $I(s,y)=I'(s,y)$ for any $y:Y$, we use
the induction principle $(I,C)$. So it suffices to show that
$I(s,\pi(x))=I'(s,\pi(x))$. Both of these terms are equal to $s(x)$. Thus,
we obtain a proof $J(s,y)$ that $I(s,y)=I'(s,y)$, with the property that
Now we need to show that $\trans{J(s)}{C(s)}=C'(s)$, which is equivalent
to the property we just stated. This finishes the proof that the type of
the induction principle and computation rule is a mere proposition.

It remains to show that $(Y,\pi)=(Y',\pi')$, provided that $Y$ and $Y'$ are both
in $\mathcal{M}$, and that both sides satisfy
the induction principle and computation rule. It suffices to find an equivalence
$f:Y\to Y'$ such that $f\circ \pi=\pi'$.

From the induction principles of $Y$ resp. $Y'$, we obtain a function
$f:Y\to Y'$ with the property that $f\circ \pi=\pi'$, and a function
$f':Y'\to Y$ with the property that $f'\circ \pi'=\pi$.
To show that $f'\circ f=\idfunc$ we use the induction principle
of $Y$. Since the type $f'(f(y))=y$ is in $\mathcal{M}$, it suffices to show that
$f'(f(\pi(y)))=\pi(y)$. This readily follows from the defining properties of $f$
and $f'$. Similarly, we have $f\circ f'=\idfunc$.

A higher modality is a uniquely eliminating modality, with the
same modal types.

Let $\modal$ be a modality with modal units $\modalunit[A]$. Our goal is to show
that the pre-composition map

\begin{equation*}
\lam{s}s\circ\modalunit[A]:(\prd{z:\modal A}\modal(P(z)))\to(\prd{a:A}\modal(P(\modalunit[A](a))))
\end{equation*}

is an equivalence for each $A:\UU$ and $P:\modal A\to\UU$.
By the given induction principle and computation rule, we obtain a
right inverse $\mathsf{ind}^\modal_A$ of $\blank\circ\modalunit[A]$.

To show that it is a left inverse, consider $s:\prd{z:\modal A}\modal(P(z))$.
We need to find a homotopy

\begin{equation*}
\prd{z:\modal A}\id{s(z)}{\mathsf{ind}^\modal_A(s\circ \modalunit_A)(z)}.
\end{equation*}

By assumption we have that $P(x)$ is
modal for each $z:\modal A$ and hence it follows that $\id{s(x)}{\mathsf{ind}^\modal_A(s\circ \modalunit_A)(x)}$
is modal for each $x$. Hence it suffices to find a function of type

\begin{equation*}
\prd{a:A}\id{s(\modalunit_A(a))}{\mathsf{ind}^\modal_A(s\circ \modalunit_A)(\modalunit_A(a))}.
\end{equation*}

This follows straight from the computation rule of higher modalities.

§.§ Uniquely eliminating modalities

Next, we show that a uniquely eliminating modality is determined by its modal types, and gives rise to a $\Sigma$-closed reflective subuniverse.

Given a uniquely eliminating modality, $\modal X$ is modal for any type $X$.

Using the elimination principle of $\modal \modal X$, we find a function
$f:\modal \modal X\to\modal X$ and an identification $f\circ\modalunit[\modal X]=\idfunc[\modal X]$.
By uniqueness, the function

\[ (\modal \modal X\to\modal \modal X) \to (\modal X\to\modal \modal X) \]

is an equivalence, and hence its fiber over $\modalunit[\modal X]$:

\begin{equation*}
\sm{g:\modal \modal X\to\modal \modal X} g\circ\modalunit[\modal X]=\modalunit[\modal X]
\end{equation*}

is contractible. Since both $\idfunc[\modal \modal X]$ and $\modalunit[\modal X]\circ f$
are in this type (with suitable identifications), we find that $f$ is also the
right inverse of $\modalunit[\modal X]$. This shows that $\modalunit[\modal X]$ is an
equivalence, so $\modal X$ is modal.

The data of two uniquely eliminating modalities $\modal$ and $\modal'$ are equivalent if and only if both have the same modal types.

We need to show that the type of uniquely eliminating modalities
with a given class $\mathcal{M}:\UU\to\prop$ of modal types
is a mere proposition. Since the types of the form $\modal X$ are modal,
it suffices to show that for any class $\mathcal{M}
:\UU\to\prop$ and any type $X$, the type of tuples $(Y,p,\pi,H)$ is a mere proposition, where:

* $Y:\UU$.

* $p:\mathcal{M}(Y)$.

* $\pi:X\to Y$.

* For each $P$, $H_P$ witnesses that the function

\begin{equation*}
(\lam{s}s\circ \pi):(\prd{y:Y}\modal(P(y)))\to(\prd{x:X}\modal(P(\pi(x))))
\end{equation*}

is an equivalence.

Let $(Y,p,\pi,H)$ and $(Y',p',\pi',H')$ be such tuples. To show that they are
equal, it suffices to show that $(Y,\pi)=(Y',\pi')$ because the other things
in the list are terms of mere propositions. Furthermore, showing that
$(Y,\pi)=(Y',\pi')$ is equivalent to finding an equivalence $f:\eqv{Y}{Y'}$ with
the property that $f\circ\pi=\pi'$. By $H$, there is such a function, and by
$H'$ there is a function $f':Y'\to Y$ such that $f'\circ\pi'=\pi$. Now the
uniqueness gives that $f'\circ f$ is the only function from $Y$ to $Y$ such
that $f'\circ f\circ\pi=\pi$ and of course $\idfunc[Y]$ is another such function.
Therefore it follows that $f'\circ f=\idfunc$, and similarly it follows that
$f\circ f'=\idfunc$.

Any uniquely eliminating modality determines a $\Sigma$-closed reflective
subuniverse with the same modal types.

It is immediate from the definition of uniquely eliminating modalities
that every map $f:A\to B$ into a modal type $B$ has a homotopy unique extension to $\modal A$
along the modal unit:

\begin{equation*}
\begin{tikzcd}
A \arrow[dr,"f"] \arrow[d,swap,"\modalunit_A"] \\ \modal A \arrow[r,densely dotted,swap,"\tilde f"] & B.
\end{tikzcd}
\end{equation*}

Since the types of the form $\modal X$ are modal, we obtain a reflective subuniverse.
It remains to verify  that the type $\sm{z:\modal X}\modal(P(z))$ is modal for
any type $X$ and $P:X\to\UU$. We have the function

\begin{equation*}
\varphi\defeq\lam{m}\pairr{f(m),g(m)}:\modal(\sm{z:\modal X}\modal(P(z)))\to\sm{z:\modal X}\modal(P(z)),
\end{equation*}

f     (xu x)        : (z:X(P(z)))→X

g     (xu u)        : w:(z:X(P(z))) (P(f(w))).

Our goal is to show that $\varphi$ is an inverse to the modal unit.

Note that

\begin{equation*}
\varphi(\modalunit(x,y)) \jdeq \pairr{f(\modalunit(x,y)),g(\modalunit(x,y))} \jdeq \pairr{x,y},
\end{equation*}

so we see immediately that $\varphi$ is a left inverse of $\modalunit$.

To show that $\varphi$ is a right inverse of $\modalunit$, note that the type
of functions $h$ fitting in a commuting triangle of the fom

\begin{equation*}
\begin{tikzcd}[column sep=-3em]
\modal(\sm{z:\modal X}\modal(P(z))) \arrow[rr,densely dotted,"h"] & & \modal(\sm{z:\modal X}\modal(P(z))) \\
\phantom{\modal(\sm{z:\modal X}\modal(P(z)))} & \sm{z:\modal X}\modal(P(z)) \arrow[ul,"\modalunit"] \arrow[ur,swap,"\modalunit"] & \phantom{\modal(\sm{z:\modal X}\modal(P(z)))}
\end{tikzcd}
\end{equation*}

is a fiber over $\modalunit$ of a precomposition equivalence, and hence contractible.
Since this type also contains the identity function, it suffices
to show that $(\modalunit\circ\varphi)\circ\modalunit=\modalunit$; but this follows
from the fact that $\varphi$ is a left inverse of the modal unit.

§.§ Σ-closed reflective subuniverses

Now we study reflective subuniverses in a bit more detail, and end by
showing that $\Sigma$-closed ones give rise to stable factorization
systems. $\Sigma$-closure is used in <ref> to
show that left maps and right maps are closed under composition.

§.§.§ Properties of reflective subuniverses

For any $\mathcal{M}:\UU\to\prop$ and any type $X$, the type of triples $(Y,f,I)$ consisting of

* $Y:\UU_{\mathcal{M}}$,

* $f:X\to Y$, and

* $I:\prd{Z:\UU_{\mathcal{M}}}\isequiv(\lam{g}g\circ f:(Y\to Z)\to(X\to Z))$

is a mere proposition.

Consider $(Y,f,I)$ and $(Y',f',I')$ of the described type. Since $I$ and $I'$
are terms of a mere proposition, it suffices to show that $(Y,f)=(Y',f')$. In
other words, we have to find an equivalence $g:Y\to Y'$ such that $g\circ f'=f$.

By $I(Y')$, the type of
pairs $(g,h)$ consisting of a function $g:Y\to Y'$ such that $h:g\circ f=f'$ is contractible. By
$I'(Y)$, the type of pairs $(g',h')$ consisting of a function $g':Y'\to Y$
such that $h':g'\circ f'=f$ is contractible.

Now $g'\circ g$ is a function such that $g'\circ g\circ f=g'\circ f'=f$, as
is $\idfunc[Y]$. By contractibility, it follows that $g'\circ g=\idfunc[Y]$.
Similarly, $g\circ g'=\idfunc[Y']$.

The data of any two reflective subuniverses with the same modal types are the same.

Given the modal types, the rest of the data of a reflective subuniverse consists of, for each type $X$, a triple $(Y,f,I)$ as in <ref>.
Thus, by <ref>, these data form a mere proposition.

Given a reflective subuniverse, a type $X$ is modal if and only if $\modalunit[X]$ is an equivalence.

Certainly if $\modalunit[X]$ is an equivalence, then $X$ is modal since it is equivalent to the modal type $\modal X$.
Conversely, if $X$ is modal then we have a triple $(X,\idfunc[X],\nameless)$ inhabiting the type from <ref>, which also contains $(\modal X,\modalunit[X],\nameless)$.
Since this type is a mere proposition, these two elements are equal; hence $\modalunit[X]$ is, like $\idfunc[X]$, an equivalence.

Given a reflective subuniverse, if a modal unit $\modalunit[X]$ has a left inverse (i.e. a retraction), then it is an equivalence, and hence $X$ is modal.

Suppose $f$ is a left inverse of $\modalunit[X]$, i.e. $f\circ \modalunit[X] = \idfunc[X]$.
Then $\modalunit[X]\circ f\circ \modalunit[X] = \modalunit[X]$, so $\modalunit[X]\circ f$ is a factorization of $\modalunit[X]$ through itself.
By uniqueness of such factorizations, $\modalunit[X]\circ f = \idfunc[\modal X]$.
Thus $f$ is also a right inverse of $\modalunit[X]$, hence $\modalunit[X]$ is an equivalence.

In the following lemma we show that any reflective subuniverse is a `a functor up to homotopy', i.e. that the localization operation has an action on morphisms which preserves composition and identities.

Given $f:A\to B$ we have an induced map $\modal f : \modal A \to \modal B$, preserving identities and composition up to homotopy.
Moreover, for any $f$ the naturality square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f"] \arrow[d,swap,"\modalunit"] & B \arrow[d,"\modalunit"] \\
\modal A \arrow[r,swap,"\modal f"] & \modal B
\end{tikzcd}
\end{equation*}

Define $\modal f$ to be the unique function such that $\modal f \circ \modalunit[A] = \modalunit[B] \circ f$, using the universal property of $\modalunit[A]$.
The rest is easy to check using further universal properties.

Given a reflective subuniverse and any type $X$, the map $\modal \modalunit[X] : \modal X \to \modal\modal X$ is an equivalence.

By naturality, we have $\modal \modalunit[X] \circ \modalunit[X] = \modalunit[\modal X] \circ \modalunit[X]$.
Hence $\modal \modalunit[X] = \modalunit[\modal X]$ by the universal property of $\modalunit[X]$, but $\modalunit[\modal X]$ is an equivalence by <ref>.

Given a reflective subuniverse, a type $X$ is modal if and only if $(\blank \circ f) : (B\to X) \to (A\to X)$ is an equivalence for any function $f:A\to B$ such that $\modal f$ is an equivalence.

If $\modal f$ is an equivalence and $X$ is modal, then by the universal property of $\modalunit$, we have a commutative square

\[
\begin{tikzcd}
(B\to X) \ar[r,"\blank\circ f"] & (A\to X) \\
(\modal B\to X) \ar[r,"\blank\circ\modal f"'] \ar[u,"{\blank\circ \modalunit[B]}"] &
(\modal A \to X) \ar[u,"{\blank\circ \modalunit[A]}"']
\end{tikzcd}
\]

in which all but the top map are equivalences; thus so is the top map.

Conversely, since $\modal\modalunit[X]$ is an equivalence, the hypothesis implies that
$(\blank \circ \modalunit[X]) : (\modal X\to X) \to (X\to X)$
is an equivalence.
In particular, its fiber over $\idfunc[X]$ is inhabited, i.e. $\modalunit[X]$ has a retraction; hence $X$ is modal.

Consider a reflective subuniverse with modal operator $\modal$, and let $P:X\to\UU$ for some type $X:\UU$.
Then the unique map for which the triangle

\begin{equation*}
\begin{tikzcd}
\sm{x:X}P(x) \arrow[d,swap,"\modalunit"] \arrow[dr,"{\lam{\pairr{x,y}}\modalunit(x,\modalunit(y))}"] \\
\modal(\sm{x:X}P(x)) \arrow[r,densely dotted] & \modal(\sm{x:X}\modal(P(x)))
\end{tikzcd}
\end{equation*}

commutes, is an equivalence.

Since both codomains are modal, it suffices to show that ${\lam{\pairr{x,y}}\modalunit(x,\modalunit(y))}$ has the universal property of $\modalunit[\sm{x:X}P(x)]$, i.e. that any map $(\sm{x:X}P(x)) \to Y$, where $Y$ is modal, extends uniquely to $\modal(\sm{x:X}\modal(P(x)))$.
But we have

\begin{align*}
((\sm{x:X}P(x)) \to Y)
\prd{x:X} P(x) \to Y\\
\prd{x:X} \modal(P(x)) \to Y\\
(\sm{x:X}\modal(P(x))) \to Y\\
\modal (\sm{x:X}\modal(P(x))) \to Y
\end{align*}

and it is easy to see that this is the desired precomposition map.

For any reflective subuniverse, if $X$ is modal, then so is the identity type $x=y$ for any $x,y:X$.

Let $X$ be a modal type, and let $x,y:X$. We have a map
$\modal(x=y)\to\unit$. The outer square in the diagram

\begin{equation*}
\begin{tikzcd}
\modal(x=y) \arrow[ddr,bend right=15] \arrow[drr,bend left=15] \\
& (x=y) \arrow[r] \arrow[d] \arrow[ul,"\modalunit"] \arrow[dr, phantom, "\lrcorner", very near start] & \unit \arrow[d,"x"] \\
& \unit \arrow[r,swap,"y"] & X
\end{tikzcd}
\end{equation*}

commutes, because both maps extend the map $(x=y)\to X$ along $\modalunit$, and
such extensions are unique because $X$ is assumed to be modal.
Hence the universal property of the pullback gives
a left inverse of $\modalunit:(x=y)\to\modal(x=y)$, so by <ref> $(x=y)$ is modal.

Given a reflective subuniverse,
if $P(x)$ is modal for all $x:X$, then so is $\prd{x:X}P(x)$.

By <ref>, it suffices to define a left inverse of the modal unit
$\modalunit:(\prd{x:A}P(x))\to \modal(\prd{x:A}P(x))$. By the universal property
of dependent product, extending

\begin{equation*}
\begin{tikzcd}
\prd{x:A}P(x) \arrow[r,"{\idfunc}"] \arrow[d,"\modalunit"] & \prd{a:A}P(a) \arrow[d,"{\psi\,\defeq\,\lam{f}{a}\modalunit[P(a)](f(a))}"] \\
\modal(\prd{x:A}P(x)) \arrow[r,densely dotted] & \prd{a:A}\modal(P(a))
\end{tikzcd}
\end{equation*}

is equivalent to extending

\begin{equation*}
\begin{tikzcd}[column sep=large]
\prd{x:A}P(x) \arrow[r,"{\mathsf{ev}_a}"] \arrow[d,swap,"{\modalunit}"]
& P(a) \arrow[d,"{\modalunit}"] \\
\modal(\prd{x:A}P(x)) \arrow[r,densely dotted,swap,"{\modal(\mathsf{ev}_a)}"] & \modal(P(a))
\end{tikzcd}
\end{equation*}

for any $a:A$. Thus, we find

\begin{equation*}
\end{equation*}

as the solution to the first extension problem. In the first extension problem,
the function $\psi$ is an equivalence by the assumption that each $P(a)$ is
modal, so we obtain a retraction of the modal unit.

Taking $X=\unit+\unit$, so that $P:X\to\UU$ is just a pair of types, we conclude that if $A$ and $B$ are modal then so is $A\times B$.
Moreover, we have:

Given any reflective subuniverse, the modal operator $\modal$ preserves finite cartesian products (including the unit type).

In the nullary case, the statement is that the unit type $\unit$ is modal, which follows directly from <ref>.
In the binary case, we have to show that the modal extension

\begin{equation*}
\begin{tikzcd}
X\times Y \arrow[d,swap,"{\modalunit[X\times Y]}"] \arrow[dr,"\lam{\pairr{x,y}}\pairr{\modalunit[X](x),\modalunit[Y](y)}"] \\
\modal(X\times Y) \arrow[r,densely dotted] & \modal X\times\modal Y
\end{tikzcd}
\end{equation*}

is an equivalence.
But $(\modal(X\times Y),\modalunit[X\times Y],\nameless)$ inhabits the type from <ref>, so if we can show that $(\modal X\times \modal Y,\lam{\pairr{x,y}}\pairr{\modalunit[X](x),\modalunit[Y](y)})$ also extends to an inhabitant of that type, then they will be equal, inducing an equivalence that by uniqueness must be the map above.
To show this, first note that $\modal X\times \modal Y$ is modal, as remarked above.
And for any modal type $Z$ we have

\begin{align*}
(X\times Y \to Z)
&\eqvsym X\to (Y\to Z)\\
&\eqvsym X\to (\modal Y\to Z)\\
&\eqvsym \modal X\to (\modal Y\to Z)\\
&\eqvsym \modal X\times \modal Y\to Z
\end{align*}

given by precomposition as desired.
Here in the penultimate step we use the fact that the function type $\modal Y\to Z$ is modal since $Z$ is, by <ref>.

Given any reflective subuniverse, the modal operator preserves mere propositions.

A type $P$ is a mere proposition if and only if the diagonal $P\to P\times P$ is an equivalence.
The result then follows from <ref>.

By contrast, even modalities do not generally preserve $n$-types for any $n\ge 0$.
For instance, the “shape” modality of [38] takes the topological circle, which is a 0-type, to the homotopical circle, which is a 1-type, and the topological 2-sphere, which is also a 0-type, to the homotopical 2-sphere, which is (conjecturally) not an $n$-type for any finite $n$.
However, we will see in <ref> that lex modalities do preserve $n$-types for all $n$.

The basic properties of types and maps in homotopy type theory, such as being contractible, being a proposition, being an $n$-type, being an equivalence, and so on, are all constructed (perhaps inductively) out of identity types and $\Sigma$- and $\Pi$-types.
Thus, a $\Sigma$-closed reflective subuniverse is closed under them as well.
That is, if $A$ and $B$ are modal and $f:A\to B$, then the propositions “$A$ is contractible”, “$A$ is an $n$-type”, “$f$ is an equivalence”, and so on, are all modal as well.

§.§.§ $\Sigma$-closed reflective subuniverses

Let $\mathcal{M}:\UU\to\prop$ be a reflective subuniverse with modal
operator $\modal$. We say
that a type $X$ is $\modal$-connected if $\modal X$ is contractible,
and we say that a function $f:X\to Y$ is $\modal$-connected if each
of its fibers is. Similarly, we say that $f$ is modal if each of its
fibers is.

Note that a type $X$ is modal or $\modal$-connected just when the map $X\to\unit$ is.

Recall from <ref> that the open modality associated to a proposition $Q$ is defined by $\open Q(A) \defeq (Q\to A)$.
We claim that $A$ is $\open Q$-connected if and only if $Q \to\iscontr(A)$.
In other words, $(Q \to\iscontr(A))\eqvsym \iscontr(Q\to A)$.
For on the one hand, if $Q\to \iscontr(A)$, then $Q\to A$; while any two $f,g:Q\to A$ can be shown equal by function extensionality, since if $Q$ then $A$ is contractible.
But on the other hand, if $\iscontr(Q\to A)$ and $Q$, then $\eqv{(Q\to A)}{A}$, hence $\iscontr(A)$.

Note that $Q \to\iscontr(A)$ is also the defining condition for the $\closed Q$-modal types from <ref>.
That is, the $\open Q$-connected types coincide with the $\closed Q$-modal types.
We will come back to this relationship in <ref>.

The following theorem combines Lemma 7.5.7 and Theorem 7.7.4 of [40].

Given a reflective universe with modal operator $\modal$,
the following are equivalent:

* It is $\Sigma$-closed.

* It is uniquely eliminating.

* The modal units are $\modal$-connected.

To show <ref>$\Leftrightarrow$<ref>, let $Y$ be modal and $P:Y \to UU_\modal$, and consider for any $X$ the following commuting square:

\begin{equation*}
\begin{tikzcd}
\Big(\modal X \to \sm{y:Y}P(y)\Big) \arrow[r] \arrow[d] & \Big(X \to \sm{y:Y}P(y)\Big) \arrow[d] \\
\sm{g:\modal X\to Y}\prd{z:\modal X}P(g(z)) \arrow[r] & \sm{f:X\to Y}\prd{x:X}P(f(x))
\end{tikzcd}
\end{equation*}

The vertical maps are equivalences, so for any $X,Y,P$ the top map is an equivalence if and only if the bottom is.

If <ref> holds, the top map is an equivalence for all $X,Y,P$.
But the converse is also true, since we can take $X \defeq \sm{y:Y}P(y)$ to obtain a retraction for its unit.

The bottom map is induced by the map $(\modal X\to Y) \to (X\to Y)$, which is an equivalence since $Y$ is modal, and the family of maps

\[\Big(\prd{z:\modal X} P(g(z))\Big) \to \Big(\prd{x:X} P(g(\modalunit[X](x)))\Big) \]

for all $g:\modal X\to Y$; thus it is an equivalence just when each of these maps is.
If <ref> holds, then this is true for all $X,Y,P,g$.
But the converse is also true, since we can take $Y \defeq \modal X$ and $g\defeq \idfunc[\modal X]$.
This completes the proof of <ref>$\Leftrightarrow$<ref>.

To show <ref>$\Rightarrow$<ref>, we want a term of type

\begin{equation*}
\prd{z:\modal X}\iscontr(\modal(\hfib{\modalunit}{z})).
\end{equation*}

Using the dependent eliminators, it is easy to find a term
$s:\prd{z:\modal X}\modal(\hfib{\modalunit}{z})$ with the property that
$s\circ\modalunit(x)=\modalunit(x,\refl{\modalunit(x)})$. Now we need to show

\begin{equation*}
\prd{z:\modal X}{w:\modal(\hfib{\modalunit}{z})}w=s(z).
\end{equation*}

Since the type $w=s(z)$ is modal, this is equivalent to

\begin{equation*}
\prd{z:\modal X}{x:X}{p:\modalunit(x)=z} \modalunit(x,p)=s(z).
\end{equation*}

Moreover, the type $\sm{z:\modal X}\modalunit(x)=z$ is contractible, so this
is equivalent to

\begin{equation*}
\prd{x:X} \modalunit(x,\refl{\modalunit(x)})=s(\modalunit(x)),
\end{equation*}

of which we have a term by the defining property of $s$.

Finally, to show <ref>$\Rightarrow$<ref> we show that for any $\modal$-connected map $f:X\to Y$ and any family $P:Y \to \UU_\modal$ of modal types of $Y$, the precomposition map

\begin{equation*}
\Big(\prd{y:Y}P(y)\Big)\to \Big(\prd{x:X}P(f(x))\Big)
\end{equation*}

is an equivalence. This is because we have a commuting square

\begin{equation*}
\begin{tikzcd}
\prd{y:Y}\Big(\modal(\hfib{f}{y})\to P(y)\Big) \arrow[r] \arrow[d] & \prd{y:Y}\Big(\hfib{f}{y}\to P(y)\Big) \arrow[d] \\
\prd{y:Y}P(y) \arrow[r] & \prd{x:X}P(f(x))
\end{tikzcd}
\end{equation*}

In this square the map on the left is an equivalence by the contractibility of $\modal(\hfib{f}{y})$; the map on the right is an equivalence by the dependent universal property of identity types; and the top map is an equivalence by the universal property of modalities. Therefore the bottom map is an equivalence.

Given $f:A\to B$ and $g:B\to C$ and a reflective subuniverse $\modal$, if $f$ is $\modal$-connected, then $g$ is $\modal$-connected if and only if $g\circ f$ is $\modal$-connected.
That is, $\modal$-connected maps are closed under composition and right cancellable.

Recall that for $f:X\to Y$ and $g:Y\to Z$, one has $\hfib{g\circ f}{z}=\sm{p:\hfib{g}{z}}\hfib{f}{\proj1(p)}$.
Thus, for any $z:C$ we have

\begin{align*}
\modal(\hfib{g\circ f}{z})
& \eqvsym
\modal(\sm{p:\hfib{g}{z}}\hfib{f}{\proj1(p)}) \\
& \eqvsym
\modal(\sm{p:\hfib{g}{z}}\modal(\hfib{f}{\proj1(p)}))
\qquad \text{(by \cref{lem:sum_idempotent})}\\
& \eqvsym
\modal(\sm{p:\hfib{g}{z}}\unit) \\
& \eqvsym
\modal\hfib{g}{z}
\end{align*}

using the fact that $f$ is $\modal$-connected.
Thus, one is contractible if and only if the other is.

In general it is not true that if $g$ and $g\circ f$ are $\modal$-connected then $f$ is; this is one of the equivalent characterizations of lex modalities (<ref>).

A $\Sigma$-closed reflective subuniverse determines a stable orthogonal factorization system with the same
modal types.

Define $\mathcal{L}$ to be the class of $\modal$-connected
maps and $\mathcal{R}$ to be the the class of modal maps.
We first show that both $\mathcal{L}$ and $\mathcal{R}$ are closed under
Since $\hfib{g\circ f}{z}=\sm{p:\hfib{g}{z}}\hfib{f}{\proj1(p)}$, by $\Sigma$-closedness if $f$ and $g$ are both in $\mathcal{R}$ then so is $g\circ f$.
Thus $\cR$ is closed under composition; while <ref> implies that $\cL$ is closed under composition.
And since the fibers of an identity map are contractible, and contractible types are both modal and $\modal$-connected, both $\mathcal{L}$ and $\mathcal{R}$ contain all identities.

To obtain a factorization system,
it remains to show that the type of
$(\mathcal{L},\mathcal{R})$-factorizations of any function $f:X\to Y$ is contractible.
\[\pairr{X,f}=_{(\sm{Z:\UU} Z\to Y)} \pairr{\sm{y:Y}\hfib{f}{y},\proj1},\]
it is sufficient to
show that $\fact_{\mathcal{L},\mathcal{R}}(\proj1)$ is contractible for any
$\proj1:\sm{y:Y}P(y)\to Y$. But $\proj1$ factors as

\begin{equation*}
\begin{tikzcd}
\sm{y:Y}P(y) \arrow[r,"p_\mathcal{L}"] & \sm{y:Y}\modal(P(y)) \arrow[r,"p_\mathcal{R}"] & Y
\end{tikzcd}
\end{equation*}

where $p_\mathcal{L}\defeq\total{\modalunit[P(\blank)]}$ and $p_\mathcal{R}\defeq\proj1$.
The fibers of $p_\mathcal{R}$ are $\modal(P(\blank))$, so it follows
immediately that $p_\mathcal{R}$ is in $\mathcal{R}$.
Moreover, since
$\eqv{\hfib{\total{\modalunit}}{\pairr{y,u}}}{\hfib{\modalunit[P(y)]}{u}}$ and each $\modalunit$ is $\modal$-connected, it follows that $p_\mathcal{L}$ is in

Now consider any other factorization $(I,g,h,H)$ of $\proj1$ into
an $\cL$-map $g:(\sm{y:Y}P(y))\to I$ followed by an $\cR$-map $h:I\to Y$. Since
$I=\sm{y:Y}\hfib{h}{y}$, we have a commuting square

\begin{equation*}
\begin{tikzcd}
\sm{y:Y}P(y) \arrow[r,"g"] \arrow[d,swap,"{\total{\gamma}}"]
& I \arrow[d,"h"] \\
\sm{y:Y}\hfib{h}{y} \arrow[ur,equals] \arrow[r,swap,"\proj1"] & Y
\end{tikzcd}
\end{equation*}

in which $\gamma(y,u)\defeq \pairr{g(y,u),H(y,u)}$.
It follows that

\[(I,g,h,H)=\left(\tsm{y:Y}\hfib{h}{y},\total{\gamma},\proj1,\nameless\right).\]

Thus it suffices to show that there is a commuting triangle

\begin{equation*}
\begin{tikzcd}[column sep=0]
\phantom{\hfib{h}{y}} & P(y) \arrow[dl,swap,"\modalunit"] \arrow[dr,"{\gamma_y}"] & \phantom{\modal(P(y))} \\
\modal(P(y)) \arrow[rr,equals] & & \hfib{h}{y}
\end{tikzcd}
\end{equation*}

for all $y:Y$.
We will do this using <ref>, by showing that $\gamma_y$ has the same universal property as $\modalunit[P(y)]$.
This follows from the following calculation:

\begin{align*}
(\hfib{h}{y}\to Z) & \eqvsym ((\sm{w:\hfib{h}{y}}\modal(\hfib{g}{\proj1(w)}))\to Z) \\
& \eqvsym ((\sm{w:\hfib{h}{y}}\hfib{g}{\proj1(w)})\to Z) \\
& \eqvsym (\hfib{h\circ g}{y}\to Z) \\
& \eqvsym (P(y)\to Z),
\end{align*}

which we can verify is given by precomposition with $\gamma_y$.

It remains to show that our orthogonal factorization system is stable. Consider a pullback diagram

\begin{equation*}
\begin{tikzcd}
A' \arrow[d,swap,"k"] \arrow[r,"f"] & A \arrow[d,"l"] \\
B' \arrow[r,swap,"g"] & B
\end{tikzcd}
\end{equation*}

in which $l$ is in $\mathcal{L}$. By the pasting lemma for pullbacks, it
follows that $\hfib{k}{b}=\hfib{l}{g(b)}$ for each $b:B'$. Thus, it follows that
$k$ is in $\mathcal{L}$.

§.§.§ Connected maps

The $\modal$-connected maps introduced in <ref> have a number of other useful properties.
Most of these are stated in <cit.> for the special case of the $n$-truncation modality, but essentially the same proofs work for any modality.

In fact, most of these properties are true about an arbitrary reflective subuniverse, although a few of the proofs must be different.
Thus, for this subsection, let $\modal$ be a reflective subuniverse, not in general $\Sigma$-closed.

If $f : A \to B$ is $\modal$-connected, then it induces an equivalence
$\modal f : \eqv{\modal{A}}{\modal{B}}$.

To define an inverse $g:\modal B \to \modal A$, by the universal property of $\modal B$, it suffices to define a map $B\to \modal A$.
But given $b:B$, we have a map $\proj1 : \hfib{f}{b} \to A$, hence $\modal\proj1 : \modal \hfib{f}{b} \to \modal A$.
And $\modal \hfib{f}{b}$ is contractible since $f$ is $\modal$-connected, so it has a point $c_b$, and we define $g(\modalunit[B](b)) = \modal \proj1(c_b)$.

Now by the universal property of $\modal A$ and $\modal B$, it suffices to show that the composites $g\circ \modal f \circ \modalunit[A]$ and $\modal f\circ g \circ \modalunit[B]$ are equal to $\modalunit[A]$ and $\modalunit[B]$ respectively.
In the first case, for $a:A$ we have

\begin{align*}
g(\modal f(\modalunit[A](a)))
&= g(\modalunit[B](f(a)))\\
&= \modal \proj1(c_{f(a)})\\
&= \modal \proj1(\modalunit[\hfib f b](a,\refl{f(a)}))\\
&= \modalunit[A](\proj1(a,\refl{f(a)}))\\
&= \modalunit[A](a),
\end{align*}

using in the third line the fact that $\modal(\hfib f b)$ is contractible.
And in the second case, for $b:B$ we have

\begin{align*}
\modal f(g(\modalunit[B](b)))
&= \modal f(\modal \proj1(c_b))\\
&= \modal(f\circ \proj1)(c_b)\\
&= \modal(\lam{u:\hfib f b} b)(c_b)\\
&= \modal(\lam{u:\unit} b)(\modalunit[\unit](\ttt))\\
&= \modalunit[B](b)
\end{align*}

where in the last two lines we use the commutativity of the following diagram:

\[
\begin{tikzcd}
\hfib f b \ar[d] \ar[r] \ar[rr,bend left,"{\lam{u:\hfib f b} b}"] & \unit \ar[r,"b"] \ar[d,"{\modalunit[\unit]}"] \ar[dl,"{c_b}"] & B \ar[d,"{\modalunit[B]}"] \\
\modal(\hfib f b) \ar[r] \ar[rr,bend right,"{\modal (\lam{u:\hfib f b} b)}"'] & \modal \unit \ar[r] & \modal B
\end{tikzcd}
\]

and the fact that $\modal\unit$ is contractible.

The converse of <ref> is false in general, even for modalities; we will see in <ref> that it holds exactly when $\modal$ is lex.

Recall that $\modaltype$ denotes the universe of modal types.
Note that the projection $\proj1 : (\sm{x:A} P(x)) \to A$ is $\modal$-modal if and only if $P$ factors through $\modaltype$.
The following generalizes the unique elimination property of $\modalunit$ to arbitrary $\modal$-connected maps.

For $f:A\to B$ and $P:B\to\modaltype$, consider the following function:

\begin{equation*}
\lam{s} s\circ f :\Parens{\prd{b:B} P(b)}\to\Parens{\prd{a:A}P(f(a))}.
\end{equation*}

For a fixed $f$, the following are equivalent.

* $f$ is $\modal$-connected.

* For every $P:B\to \modaltype$, the map $\lam{s} s\circ f$ is an equivalence.

* For every $P:B\to \modaltype$, the map $\lam{s} s\circ f$ has a section.

First suppose $f$ is $\modal$-connected and let $P:B\to\modaltype$. Then:

\begin{align*}
\prd{b:B} P(b) & \eqvsym \prd{b:B} \Parens{\modal{\hfib{f}b} \to P(b)}
\tag{since $\modal{\hfib{f}b}$ is contractible}\\
& \eqvsym \prd{b:B} \Parens{\hfib{f}b\to P(b)}
\tag{since $P(b)$ is modal}\\
& \eqvsym \prd{b:B}{a:A}{p:f(a)= b} P(b)\\
& \eqvsym \prd{a:A} P(f(a))
\end{align*}

and the composite equivalence is indeed composition with $f$.
Thus, <ref>$\Rightarrow$<ref>, and clearly <ref>$\Rightarrow$<ref>.
To show <ref>$\Rightarrow$<ref>, let
$P(b)\defeq \modal{\hfib{f}b}$.
Then <ref> yields a map $c:\prd{b:B} \modal{\hfib{f}b}$ with
$c(f(a))=\modalunit{\pairr{a,\refl{f(a)}}}$. To show that each $\modal{\hfib{f}b}$ is contractible, we will show that $c(b)=w$ for any $b:B$ and $w:\modal{\hfib{f}b}$.
In other words, we must show that the identity function $\modal{\hfib{f}b} \to \modal{\hfib{f}b}$ is equal to the constant function at $c(b)$.
By the universal property of $\modal{\hfib{f}b}$, it suffices to show that they become equal when precomposed with $\modalunit[\hfib{f}b]$, i.e. we may assume that $w = \modalunit\pairr{a,p}$ for some $a:A$ and $p:f(a)=b$.
But now path induction on $p$ reduces our goal to the given $c(f(a))=\modalunit{\pairr{a,\refl{f(a)}}}$.

A type $A$ is $\modal$-connected if and only if the “constant functions” map
B \to (A\to B)
is an equivalence for every modal type $B$.

Dually, we will prove in <ref> that when $\modal$ is a modality, if this holds for all $\modal$-connected $A$ then $B$ is modal.

Let $B$ be a modal type and let $f:A\to B$ be a function.
If $f$ is $\modal$-connected, then the induced function $g:\modal A\to B$ is an equivalence; the converse holds if $\modal$ is $\Sigma$-closed.

By <ref>, if $f$ is $\modal$-connected then $\modal f$ is an equivalence.
But $g$ is the composite $\modalunit[B]^{-1}\circ \modal f$, hence also an equivalence.

Conversely, by <ref>, $\modalunit$ is $\modal$-connected.
Thus, since $f = g\circ \modalunit[A]$, if $g$ is an equivalence then $f$ is also $\modal$-connected.

Let $f:A\to B$ be a function and $P:A\to\type$ and $Q:B\to\type$ be type families. Suppose that $g:\prd{a:A} P(a)\to Q(f(a))$
is a family of $\modal$-connected functions.
If $f$ is also $\modal$-connected, then so is the function

\begin{align*}
\varphi &:\Parens{\sm{a:A} P(a)}\to\Parens{\sm{b:B} Q(b)}\\
\varphi(a,u) &\defeq \pairr{f(a),g_a(u)}.
\end{align*}

Conversely, if $\varphi$ and each $g_a$ are $\modal$-connected, and moreover $Q$ is fiberwise merely inhabited (i.e. we have $\brck{Q(b)}$ for all $b:B$), then $f$ is $\modal$-connected.

For any $b:B$ and $v:Q(b)$ we have

\begin{align*}
\modal{\hfib{\varphi}{\pairr{b,v}}} & \eqvsym \modal{\sm{a:A}{u:P(a)}{p:f(a)= b} \trans{p}{g_a(u)}= v}\\
& \eqvsym \modal{\sm{w:\hfib{f}b}{u:P(\proj1(w))} g_{\proj 1 w}(u)= \trans{\opp{\proj2(w)}}{v}}\\
& \eqvsym \modal{\sm{w:\hfib{f}b} \hfib{g(\proj1 w)}{\trans{\opp{\proj 2(w)}}{v}}}\\
& \eqvsym \modal{\sm{w:\hfib{f}b} \modal{\hfib{g(\proj1 w)}{\trans{\opp{\proj 2(w)}}{v}}}}\\
& \eqvsym \modal{\hfib{f}b}
\end{align*}

where the transportations along $f(p)$ and $f(p)^{-1}$ are with respect to $Q$, and we use <ref> on the penultimate line.
Therefore, if either of $\modal{\hfib{\varphi}{\pairr{b,v}}}$ or $\modal{\hfib{f}b}$ is contractible, so is the other.

In particular, if $f$ is $\modal$-connected, then $\modal{\hfib{f}b}$ is contractible for all $b:B$, and hence so is $\modal{\hfib{\varphi}{\pairr{b,v}}}$ for all $(b,v):\sm{b:B} Q(b)$.
On the other hand, if $\varphi$ is $\modal$-connected, then $\modal{\hfib{\varphi}{\pairr{b,v}}}$ is contractible for all $(b,v)$, hence so is $\modal{\hfib{f}b}$ for any $b:B$ such that there exists some $v:Q(b)$.
Finally, since contractibility is a mere proposition, it suffices to merely have such a $v$.

Let $P,Q:A\to\type$ be type families and $f:\prd{a:A} \Parens{P(a)\to Q(a)}$.
Then $\total f: \sm{a:A}P(a) \to \sm{a:A} Q(a)$ is $\modal$-connected if and only if each $f(a)$ is $\modal$-connected.

We have
$\hfib{\total f}{\pairr{x,v}}\eqvsym\hfib{f(x)}v$
for each $x:A$ and $v:Q(x)$. Hence $\modal{\hfib{\total f}{\pairr{x,v}}}$ is contractible if and only if
$\modal{\hfib{f(x)}v}$ is contractible.

Of course, the “if” direction of <ref> is a special case of <ref>.
This suggests a similar generalization of the “only if” direction of <ref>, which would be a version of <ref> asserting that if $f$ and $\varphi$ are $\modal$-connected then so is each $g_a$.
However, this is not true in general; we will see in <ref> that it holds if and only if the modality is lex.

Finally, we note that the $\modal$-modal and $\modal$-connected maps are classified.
More generally, we prove the following generalization of <cit.>.

Let $P:\UU\to\prop$ be a predicate on the universe, let $\UU_P\defeq
\sm{X:\UU}P(x)$ and $(\UU_P)_\bullet\defeq\sm{X:\UU_P}X$. The projection
$\proj1:(\UU_P)_\bullet\to\UU_P$ classifies the maps whose fibers satisfy $P$, in the sense that these are exactly the maps that occur as pullbacks of it.

The fiber of $\proj1:(\UU_P)_\bullet\to\UU_P$ over $X:\UU_P$ is $X$, which satisfies $P$ by definition.
Thus all fibers of this map satisfy $P$, hence so do all fibers of any of its pullbacks.

Conversely, let $f:Y\to X$ be any map into $X$. Then $\hfibfunc{f}:X\to\UU$ factors through
$\UU_P$ if and only if all the fibers of $f$ satisfy $P$. Let us write
$P(f)$ for $\prd{x:X}P(\hfib{f}{x})$. Then we see that the equivalence
$\chi$ of Theorem 4.8.3 of [40] restricts to an

\begin{equation*}
\chi^P:(\sm{Y:\UU}{f:Y\to X}P(f))\to(X\to\UU_P).
\end{equation*}

Now observe that the outer square and the square on the right in the diagram

\begin{equation*}
\begin{tikzcd}[column sep=6em]
Y \arrow[d,swap,"f"] \arrow[rr,"{\lam{y}\pairr{\hfib{f}{f(y)},\blank,\pairr{y,\refl{f(y)}}}}"] & & \pointed{(\UU_P)} \arrow[r] \arrow[d] & \pointed{\UU} \arrow[d] \\
X \arrow[rr,swap,"{\hfibfunc{f}}"] & & \UU_P \arrow[r] & \UU
\end{tikzcd}
\end{equation*}

are pullback squares. Hence the square on the left is a pullback square.

The $\modal$-modal maps are classified by the universe of $\modal$-modal types, and the $\modal$-connected maps are classified by the universe of $\modal$-connected types.

§.§ Stable orthogonal factorization systems

To complete <ref>, we will show that stable orthogonal factorization systems are also determined by their modal types, and give rise to higher modalities.

§.§.§ Orthogonal factorization systems

In classical category theory, orthogonal factorization systems are equivalently characterized by a unique lifting property.
We begin with the analogue of this in our context.

Let $(\mathcal{L},\mathcal{R})$ be an orthogonal factorization system, and
consider a commutative square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f"] \arrow[d,swap,"l"] \ar[dr,phantom,"\scriptstyle S"] & X \arrow[d,"r"] \\
B \arrow[r,swap,"g"] & Y
\end{tikzcd}
\end{equation*}

(i.e. paths $S : r\circ f = g\circ l$)
for which $l$ is in $\mathcal{L}$ and $r$ is in $\mathcal{R}$. We define
$\fillers S$ to be the type of diagonal fillers
of the above diagram, i.e. the type of tuples $(j,H_f,H_g,K)$ consisting of
$j:B\to X$, $H_f:j\circ l=f$ and $H_g:r\circ j=g$ and an equality $K : r\circ H_f = \ct S{(H_g \circ l)}$.

The equality $K$ is required because of homotopy coherence: the commutativity of the given square and of the two triangles are not mere propositions but data consisting of homotopies inhabiting those squares and triangles, so to actually have a “filler” in the homotopy coherent sense we need to know that the “pasting composite” of the two triangles is the given square.

Let $(\mathcal{L},\mathcal{R})$ be an orthogonal factorization system, and
consider a commutative square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f"] \arrow[d,swap,"l"] \ar[dr,phantom,"\scriptstyle S"] & X \arrow[d,"r"] \\
B \arrow[r,swap,"g"] & Y
\end{tikzcd}
\end{equation*}

for which $l$ is in $\mathcal{L}$ and $r$ is in $\mathcal{R}$. Then the type
$\fillers S$ of diagonal fillers is contractible.

By the fact that every morphism factors uniquely as a left map followed by a
right map, we may factorize $f$ and $g$ in $(\mathcal{L},\mathcal{R})$ as $H_f : f = f_\cR \circ f_\cL$ and $H_g : g = g_\cR \circ g_\cL$, obtaining the diagram

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f_{\mathcal{L}}"] \arrow[d,swap,"l"] & \im(f) \arrow[r,"f_{\mathcal{R}}"] & X \arrow[d,"r"] \\
B \arrow[r,swap,"g_{\mathcal{L}}"] & \im(g) \arrow[r,swap,"g_{\mathcal{R}}"] & Y.
\end{tikzcd}
\end{equation*}

Now both $(r\circ f_{\mathcal{R}})\circ f_{\mathcal{L}}$ and
$g_{\mathcal{R}}\circ(g_{\mathcal{L}}\circ l)$ are factorizations
of the same function $r\circ f:A\to Y$.
Since $\fact_{\mathcal{L},\mathcal{R}}(r\circ f)$ is contractible, so is its identity type

\[ (\im(f), f_\cL, r\circ f_\cR, r\circ H_f) = (\im(g), g_\cL \circ l, g_\cR, \ct{S}{(H_g\circ l)}). \]

This identity type is equivalent to

\begin{multline*}
\sm{e:\im(f) \simeq \im(g)}{H_\cL : g_\cL \circ l = e\circ f_\cL}{H_\cR : r\circ f_\cR = g_\cR\circ e}\\
(\ct{(r\circ H_f)}{(H_\cR \circ f_\cL)} = \ct S{\ct{(H_g \circ l)}{(g_\cR \circ H_\cL)}})
\end{multline*}

Now since $\fact_{\cL,\cR}(f)$ and $\fact_{\cL,\cR}(g)$ are also contractible, we can sum over them to get that the following type is contractible:

\begin{multline*}
\sm{\im(f):\UU}{f_\cL : A \to \im(f)}{f_\cR : \im(f) \to X}{H_f : f = f_\cR \circ f_\cL}\\
\sm{\im(g):\UU}{g_\cL : B \to \im(g)}{g_\cR : \im(g) \to Y}{H_g : g = g_\cR \circ g_\cL}\\
\sm{e:\im(f) \simeq \im(g)}{H_\cL : g_\cL \circ l = e\circ f_\cL}{H_\cR : r\circ f_\cR = g_\cR\circ e}\\
(\ct{(r\circ H_f)}{(H_\cR \circ f_\cL)} = \ct S{\ct{(H_g \circ l)}{(g_\cR \circ H_\cL)}})
\end{multline*}

(omitting the hypotheses that $f_\cL,g_\cL\in\cL$ and $f_\cR,g_\cR\in\cR$).
Reassociating and removing the contractible type $\sm{\im(g):\UU}(\im(f) \simeq \im(g))$, and renaming $\im(f)$ as simply $I$, this is equivalent to

\begin{multline*}
\sm{I:\UU}{f_\cL : A \to I}{f_\cR : I \to X}{H_f : f = f_\cR \circ f_\cL}\\
\sm{g_\cL : B \to I}{g_\cR : I \to Y}{H_g : g = g_\cR \circ g_\cL}{H_\cL : g_\cL \circ l = f_\cL}{H_\cR : r\circ f_\cR = g_\cR}\\
(\ct{(r\circ H_f)}{(H_\cR \circ f_\cL)} = \ct S{\ct{(H_g \circ l)}{(g_\cR \circ H_\cL)}})
\end{multline*}

Removing the contractible $\sm{f_\cL : A \to I} (g_\cL \circ l = f_\cL)$ and $\sm{g_\cR : I \to Y} (r\circ f_\cR = g_\cR)$, this becomes

\begin{multline*}
\sm{I:\UU}{f_\cR : I \to X}{g_\cL : B \to I}{H_f : f = f_\cR \circ g_\cL \circ l}{H_g : g = r\circ f_\cR \circ g_\cL}\\
(r\circ H_f = \ct S{(H_g \circ l)})
\end{multline*}

Inserting a contractible $\sm{j:B\to X} (f_\cR \circ g_\cL = j)$, and reassociating some more, we get

\begin{multline*}
\sm{j:B\to X}{I:\UU}{f_\cR : I \to X}{g_\cL : B \to I}{H_j:f_\cR \circ g_\cL = j}\\
\sm{H_f : f = f_\cR \circ g_\cL \circ l}{H_g : g = r\circ f_\cR \circ g_\cL}
(r\circ H_f = \ct S{(H_g \circ l)})
\end{multline*}

But now $\sm{I:\UU}{f_\cR : I \to X}{g_\cL : B \to I}{H_j:f_\cR \circ g_\cL = j}$ is just $\fact_{\cL,\cR}(j)$, hence contractible.
Removing it, we get

\begin{equation*}
\sm{j:B\to X}{H_f : f = j \circ l}{H_g : g = r\circ j}(r\circ H_f = \ct S{(H_g \circ l)})
\end{equation*}

which is just $\fillers S$.
Therefore, this is also contractible.

For any class $\mathcal{C}:\prd*{A,B:\UU}(A\to B)\to\prop$ of maps, we define

* $^{\bot}\mathcal{C}$ to be the class of maps with (unique) left lifting
property with respect to all maps in $\mathcal{C}$: the mere proposition
$({}^\bot\mathcal{C})(l)$ asserts that for every commutative square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f"] \arrow[d,swap,"l"] \ar[dr,phantom,"S"] & X \arrow[d,"r"] \\
B \arrow[r,swap,"g"] & Y
\end{tikzcd}
\end{equation*}

with $r$ in $\mathcal{C}$, the type $\fillers S$ of diagonal fillers is contractible.

* $\mathcal{C}^\bot$ to be the class of maps with the dual (unique) right lifting
property with respect to all maps in $\mathcal{C}$.

* $l\perp r$ to mean $r\in \{l\}^\perp$ (equivalently, $l\in {}^{\perp}\{r\}$).

In an orthogonal factorization system $(\mathcal{L},\mathcal{R})$, one has
$\mathcal{L}={^\bot\mathcal{R}}$ and $\mathcal{L}^\bot=\mathcal{R}$.

We first show that $\mathcal{L}={^\bot\mathcal{R}}$, i.e. we show that
$\mathcal{L}(f)\leftrightarrow {^\bot\mathcal{R}}(f)$ for any map $f$. Note
that the implication $\mathcal{L}(f)\to {^\bot\mathcal{R}}(f)$ follows from

Let $f:A\to B$ be a map in ${^\bot\mathcal{R}}$.
We wish to show that $\mathcal{L}(f)$. Consider the factorization
$(f_{\mathcal{L}},f_{\mathcal{R}})$ of $f$. Then the square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f_{\mathcal{L}}"] \arrow[d,swap,"f"] & \mathsf{im}_{\mathcal{L},\mathcal{R}}(f) \arrow[d,"f_{\mathcal{R}}"] \\
B \arrow[r,swap,"\idfunc"] & B
\end{tikzcd}
\end{equation*}

commutes. Since $f$ has the left lifting property, the type of diagonal fillers
of this square is contractible. Thus we have a section $j$ of $f_{\mathcal{R}}$.
The map $j\circ f_\mathcal{R}$ is then a diagonal filler of the square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f_{\mathcal{L}}"] \arrow[d,swap,"f_{\mathcal{L}}"] & \mathsf{im}_{\mathcal{L},\mathcal{R}}(f) \arrow[d,"f_{\mathcal{R}}"] \\
\mathsf{im}_{\mathcal{L},\mathcal{R}}(f) \arrow[r,swap,"f_{\mathcal{R}}"] & B.
\end{tikzcd}
\end{equation*}

Of course, the identity map $\idfunc[\mathsf{im}_{\mathcal{L},\mathcal{R}}(f)]$
is also a diagonal filler for this square, so the fact that the type of
such diagonal fillers is contractible implies that $j\circ f_{\mathcal{R}}=\idfunc$.
Thus, $j$ and $f_\cR$ are inverse equivalences, and so the pair $(B,f)$ is equal to the pair $(\mathsf{im}_{\mathcal{L},\mathcal{R}}(f),f_\cL)$.
Hence $f$, like $f_\cL$, is in $\cL$.

Similarly, <ref> also implies that $\mathcal{R}(f)\to \mathcal{L}^\bot(f)$
for any map $f$, while we can prove $\mathcal{L}^\bot(f)\to\mathcal{R}(f)$ analogously to ${^\bot\mathcal{R}}(f)\to\mathcal{L}(f)$.

The data of two orthogonal factorization systems $(\mathcal{L},\mathcal{R})$ and
$(\mathcal{L}',\mathcal{R}')$ are identical if and only if

“Only if” is obvious.
Conversely, if $\mathcal{R}=\mathcal{R}'$, then by <ref> we have $\cL = \cL'$, and the remaining data of an orthogonal factorization system is a mere proposition.

For each $l:X\to Y$ such that $\mathcal{L}(l)$ and each type $Z$, the function

\begin{equation*}
\lam{g} g\circ l: (\sm{g:Y\to Z}\mathcal{R}(g))\to(\sm{f:X\to Z}\mathcal{R}(f))
\end{equation*}

is a monomorphism. Also, for each $r:X\to Y$ such that $\mathcal{R}(r)$ and
each type $Z$, the function

\begin{equation*}
\lam{f} r\circ f : (\sm{f:Z\to X}\mathcal{L}(f))\to(\sm{g:Z\to Y}\mathcal{L}(g))
\end{equation*}

is a monomorphism.

We prove the first statement. Suppose $g,g':Y\to Z$ are two $\mathcal{R}$-maps
such that $H:g\circ l=f$ and $H':g'\circ l=f$. Then we obtain two  ...

From every orthogonal factorization system we obtain a reflective subcategory with the same modal types.

We define $P(A)$ to be the proposition that the unique map $A\to\unit$ is in
For any type $A$, there is a unique factorization

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"{\modalunit[A]}"] & \modal A \arrow[r] & \unit
\end{tikzcd}
\end{equation*}

of the unique map $A\to\unit$, where $\modalunit[A]$ is in $\mathcal{L}$. This
defines the operation $\modal$ and the modal units.

Now let $A:\UU$ and $B:\UU_P$, and consider $f:A\to B$. We have to show that
the type of extensions of $f$ along $\modalunit$ is contractible.
It is immediate that the type of such extensions is equivalent to the type
$\mathsf{fill}_{\mathcal{L},\mathcal{R}}(f,g)$ of diagonal fillers
of the square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"f"] \arrow[d,swap,"{\modalunit[A]}"] & B \arrow[d] \\
\modal A \arrow[r,swap,"g"] & \unit.
\end{tikzcd}
\end{equation*}

By <ref>, the assumption that $P(B)$ holds and the fact that $\modalunit[A]$ is
in $\mathcal{L}$, we know that this type of diagonal fillers is contractible.

Let $(\mathcal{L},\mathcal{R})$ be an orthogonal factorization system. Then
the class $\mathcal{R}$ is stable under pullbacks.

Consider a pullback diagram

\begin{equation*}
\begin{tikzcd}
A \arrow[d,swap,"k"] \arrow[r,"g"] & X \arrow[d,"h"] \\
B \arrow[r,swap,"f"] & Y
\end{tikzcd}
\end{equation*}

where $h:X\to Y$ is assumed to be in $\mathcal{R}$, and let $k=k_{\mathcal{R}}\circ k_\mathcal{L}$ be a factorization of $k$.
Then the outer rectangle in the diagram

\begin{equation*}
\begin{tikzcd}
A \arrow[r,equals] \arrow[d,swap,"k_{\mathcal{L}}"] & A \arrow[d,swap,"k"] \arrow[r,"g"] & X \arrow[d,"h"] \\
\im_{\mathcal{L},\mathcal{R}}(k) \arrow[r,swap,"k_{\mathcal{R}}"] & B \arrow[r,swap,"f"] & Y
\end{tikzcd}
\end{equation*}

commutes, so by <ref> there is a diagonal lift $j:\im_{\mathcal{L},\mathcal{R}}(k)\to X$ with $i \circ k_{\cL} = g$ and $h\circ i = f \circ k_{\cR}$.
Then by the universal property of pullbacks, we obtain a map $j:\im_{\mathcal{L},\mathcal{R}}(k)\to A$ with $g\circ j = i$ and $k\circ j=k_{\mathcal{R}}$.
And since $g\circ j \circ k_{\cL} = i\circ k_{\cL} = g$ and $k\circ j\circ k_{\cL} = k_{\cR}\circ k_{\cL} = k$ (by homotopies coherent with the pullback square), the uniqueness aspect of the pullback gives $j\circ k_{\mathcal{L}}=\idfunc$.

It suffices to show that $k_{\mathcal{L}}$ is an equivalence, and since we already have that $j\circ k_{\mathcal{L}}=\idfunc$ we only need to show that $k_{\mathcal{L}}\circ j=\idfunc$.
We do this using the contractibility of the type of diagonal fillers. Consider the square

\begin{equation*}
\begin{tikzcd}
A \arrow[r,"k_{\mathcal{L}}"] \arrow[d,swap,"k_{\mathcal{L}}"] & \im_{\mathcal{L},\mathcal{R}}(k) \arrow[d,"k_{\mathcal{R}}"] \\
\im_{\mathcal{L},\mathcal{R}}(k) \arrow[r,swap,"k_{\mathcal{R}}"] & B,
\end{tikzcd}
\end{equation*}

for which $\idfunc:\im_{\mathcal{L},\mathcal{R}}(k)\to \im_{\mathcal{L},\mathcal{R}}(k)$ (with the trivial homotopies) is a diagonal filler. However, we also have the homotopies $k_{\mathcal{L}}\circ j\circ k_{\mathcal{L}} \htpy k_{\mathcal{L}}$ and $k_{\mathcal{R}}\circ k_{\mathcal{L}}\circ j\htpy k\circ j\htpy k_{\mathcal{R}}$. This shows that we have a second diagonal filler, of which the underlying map is $k_{\mathcal{L}}\circ j$. Since the type of diagonal fillers is contractible, it follows that $k_{\mathcal{L}}\circ j=\idfunc$, as desired.

§.§.§ Stable orthogonal factorization systems

Given $l,r,f,g$ and a homotopy $S : r \circ f = g  \circ l$, consider as $b:B$ varies all the diagrams of the form

\begin{equation*}
\begin{tikzcd}
\hfib{l}{b} \arrow[r,"\proj1"] \arrow[d,"!"'] & A \arrow[d,swap,"l"] \arrow[r,"f"] \ar[dr,phantom,"S"] & X \arrow[d,"r"] \\
\unit \arrow[r,swap,"b"] & B \arrow[r,swap,"g"] & Y
\end{tikzcd}
\end{equation*}

and write $S_b : r \circ (f \circ \proj1) = (g\circ b) \circ \mathord !$ for the induced commutative square.
Then the map

\begin{equation*}
\fillers{S} \to \prd{b:B}\fillers{S_b},
\end{equation*}

defined by precomposition with $b$, is an equivalence.

The domain and codomain of the map in question are by definition

\[
\sm{j:B\to X}{H_f :j\circ l=f}{H_g:r\circ j=g} r\circ H_f = \ct{S}{(H_g\circ l)}
\]

\begin{equation*}
\prd{b:B}\sm{j_b:\unit\to X}{H_{f,b} : j_b\circ \mathord{!}=f\circ \proj1}{H_{g,b}: r\circ j_b=g\circ b} r\circ H_{f,b} = \ct{S_b}{(H_{g,b}\circ \mathord!)}.
\end{equation*}

The latter is equivalent (using function extensionality and contractibility of $\unit$) to

\begin{multline*}
\prd{b:B}\sm{j_b:X}{H_{f,b} : \prd{u:\hfib l b} j_b=f(\proj1(u))}{H_{g,b}: r(j_b)=g(b)}\\
\prd{u:\hfib l b} r(H_{f,b}(u)) = \ct{S_b}{H_{g,b}}.
\end{multline*}

and thereby to

\begin{multline*}
\sm{j:B\to X}{H_{f} : \prd{b:B}\prd{u:\hfib l b} j(b)=f(\proj1(u))}{H_{g}: \prd{b:B} r(j(b))=g(b)}\\
\prd{b:B}\prd{u:\hfib l b} r(H_{f}(b,u)) = \ct{S_b}{H_{g}(b)}.
\end{multline*}

Modulo these equivalences, the desired map acts as the identity on $j:B\to X$.
Moreover, its action on the remaining parts is given by the equivalences

\begin{align*}
(j\circ l = f)
&\eqvsym \prd{a:A} j(l(a)) = f(a)\\
&\eqvsym \prd{a:A}{b:B}{p:l(a)=b} j(l(a)) = f(a)\\
&\eqvsym \prd{b:B}{a:A}{p:l(a)=b} j(b) = f(a)\\
&\eqvsym \prd{b:B} \prd{u:\hfib l b} j(b) = f(\proj1(u))
\end{align*}

\begin{equation*}
(r\circ j = g)
\eqvsym \prd{b:B} r(j(b)) = g(b)
\end{equation*}

\begin{align*}
(r\circ H_f = \ct{S}{(H_g\circ l)})
&\eqvsym \prd{a:A} r(H_f(a)) = \ct{S(a)}{H_g(l(a))}\\
&\eqvsym \prd{a:A}{b:B}{p:l(a)=b} r(H_f(a)) = \ct{S(a)}{H_g(l(a))}\\
&\eqvsym \prd{b:B}{a:A}{p:l(a)=b} r(H_f(a)) = \ct{S(a)}{H_g(b)}\\
&\eqvsym \prd{b:B}{u:\hfib l b} r(H_f(b,u)) = \ct{S_b}{H_g(b)}
\end{align*}

hence the whole thing is an equivalence.

In any orthogonal factorization system
$(\mathcal{L},\mathcal{R})$, if
$l:A\to B$ is a map such that $\hfib{l}{b} \to \unit$ is in $\cL$ for each $b:B$, then also $l$ itself is in $\cL$.

By <ref>, $l$ is in $\cL$ iff $\fillers S$ is contractible for each $r\in\cR$ and $S$ as in <ref>, while similarly $\hfib{l}{b} \to \unit$ is in $\cL$ iff $\fillers {S_b}$ is contractible.
But the product of contractible types is contractible.

In any stable orthogonal factorization system, if $l\perp r$ for all maps $l\in\cL$ of the form $l:A\to \unit$, then $r\in\cR$.
In particular, for any modality $\modal$, if $X\to (A\to X)$ is an equivalence for all $\modal$-connected types $A$, then $X$ is modal.

By <ref>, for any $l\in\cL$ and commutative square $S$ from $l$ to $r$, we have $\fillers{S} \eqvsym \prd{b:B}\fillers{S_b}$.
Since $(\cL,\cR)$ is stable, each map $\mathord{!}_b:\hfib{l}{b}\to \unit$ is also in $\cL$, so that $\mathord{!}_b\perp r$ by assumption.
Thus $\fillers{S_b}$ is contractible for all $b$, hence so is $\fillers{S}$.

For the second statement, the type $A\to X$ is equivalent to the type of commutative squares

\[
\begin{tikzcd}
A \ar[r,"f"] \ar[d] & X \ar[d] \\ \unit\ar[r] & \unit
\end{tikzcd}
\]

and the type of fillers for such a square is equivalent to the type of $x:X$ such that $f(a) = x$ for all $a:A$, i.e. the fiber of $X\to (A\to X)$ over $f$.
Thus, the assumption ensures that all such types of fillers are contractible, i.e. $l\perp r$ for all $\modal$-connected maps of the form $l:A\to \unit$, so the first statement applies.

Let $(\mathcal{L},\mathcal{R})$ be a stable orthogonal factorization system.
Then a map $r:X\to Y$ is in $\mathcal{R}$ if and only if $\hfib{r}{y}$
is $(\mathcal{L},\mathcal{R})$-modal for each $y:Y$.

The class of right maps is stable under pullbacks by <ref>,
so it suffices to show that any map with modal fibers is in $\mathcal{R}$.

Let $r:X\to Y$ be a map with modal fibers. Our goal is to show that
$r$ is in $\mathcal{R}$. By <ref> it suffices to show that
$r$ has the right lifting property with respect to the left maps.
Consider a diagram of the form

\begin{equation*}
\begin{tikzcd}
A \arrow[d,swap,"l"] \arrow[r,"f"] & X \arrow[d,"r"] \\
B \arrow[r,swap,"g"] & Y
\end{tikzcd}
\end{equation*}

in which $l$ is a map in $\mathcal{L}$.
We wish to show that the type of diagonal fillers is contractible.
By <ref>, the type of diagonal fillers of the above diagram
is equivalent to the dependent product of the types of fillers of

\begin{equation*}
\begin{tikzcd}
\hfib{l}{b} \arrow[d] \arrow[r,"f\circ i_b"] & X \arrow[d,"r"] \\
\unit \arrow[r,swap,"g(b)"] & Y
\end{tikzcd}
\end{equation*}

indexed by $b:B$. Thus, it suffices that the type of diagonal fillers for this
square is contractible for each $b:B$. Since any filler factors uniquely through
the pullback $\unit\times_Y X$, which is $\hfib{r}{g(b)}$, the type of diagonal
fillers of the above square is equivalent to the type of diagonal fillers of the

\begin{equation*}
\begin{tikzcd}
\hfib{l}{b} \arrow[d] \arrow[r,densely dotted] & \hfib{r}{g(b)} \arrow[d] \\
\unit \arrow[r,equals] & \unit
\end{tikzcd}
\end{equation*}

where the dotted map is the uniqe map into the pullback $\hfib{r}{g(b)}$. In
this square, the left map is in $\mathcal{L}$ because $\mathcal{L}$ is assumed
to be stable under pullbacks, and the right map is in $\mathcal{R}$ by assumption,
so the type of diagonal fillers is contractible.

Any two stable orthogonal factorization systems with the same modal types are

By <ref> it follows that any orthogonal factorization system
is completely determined by the class of right maps.
By <ref> it follows that in a stable orthogonal factorization
system, the class of right maps is completely determined by the modal types.

Any stable orthogonal factorization system determines a higher modality with
the same modal types.

For every type $X$ we have the $(\cL,\cR)$-factorization $X\to\modal X\to\unit$ of the
unique map $X\to\unit$. This determines the modal unit
$\modalunit:X\to\modal X$ which is in $\mathcal{L}$, and the
unique map $\modal X\to\unit$ is in $\mathcal{R}$, i.e. $\modal X$ is $(\cL,\cR)$-modal.

To show the induction principle, let $P:\modal X\to\UU$ and $f:\prd{x:X} \modal(P(\eta(x)))$.
Then we have a (judgmentally) commutative square

\begin{equation*}
\begin{tikzcd}
X \arrow[r,"f"] \arrow[d,swap,"\modalunit"] & \sm{z:\modal X}\modal(P(z)) \arrow[d,"\proj1"] \\
\modal X \arrow[r,equals] & \modal X.
\end{tikzcd}
\end{equation*}

Note that by <ref>,
the projection $\proj1:(\sm{z:\modal X}\modal(P(z)))\to\modal X$ is in $\mathcal{R}$
because its fibers are modal. Also, the modal unit
$\modalunit:X\to\modal X$ is in $\mathcal{L}$.
Thus, by <ref>, the type of fillers of this square is contractible.
Such a filler consists of a function $s$ and homotopies filling the two triangles

\begin{equation*}
\begin{tikzcd}
X \arrow[r,"f"] \arrow[d,swap,"\modalunit"] & \sm{z:\modal X}\modal(P(z)) \arrow[d,"\proj1"] \\
\modal X \arrow[r,equals] \arrow[ur,densely dotted] & \modal X
\end{tikzcd}
\end{equation*}

whose composite is reflexivity, i.e. the type

\begin{multline*}
\sm{s:\modal X \to \sm{z:\modal X}\modal(P(z))}{H:\prd{z:\modal X} \proj1(s(z))=z}{K:\prd{x:X} s(\modalunit(x))=f(x)}\\
\prd{x:X} \proj1(K(x)) = H(\modalunit(x)).
\end{multline*}

If we decompose $s$, $f$, and $K$ by their components, we get

\begin{multline*}
\sm{s_1:\modal X \to \modal X}{s_2:\prd{z:\modal X} \modal(P(s_1(z)))}{H:\prd{z:\modal X} s_1(z)=z}\\
\sm{K_1:\prd{x:X} s_1(\modalunit(x))=f_1(x)}{K_2 :\prd{x:X} s_2(\modalunit(x)) =_{K_1(x)} f_2(x)}\\
\prd{x:X} K_1(x) = H(\modalunit(x)).
\end{multline*}

Now we can contract $s_1$ and $H$, and also $K_1$ with the final unnamed homotopy, to get

\begin{equation*}
\sm{s_2:\prd{z:\modal X} \modal(P(z))}  \prd{x:X} s_2(\modalunit(x)) = f_2(x).
\end{equation*}

But this is just the type of extensions of $f$ along $\modalunit$, i.e. the fiber of precomposition by $\modalunit$.
Thus, precomposition by $\modalunit$ is an equivalence, so in fact we have a uniquely eliminating modality.
By <ref>, the identity types of $\modal X$ are modal, so we have a higher modality as well.

§ LOCALIZATION

Localization is the process of inverting a specified class of maps.
In category theory, the localization of a category $\mathcal{C}$ at a family of maps $F$ is obtained by adding formal inverses to those maps freely, obtaining a category $\mathcal{C}[F^{-1}]$ with a universal functor $\mathcal{C}\to \mathcal{C}[F^{-1}]$ sending each map in $F$ to an isomorphism.
In good situations, this universal functor is equivalent to the reflection onto a reflective subcategory of $\mathcal{C}$, which consists of the $F$-local objects: those that “see each map in $F$ as an isomorphism”.
We will not be concerned here with the universal property of the localized category; instead we are interested in constructing reflective subcategories of local objects.
We can do this with a higher inductive type, giving a general construction of reflective subuniverses and modalities.

§.§ Local types and null types

Consider a family $F:\prd{a:A}B(a)\to C(a)$ of maps. We say that a type $X$
is $F$-local if the function

\begin{equation*}
\lam{g}g\circ F_a : (C(a)\to X)\to (B(a)\to X)
\end{equation*}

is an equivalence for each $a:A$.

In other words, $X$ is $F$-local if every $f:B(a)\to X$ extends uniquely to a map $\bar{f}:C(a)\to X$, along the map $F_a:B(a)\to C(a)$, as indicated in the diagram

\begin{equation*}
\begin{tikzcd}
B(a) \arrow[r,"f"] \arrow[d,swap,"F_a"] & X. \\
C(a) \arrow[ur,densely dotted,swap,"\bar{f}"]
\end{tikzcd}
\end{equation*}

Thus, one might say that a type $X$ is $F$-local if it is (right) orthogonal to the maps $F_a$, or that it “thinks each map $F_a$ is an equivalence”.
In <ref> we will see that the $F$-local types determine a reflective subuniverse.

In most of our examples $C$ will be the constant family $\unit$, giving the following specialization.

Let $B:A\to \UU$ be a type family. A type $X$ is said to be $B$-null if the map

\begin{equation*}
\lam{x}\lam{b}x : X \to (B(a) \to X)
\end{equation*}

is an equivalence for each $a:A$.

In other words, $X$ is $B$-null if and only if any map $f:B(a)\to X$ has a unique extension to a map $\unit\to X$, as indicated in the diagram

\begin{equation*}
\begin{tikzcd}
B(a) \arrow[r,"f"] \arrow[d] & X. \\
\unit \arrow[ur,densely dotted]
\end{tikzcd}
\end{equation*}

Thus, a type $X$ is $B$-null if it is (right) orthogonal to the types $B(a)$, or that it “thinks each type $B(a)$ is contractible”.
In <ref> we will see that the $B$-null types determine a modality.

* The unit type is local for any family of maps.

* Since $\emptyt\to X$ is contractible for any type $X$, a type is $\emptyt$-null if and only if it is contractible.

* Any type is $\unit$-null.

* A type $X$ is $\bool$-null if and only if $X$ is a mere proposition. To see this, recall that a mere proposition is a type for which any two points can be identified. A map of type $\bool\to X$ is equivalently specified by two points in $X$. If $X$ is assumed to be $\bool$-null, and $x,y:X$ are points in $X$, then it follows that there is a (unique) point $z:X$ such that $x=z$ and $y=z$. In particular it follows that $x=y$, so we conclude that $X$ is a mere proposition.

* More generally, a type is $\Sn^{n+1}$-null if and only if it is $n$-truncated.
This follows from  <cit.>.

* If $Q$ is a mere proposition, then the $Q$-null types are exactly the $\open Q$-modal types (see <ref>).

We choose to consider the notion of being local at a family of maps, rather than
as a class of maps (i.e. a subtype of $\sm{X,Y:\UU}X\to Y$). A family of maps (indexed by a type $A$ in $\UU$) is intrinsically small with respect to $\UU$, whereas a class
is not. By localizing at a small family of maps, we obtain a small type constructor.
Nevertheless, one can show that for any family $F$ of maps, a type is $F$-local
if and only if it is local at the class $\im(F)$, when $\im(F)$ is regarded
as a subtype of $\sm{X,Y:\UU}X\to Y$. A similar relation holds for
set-quotients in [33].

A more nontrivial example is the following.

Let $A$ be a type, and let $\susp(A)$ be its suspension.
Then a type $X$ is $\susp(A)$-local if and only if its identity types are $A$-local.

The universal property of $\susp(A)$ is that

\[ (\susp(A) \to X) \simeq \sum_{x,y:A} (A\to (x=y)). \]

Since $A\simeq \sum_{x,y:A} (x=y)$, to say that $X$ is $\susp(A)$-local is to say that the map

\[ \Big(\sm{x,y:A} (x=y)\Big) \to \Big(\sm{x,y:A} (A\to (x=y))\Big) \]

is an equivalence.
But this is the total space of the fiberwise map

\[ (x=y) \to (A\to (x=y)) \]

for all $x,y:A$, hence it is an equivalence if and only if they all are, i.e. if and only if all identity types of $X$ are $A$-local.

Since the $n$-sphere $\Sn^n$ is equivalent the $n$-fold suspension of $\bool$, it follows that:

A type if $\Sn^{n+1}$-local if and only if it is an $n$-type.

Suppose $F:\prd{a:A}B(a)\to C(a)$ is a family of maps, and $X$ is a type for
which the map

\begin{equation*}
\lam{g}g\circ F_a : (C(a)\to X)\to (B(a)\to X)
\end{equation*}

is an embedding. Then the identity types of $X$ are $F$-local.

We will see [later] that the converse also holds.add autoref

By the assumption that the map $\blank\circ F_a: (C(a)\to X)\to(B(a)\to X)$ is
an embedding,
its action on paths

\begin{equation*}
\mapfunc{\blank\circ F_a}(g,g'):{(g=g')}\to{(g\circ F_a=g'\circ F_a)}
\end{equation*}

is an equivalence for any $g,g':C(a)\to X$.
In particular, we have this equivalence for $g\defeq \lam{c}x$ and
$g'\defeq\lam{c}y$, for any $x,y:X$.
We have a commuting square

\begin{equation*}
\begin{tikzcd}
(\lam{c}x=\lam{c}y) \arrow[d,swap,"{\lam{p}\mapfunc{\blank\circ F_a}(p)}"] \arrow[r,"\eqvsym"] & (x=y)^{C(a)} \arrow[d,"\blank\circ F_a"] \\
(\lam{b}x=\lam{b}y) \arrow[r,swap,"\eqvsym"] & (x=y)^{B(a)}
\end{tikzcd}
\end{equation*}

of which the top and bottom maps are equivalences by the function extensionality
principle. It follows that the right map is a composite of equivalences.
Hence we see that the type $x=y$ is $F$-local.

If $X$ is an $F$-local type, then so are its identity types.

§.§ Localizing at a family of maps

In this subsection we introduce the localization operation and show that it determines a reflective subuniverse, which is a modality in the case of nullification.
We define a modal operator $\localization{F}:\UU\to\UU$ called localization at $F$, via a construction involving higher inductive types.
The idea is that one of the point constructors will be the modal unit $\modalunit[X]$ and the other constructors build in exactly the data making each $\lam{g}g\circ F_a$ an equivalence.

For this to be homotopically well-behaved, we have to choose a “good” notion of equivalence such as those in <cit.>.
Any such choice is possible, but some are easier than others.
Of those in [40], “bi-invertibility” is easiest because it allows us to avoid 2-path constructors.
However, the following notion of equivalence, which doesn't appear in [40], is easier still.
As we will see, this is because although it does include 2-path constructors, the four data it comprises can be broken into two pairs that can be treated “uniformly” despite occuring at “different dimensions”; thus we only need to deal explicitly with one point constructor and one path constructor (and no 2-path constructors).

For $f:A\to B$ we write

\begin{equation*}
\mathsf{rinv}(f) \defeq \sm{g:B\to A} (f\circ g = \idfunc[B])
\end{equation*}

and for $x,y:A$ we write $\apfunc{f}^{x,y} : (x=y) \to (fx=fy)$ for the action of $f$ on identities.

We say that $f$ is path-split if we have an inhabitant of the following type:

\[ \mathsf{pathsplit}(f) \defeq \mathsf{rinv}(f) \times \prd{x,y:A} \mathsf{rinv}(\apfunc{f}^{x,y}). \]

For any $f$ we have $\eqv{\mathsf{pathsplit}(f)}{\isequiv(f)}$.

If $f$ is path-split, to show that it is an equivalence it suffices to show that its right inverse $g$ is also a left inverse, i.e. that $gfx=x$ for all $x:A$.
But $fgfx = fx$ since $f\circ g = \idfunc[B]$, and $\apfunc{f} : (gfx=x) \to (fgfx=fx)$ has a right inverse, so $gfx=x$.

This gives a map $\mathsf{pathsplit}(f) \to \isequiv(f)$; to show that it is an equivalence, we may assume that its codomain is inhabited.
But if $f$ is an equivalence, then so is $\apfunc{f}^{x,y}$, and hence $\mathsf{rinv}(f)$ and $\mathsf{rinv}(\apfunc{f}^{x,y})$ are both contractible.
So in this case $\mathsf{pathsplit}(f)$ and $\isequiv(f)$ are both contractible, hence equivalent.

Now let $F:\prd{a:A} B(a) \to C(a)$ be a family of functions and $X:\UU$.
As a “first approximation” to the localization $\localization{F}(X)$, let $\localhit{F}{X}$ be the higher inductive type with the following constructors:

* $\alpha_X : X \to \localhit{F}{X}$

* $\mathsf{ext} : \prd*{a:A} (B(a) \to \localhit{F}{X}) \to (C(a) \to \localhit{F}{X})$

* $\mathsf{isext} : \prd*{a:A}{f:B(a)\to\localhit{F}{X}}{b:B(a)}\id{\mathsf{ext}(f)(F_a(b))}{f(b)}$.

The induction principle of $\localhit{F}{X}$ is that for any type family $P:\localhit{F}{X}\to \UU'$, if there are terms

\begin{align*}
N & : \prd{x:X}P(\alpha_X(x))\\
R & : \prd*{a:A}{f:B(a)\to\localhit{F}{X}}(\prd{b:B(a)}P(f(b)))\to\prd{c:C(a)} P(\mathsf{ext}(f,c)) \\
S & : \prd*{a:A}{f:B(a)\to\localhit{F}{X}}{f':\prd{b:B(a)}P(f(b))}{b:B(a)}\dpath{P}{\mathsf{isext}(f,b)}{R(f')(F_a(b))}{f'(b)},
\end{align*}

then there is a section $s:\prd{x:\localhit{F}{X}}P(x)$ such that $s\circ \alpha_X= N$.
(The section $s$ also computes on $\mathsf{ext}$ and $\mathsf{isext}$, but we will not need those rules.)
Note that the family $P$ does not have to land in the same universe $\UU$ that contains our types $A,B,C,X$; this will be important in <ref>.

This approximation $\localhit{F}{X}$ behaves like we expect $\localization{F}(X)$ to behave when mapping into local types:

If $Y$ is $F$-local (and $X$ is arbitrary), then precomposition with $\alpha_X$

\[ (-\circ \alpha_X) : (\localhit{F}{X} \to Y) \to (X\to Y) \]

is an equivalence.

We will show that this map is path-split.

First we have to construct a right inverse to it, i.e. given $g:X\to Y$ we must extend it to $\localhit{F}{X}$.
We will apply the induction principle using the constant family $Y$ over $\localhit{F}{X}$ and $N\defeq g$, so that the computation rule shows that what we get is an extension of $g$.
To construct the cases of $R$ and $S$, let $f:B(a)\to \localhit{F}{X}$, and let $f':B(a)\to Y$.
Our goal is to construct $R(f,f'):C(a)\to Y$ together with a witness $S(f,f')$ that the triangle

\begin{equation*}
\begin{tikzcd}[column sep=large]
B(a) \arrow[dr,"{f'}"] \arrow[d,swap,"F_a"] \\
C(a) \arrow[r,swap,"{R(f,f')}"] & Y
\end{tikzcd}
\end{equation*}

But $Y$ is $F$-local, so the map

\[ (-\circ F_a) : (C(a) \to Y) \to (B(a)\to Y) \]

is an equivalence, and hence in particular has a right inverse; applying this right inverse to $f'$ gives $R$ and $S$.

Second, we must suppose given $g,h:\localhit{F}{X} \to Y$ and construct a right inverse to

\[ \apfunc{(-\circ \alpha_X)} : (g=h) \to (g\circ \alpha_X = h\circ \alpha_X). \]

Thus, suppose we have $K : \prd{x:X} g(\alpha_X(x)) = h(\alpha_X(x))$; we must extend $K$ to a homotopy $\tilde{K} : \prd{z:\localhit{F}{X}} g(z)=h(z)$ such that $\tilde{K}(\alpha_X(x)) = K(x)$.
We will apply the induction principle using the family $P:\localhit{F}{X} \to \UU$ defined by $P(z) \defeq (g(z)=h(z))$, and $N\defeq K$.
To construct the cases of $R$ and $S$, let $f:B(a)\to \localhit{F}{X}$ and $f':\prd{b:B(a)} gfb = hfb$.
Our goal is to construct $R(f,f'):\prd{c:C(a)} g(\mathsf{ext}(f,c))=h(\mathsf{ext}(f,c))$ together with a witness $S(f,f')$ that for any $b:B(a)$ we have

\begin{equation}
R(f,f')(F_a(b)) = \ct{\ap{g}{\mathsf{isext}(f,b)}}{\ct{f'(b)}{\ap{h}{\mathsf{isext}(f,b)}^{-1}}}.\label{eq:locpsRS}
\end{equation}

However, once again, since $Y$ is $F$-local, the map

\[ (-\circ F_a) : (C(a) \to Y) \to (B(a)\to Y) \]

is an equivalence, and hence in particular

\begin{equation}
\apfunc{(-\circ F_a)} :
(g\circ \mathsf{ext}(f) = h\circ \mathsf{ext}(f)) \to (g\circ \mathsf{ext}(f) \circ F_a = h\circ \mathsf{ext}(f) \circ F_a)\label{eq:locpsap}
\end{equation}

has a right inverse.
But the right-hand side of (<ref>) inhabits the codomain of (<ref>), so applying this right inverse gives $R$ and $S$.

In general, $\localhit{F}{X}$ is not $F$-local: its constructors only ensure that each map

\[ (-\circ F_a) : (C(a) \to \localhit{F}{X}) \to (B(a) \to \localhit{F}{X}) \]

has a right inverse, not that it is an equivalence.
(In fact, $\localhit{F}{X}$ is the “free algebraically $F$-injective type on $X$”, cf. [7].)

However, it does happen in many common cases that $\localhit{F}{X}$ is already $F$-local (and hence the $F$-localization of $X$).
Specifically, this happens whenever each $(-\circ F_a)$ already has a left inverse, which happens whenever each $F_a : B(a) \to C(a)$ has a right inverse.
For instance, if $C(a)\defeq\unit$ for all $a$ (so that we are talking about $B$-nullification), then this happens whenever all the types $B(a)$ are inhabited (i.e. we have $\prd{a:A}B(a)$); cf. <cit.>.

In particular, this occurs for $\Sn^{n+1}$-nullification for $n\ge -1$, which as we saw in <ref> coincides with $n$-truncation.
In this case $\localhit{F}{X}$ essentially reduces to the “hub and spoke” construction of truncations from <cit.>.

A concrete example where $\localhit{F}{X}$ is not yet $F$-local is $\emptyset$-nullification, where $\localhit{F}{X} = X+\unit$, but only contractible types are $\emptyset$-null.
Note that $\emptyset = \Sn^{-1}$, so this is equivalently $(-2)$-truncation.

To modify $\localhit{F}{X}$ to become $F$-local using bi-invertibility or half-adjoint equivalences, we would need to add two more constructors to $\localhit{F}{X}$ corresponding to the additional two pieces of data in those definitions of equivalence, and then add two more cases to the proof of <ref> to deal with those constructors.
Moreover, these additional cases are rather more difficult than the ones we gave, since they involve homotopies “on the other side”.

Fortunately, with path-splitness, we can instead use a simple trick.
Given any map $f:B\to C$, let $\Delta_f : B\to B\times_C B$ be its diagonal and $\nabla_f : C +_B C \to C$ its codiagonal.

For any $f:B\to C$ and any $X$, we have a commuting triangle

\begin{equation*}
\begin{tikzcd}[column sep=-2em]
\phantom{(C\to X) \times_{(B\to X)} (C\to X)} & (C\to X) \arrow[dl,swap,"(-\circ \nabla_f)"] \arrow[dr,"\Delta_{(-\circ f)}"] \\
(C +_B C \to X) \arrow[rr,"\sim"] & & (C\to X) \times_{(B\to X)} (C\to X)
\end{tikzcd}
\end{equation*}

in which the bottom map is an equivalence.

By the universal property of the pushout.

For any $f:B\to C$, we have

\[ \mathsf{pathsplit}(f) \eqvsym \mathsf{rinv}(f) \times \mathsf{rinv}(\Delta_f). \]

Decomposing $B\times_C B$ and its identity types into $\Sigma$-types, we have

\begin{align*}
\mathsf{rinv}(\Delta_f)
&\eqvsym \prd{x,y:B}{p:fx=fy}\sm{z:B}{q:x=z}{r:z=y} \ct{\apfunc{f}^{x,z}(q)}{\apfunc{f}^{z,y}(r)} = p\\
&\eqvsym \prd{x,y:B}{p:fx=fy}\sm{r:x=y} \apfunc{f}^{x,y}(r) = p\\
&\eqvsym \prd{x,y:B} \mathsf{rinv}(\apfunc{f}^{x,y}).\qedhere
\end{align*}

For $f:B\to C$, a type $X$ is $f$-local if and only if both maps

\begin{align*}
(-\circ f) &: (C\to X) \to (B\to X) \\
(-\circ \nabla_f) &: (C\to X) \to (C +_B C \to X)
\end{align*}

have right inverses, and if and only if both of these maps are equivalences.

By <ref>, $X$ is $f$-local if and only if $(-\circ f)$ and $\Delta_{(-\circ f)}$ have right inverses, but by <ref> the latter is equivalent to $(-\circ \nabla_f)$.
The second statement follows since the diagonal of an equivalence is an equivalence.

<ref> implies that for $F$-locality it suffices for precomposition with each $F_a$ and $\nabla_{F_a}$ to have right inverses.
But $\localhit{F}{X}$ is the universal way to make precomposition with each $F_a$ have right inverses, so to localize we just need to add all the morphisms $\nabla_{F_a}$ to $F$.

Specifically, for any $F:\prd{a:A} B(a) \to C(a)$, define $\hat B,\hat C : A+A \to \UU$ and a family $\hat F: \prd{a:A+A} \hat B(a) \to \hat C(a)$ by

B̂((a))    B(a)      Ĉ((a))    C(a)      F̂((a))    F_a

B̂((a))    C(a) +_B(a) C(a)      Ĉ((a))    C(a)      F̂((a))    ∇_F_a.

For any $X:\UU$, the localization of $X$ at $F$ is $\localization{F}(X) \defeq \localhit{\hat F}{X}$, and $\modalunit[X] : X\to \localization{F}(X)$ is $\alpha^{\hat F}_X$.

As noted in <ref>, a simple example where $\localhit{F}{X}$ is not yet $F$-local is $\emptyset$-nullification, where $F$ is the single map $\emptyset\to\unit$.
In this case $\hat F$ consists of $\emptyset\to\unit$ and the fold map $\nabla : \unit+\unit \to \unit$.
The constructors of $\localhit{\hat F}{X}$ corresponding to the former give it a point, and those corresponding to the latter make it a mere proposition (in fact they are the constructors of $(-1)$-truncation, i.e. $\Sn^{0}$-nullification).
Thus, $\localhit{\hat F}{X}$ is contractible, i.e. $\emptyset$-local.

For any $F:\prd{a:A} B(a) \to C(a)$, the type $\localization{F}(X)$ is $F$-local.

The constructors of $\localization{F}(X)$ as $\localhit{\hat F}{X}$ say that the precomposition maps

\[ (-\circ \hat F_a) : (\hat C(a) \to \localhit{\hat F}{X}) \to (\hat B(a) \to \localhit{\hat F}{X}) \]

have right inverses for all $a:A+A$.
But by definition of $\hat F$, these maps consist of precomposition with each $F_a$ and $\nabla_{F_a}$.
Thus, by <ref>, $\localhit{\hat F}{X}$ is $F$-local.

If $Y$ is $F$-local (and $X$ is arbitrary), then precomposition with $\modalunit[X]$

\[ (-\circ \modalunit[X]) : (\localization{F}(X) \to Y) \to (X\to Y) \]

is an equivalence.

By the second clause of <ref>, any $F$-local type is also $\hat F$-local; so this follows from <ref>.

The subuniverse of $F$-local types in $\UU$ is a reflective subuniverse, with modal operator $\localization{F}$.

By <ref>.

§.§ Nullification and accessibility

A general localization is only a reflective subuniverse, but there is a convenient sufficient condition for it to be a modality: if each $C(a)=\unit$.
A localization modality of this sort is called nullification.

If $F:\prd{a:A} B(a) \to C(a)$ is such that each $C(a)=\unit$, then localization at $F$ is a modality, called nullification at $B$.

It suffices to show that for any $B:A\to\UU$, the $B$-null types are $\Sigma$-closed.
Thus, let $X:\UU$ and $Y:X\to \UU$ be such that $X$ and each $Y(x)$ are $B$-null.
Then for any $a:A$ we have

\begin{align*}
(B(a)\to \sm{x:X} Y(x))
&\eqvsym \sm{g:B(a)\to X} \prd{b:B(a)} Y(g(b)) \\
&\eqvsym \sm{x:X} B(a) \to Y(x) \\
&\eqvsym \sm{x:X} Y(x)
\end{align*}

with the inverse equivalence being given by constant maps.
Thus, $\sm{x:X} Y(x)$ is $B$-null.

Of course, it might happen that $\localization{F}$ is a modality even if $F$ doesn't satisfy the condition of <ref>.
For instance, if $B:A\to \UU$ has a section $s:\prd{a:A} B(a)$, then localizing at the family $s' : \prd{a:A} \unit \to B(a)$ is equivalent to nullifying at $B$, since in a section-retraction pair the section is an equivalence if and only if the retraction is.
However, we can say the following.

If $F:\prd{a:A} B(a)\to C(a)$ is such that $\localization{F}$ is a modality, then there exists a family $E:D\to \UU$ such that $\localization{F}$ coincides with nullification at $E$.

Write $\modal\defeq\localization{F}$ and $\modalunit$ for its modal unit.
Define $D = \sm{a:A} (\modal (B(a)) + \modal(C(a)))$, and $E:D\to \UU$ by

\begin{align*}
E(a,\inl(b)) &\defeq \hfib{\modalunit[B(a)]}{b}\\
E(a,\inr(c)) &\defeq \hfib{\modalunit[C(a)]}{c}.
\end{align*}

Then since $\modalunit$ is $\modal$-connected, each $E(d)$ is $\modal$-connected, and hence every $F$-local type is $E$-null.

On the other hand, suppose $X$ is an $E$-null type.
Each $\modalunit[B(a)]$ and $\modalunit[C(a)]$ is $\localization{E}$-connected, since their fibers are $\localization{E}$-connected (by definition); thus $X$ is also $\modalunit[B(a)]$-local and $\modalunit[C(a)]$-local.
But we have the following commutative square:

\[
\begin{tikzcd}[column sep=large]
B(a) \ar[r,"{\modalunit[B(a)]}"] \ar[d,"F_a"'] & \modal(B(a)) \ar[d,"{\modal(F_a)}"]\\
C(a) \ar[r,"{\modalunit[C(a)]}"'] & \modal(C(a))
\end{tikzcd}
\]

and ${\modal(F_a)}$ is an equivalence; thus $X$ is also $F_a$-local.
So the $F$-local types coincide with the $E$-null types.

This shows that the following pair of definitions are consistent.

A reflective subuniverse on $\UU$ is said to be accessible if it is the localization at a family of maps in $\UU$, indexed by a type in $\UU$.
Similarly, a modality $\modal$ on $\UU$ is said to be accessible if it is the nullification at a family of types in $\UU$, indexed by a type in $\UU$.

Explicitly, a presentation of a reflective subuniverse $\modal$ of $\UU$ consists of a family of maps $F : \prd{a:A} B(a) \to C(a)$, where $A:\UU$ and $B,C:A\to\UU$, such that $\modal = \localization{F}$.
Similarly, a presentation of a modality $\modal$ consists of a family of types $B: A\to\UU$, where $A:\UU$, such that $\modal = \localization{\lam{a} B(a)\to \unit}$.

Note that being accessible is structure; different families can present the same reflective subuniverse or modality.
As a trivial example, note that localizing at the empty
type, and localizing at the type family on $\bool$ defined by
$\bfalse\mapsto \emptyt$ and $\btrue\mapsto \unit$ both map all types to contractible types.

However, we are usually only interested in properties of presentations insofar as they determine properties of subuniverses.
For instance, by <ref>, a reflective subuniverse is a modality exactly when it has a presentation in which each $C(a)=\unit$.
Similarly, in <ref> we will define a modality to be “topological” if it has a presentation in which each $C(a)=\unit$ and each $B(a)$ is a mere proposition.

The trivial modality $\truncf{(-2)}$ is presented by $\emptyt$, while the propositional truncation modality $\truncf{(-1)}$ is presented by $\bool$.  More generally, the
$n$-truncation modality $\truncf{n}$ is presented by the $(n+1)$-sphere $\Sn^{n+1}$.

For every mere proposition $P$, the open modality $\open P (X) \defeq (P\to X)$ from <ref> is
presented by the singleton type family $P$.
To see this, note that $\modalunit[X] : X \to (P\to X)$ is the same as the map in the definition of locality, so that $X$ is modal for the open modality on $P$ if and only if it is $P$-null.
(If $P$ is not a mere proposition, however, then $X\mapsto (P\to X)$ is not a modality, and in particular does not coincide with localization at $P$.)

The closed modality $\closed P$ from <ref> associated to a mere proposition $P$ is presented by the type family $\lam{x} \emptyt : P \to \UU$.
For by definition, $A$ is null for this family if and only if for any $p:P$ the map $A \to (\emptyt \to A)$ is an equivalence.
But $\emptyt \to P$ is contractible, so this says that $P\to\iscontr(A)$, which was the definition of $\closed P$-modal types from <ref>.

One of the main uses of accessibility is when passing between universes.
Our definitions of reflective subuniverses and modalities are relative to a particular universe $\UU$, but most examples are “uniform” or “polymorphic” and apply to types in all universes (or all sufficiently large universes) simultaneously.
Accessibility is one technical condition which ensures that this holds and that moreover these modal operators on different universes “fit together” in a convenient way.
For instance, we have:

If $\modal$ is an accessible reflective subuniverse on a universe $\UU$, and $\UU'$ is a larger universe containing $\UU$, then there is a reflective subuniverse $\modal'$ on $\UU'$ such that:

* If $\modal$ is a modality, so is $\modal'$.

* A type $X:\UU$ is $\modal'$-modal if and only if it is $\modal$-modal.

* For $X:\UU$, the induced map $\modal' X \to \modal X$ is an equivalence.

* A type $X:\UU'$ is $\modal'$-modal if and only if $(\blank\circ f) : (B\to X) \to (A\to X)$ is an equivalence for any map $f:A\to B$ in $\UU$ such that $\modal(f)$ is an equivalence.

* $\modal'$ depends only on $\modal$, not on a choice of presentation for it.

Since $\modal$ is accessible, it is generated by some family $F:\prd{a:A} B(a) \to C(a)$.
Define $\modal':\UU'\to\UU'$ to be the higher inductive localization at the same family $F$, which lives in $\UU'$ as well since $\UU'$ is larger than $\UU$.
If $\modal$ is a modality, we can take each $C(a)=\unit$ so that $\modal'$ is also a modality, giving <ref>.

The notion of $F$-locality for a type $X$ is independent of what universe $X$ lives in, giving <ref>.
Moreover, because the induction principle for a higher inductive localization allows us to eliminate into any type in any universe, <ref> applies no matter what universe the target lives in.
Thus, if $X:\UU$ then $\modal X$ and $\modal' X$ have the same universal property, hence are canonically equivalent, giving <ref>.

To prove <ref>, note first that certainly each $\modal (F_a)$ is an equivalence, so any type with the stated property is $F$-local.
Conversely, if $X$ is $F$-local, hence $\modal'$-modal, then $(B\to X) \to (A\to X)$ is certainly an equivalence for any map $f$ such that $\modal'(f)$ is an equivalence; but $\modal'$ and $\modal$ coincide on $\UU$.
Thus <ref> holds; and this implies <ref> since a reflective subuniverse is determined by its modal types.

We refer to the $\modal'$ constructed in <ref> as the canonical accessible extension of $\modal$ to $\UU'$.

Our characterizations of the truncation and open and closed modalities in <ref> made no reference to the ambient universe.
Thus, when these modalities are defined in the standard ways on $\UU$ and $\UU'$ respectively, their $\UU'$-version is the canonical accessible extension of their $\UU$-version.

By contrast, the double-negation modality $\neg\neg$ is defined in a polymorphic way on all universes, but in general there seems no reason for it to be accessible on any of them.
However, if propositional resizing holds, then it is the nullification at $\bool$ together with all propositions $P$ such that $\neg\neg P$ holds, and hence accessible.

Whether or not any inaccessible modalities remain after imposing propositional resizing may depend on large-cardinal principles.
It is shown in [10] that this is the case for the analogous question about reflective sub-$(\infty,1)$-categories of the $(\infty,1)$-category of $\infty$-groupoids.

Suppose that all types in $\UU$ are 0-types.
We have tacitly assumed that all universes are closed under all higher inductive types, so (assuming univalence) this is not actually possible, but to get a feeling for what else could in principle go wrong suppose we drop that assumption.
Then if $F$ is a family such that the higher inductive type $\localization{F}$ does not preserve 0-types, we might (depending on what we assume about closure under higher inductive types) still be able to define a modality on $\UU$ by $\modal X = \trunc0{\localization{F}X}$.
But if $\UU'$ is a larger universe containing non-0-types, then this $\modal$ would not eliminate into types in $\UU'$, and if we define $\modal'$ by localizing at $F$ in $\UU'$ then the canonical map $\modal' X \to \modal X$ would be the 0-truncation rather than an equivalence.
So <ref> is not as trivial as it may seem.

It is tempting to think that any reflective subuniverse $\modal$ on $\UU$ could be extended to an accessible one on $\UU'$ by localizing at the family of all functions in $\UU$ that are inverted by $\modal$ (or nullifying at the family of all $\modal$-connected types in $\UU$, in the case of modalities), which is a $\UU'$-small family though not a $\UU$-small one.
This does produce an accessible reflective subuniverse $\modal'$ of $\UU'$ such that the $\modal'$-modal types in $\UU$ coincide with the $\modal$-modal ones, but there seems no reason why the modal operators $\modal'$ and $\modal$ should agree on types in $\UU$.

Reflective subuniverses and modalities defined by localization have another convenient property: their eliminators have a strict judgmental computation rule (assuming that our higher inductive localization type has a judgmental computation rule on point-constructors, which is usually assumed).
This will be useful in <ref>.

§.§ Non-stable factorization systems

We have seen in <ref> that $\Sigma$-closed reflective subuniverses are equivalent to stable orthogonal factorization systems.
Without $\Sigma$-closedness and stability, this equivalence fails.
However, we can still say:

Any orthogonal factorization system has an underlying reflective subuniverse, consisting of those types $X$ such that $X\to\unit$ is in $\cR$.

If $Y$ is modal in this sense, then by applying orthogonality to squares of the form

\[
\begin{tikzcd}
A \ar[d,"f"'] \ar[r] & Y \ar[d] \\ B \ar[r] & \unit
\end{tikzcd}
\]

we see that if $f:A\to B$ lies in $\cL$, then precomposition

\[ (-\circ f) : (B\to Y) \to (A\to Y) \]

is an equivalence.
Thus, it suffices to show that for every $X$ there is an $\cL$-map $X\to \modal X$ where $\modal X\to \unit$ is in $\cR$; but this is just an $(\cL,\cR)$-factorization of the map $X\to\unit$.

Conversely, in classical category theory there are various ways of extending a reflective subcategory to a factorization system.
One canonical one is considered in [11], but this is harder to reproduce homotopy-theoretically.
(It is possible in what is there called the “simple” case, hence also the “semi-left-exact” case — which includes all modalities, as the case of “stable units” — but we will not investigate that construction here.)
Instead, if we have an accessible reflective subuniverse presented by localization at a family of maps, we can generalize the construction of localization to produce a factorization system (though in general the result will depend on the choice of presentation, not just on the reflective subuniverse we started with).

To avoid too much wrangling with witnesses of commutative squares, we will factorize dependent types rather than functions.
In this case, right orthogonality (<ref>) can be expressed in the following way.

Given $l:A\to B$ and $X:Y\to\UU$, and functions $g:B\to Y$ and $f:\prd{a:A} X(g(l(a)))$ forming a judgmentally commutative square

\begin{equation}
\begin{tikzcd}[column sep=large]
A \ar[d,"l"'] \ar[r,"{(g\circ l,f)}"] & \sm{y:Y}X(y) \ar[d,"\proj1"] \\ B \ar[r,"g"'] & Y
\end{tikzcd}\label{eq:dfill-sq}
\end{equation}

a dependent filler in this square consists of a morphism ${j:\prd{b:B} X(g(b))}$ and a homotopy $j\circ l \sim f$.
That is, the type of dependent fillers is

\begin{equation}
\dfill{l,X,g,f} \defeq \sm{j:\prd{b:B} X(g(b))} \prd{a:A} j(l(a)) = f(a).\label{eq:dep-fillers}
\end{equation}

Recall that for a map $f:B\to C$, we denote by $\Delta_f : B\to B\times_C B$ its diagonal and $\nabla_f : C +_B C \to C$ its codiagonal.
We have the following dependent generalization of <ref>:

Let $f:B\to C$ and $X:Y\to\UU$ and $g:C\to Y$; then we have a commuting triangle

\begin{equation*}
\begin{tikzcd}
& \prd{c:C} X(g(c)) \arrow[dl,swap,"(-\circ \nabla_f)"] \arrow[d,"\Delta_{(-\circ f)}"] \\
\prd{z:C +_B C} X(g'(z)) \arrow[r,"\sim"'] &
\Big(\prd{c:C} X(g(c))\Big) \times_{(\prd{b:B} X(g(f(b))))} \Big(\prd{c:C} X(g(c))\Big)
\end{tikzcd}\end{equation*}

where $g':C+_BC \to Y$ is induced by $g$ on both copies of $C$, and the bottom map is an equivalence.

Like the non-dependent case <ref>, this follows from the universal property of the pushout.

And similarly for <ref>:

For $l:B\to C$ and $X:Y\to\UU$, the following are equivalent.

* The map $\proj1 : (\sm{y:Y}X(y)) \to Y$ is right orthogonal to $l$.

* For every $g:C\to Y$ and $f:\prd{b:B} X(g(l(b)))$, the type $\dfill{l,X,g,f}$ of dependent fillers in (<ref>) is contractible.

* For every $g:C\to Y$, the precomposition map

\begin{equation}
(-\circ l) : \Big(\prd{c:C} X(g(c))\Big) \to \Big(\prd{b:B} X(g(l(b)))\Big)\label{eq:dfill-eqv}
\end{equation}

is an equivalence.

* For every $g:C\to Y$, the precomposition maps

\begin{align*}
(-\circ l) &: \Big(\prd{c:C} X(g(c))\Big) \to \Big(\prd{b:B} X(g(l(b)))\Big)\\
(-\circ \nabla_l) &: \Big(\prd{c:C} X(g(c))\Big) \to \Big(\prd{z:C+_BC} X(g'(z))\Big)
\end{align*}

have right inverses.

* For every $g:C\to Y$, the maps in <ref> are equivalences.

The equivalence of <ref> and <ref> is immediate, since $\dfill{l,X,g,f}$ is the fiber of (<ref>) over $f$.
And as in <ref>, <ref> is equivalent to <ref> and <ref> using <ref>.

Finally, regarding <ref>, if we have any commutative square

\[
\begin{tikzcd}
B \ar[d,"l"'] \ar[r,"f'"] \ar[dr,phantom,"S"] & \sm{y:Y}X(y) \ar[d,"\proj1"] \\ C \ar[r,"g"'] & Y
\end{tikzcd}
\]

witnessed by $S:\proj1 \circ f'=g\circ l$, we can define $f(b) \defeq \trans{S(b)}{\proj2(f'(b))}$ to get an equivalent and judgmentally commutative square as in (<ref>).
Thus, <ref> is equivalent to its restriction to such squares.
But given such a square, the type of ordinary diagonal fillers (<ref>) is equivalent to

\[ \sm{j:C\to \sm{y:Y} X(y)}{H_f : j\circ l = (g\circ l,f)}{H_g : \proj1 \circ j = g} \proj1 \circ H_f = H_g \circ l \]

and thereby to

\begin{multline*}
\sm{j_1:C\to Y}{j_2 : \prd{c:C} X(j_1(c))}\\
\sm{H_{f1} : j_1 \circ l = g\circ l}{H_{f2} : \dpath{X}{H_{f1}}{j_2\circ l}{f}}{H_g : j_1 = g} H_{f1} = H_g \circ l.
\end{multline*}

But now we can contract two based path spaces (combining $j_1$ with $H_g$, and $H_{f1}$ with the final unnamed equality $H_{f1} = H_g\circ l$) to get the type (<ref>) of dependent fillers.

Let $F:\prd{a:A} B(a) \to C(a)$ and let $X:Y\to\UU$ be a type family.
We define an indexed higher inductive type $\factorhit{F}{Y}{X} : Y\to \UU$ by the following constructors:

\begin{align*}
\beta_X &: \prd{y:Y} X(y) \to \factorhit{F}{Y}{X}(y)\\
\mathsf{lift} &: \prd*{a:A}{g:C(a) \to Y}{f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))}{c:C(a)} \factorhit{F}{Y}{X}(g(c))\\
\mathsf{islift} &
\!\begin{multlined}[t]
: \prd*{a:A}{g:C(a) \to Y}{f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))}{b:B(a)}\\
\mathsf{lift}(g,f,F_a(b)) = f(b).
\end{multlined}
\end{align*}

Diagrammatically, $\mathsf{lift}$ and $\mathsf{islift}$ comprise a specified dependent filler for any judgmentally commutative square as follows:

\[
\begin{tikzcd}
B(a) \ar[d,"{F_a}"'] \ar[r,"f"] & \sm{y:Y} \factorhit{F}{Y}{X}(y) \ar[d,"\proj1"] \\
C(a) \ar[ur,dotted] \ar[r,"g"'] & Y.
\end{tikzcd}
\]

The induction principle of $\factorhit{F}{Y}{X}$ says that for any $P:\prd{y:Y} \factorhit{F}{Y}{X}(y) \to \UU$ with

\begin{align*}
N &: \prd{y:Y}{x:X(y)} P(y,\beta_X(y,x))\\
R &
\!\begin{multlined}[t]
: \prd{a:A}{g:C(a) \to Y}{f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))}\\
\prd{f':\prd{b:B(a)} P(g(F_a(b)),f(b))}{c:C(a)} P(g(c),\mathsf{lift}(g,f,c))
\end{multlined}
\\
S &
\!\begin{multlined}[t]
: \prd{a:A}{g:C(a) \to Y}{f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))}\\
\prd{f':\prd{b:B(a)} P(g(F_a(b)),f(b))}{b:B(a)} \dpath{P}{\mathsf{islift}(g,f,b)}{R(g,f,f',F_a(b))}{f'(b)}
\end{multlined}
\end{align*}

there is a section $s:\prd{y:Y}{w:\factorhit{F}{Y}{X}(y)} P(y,w)$ such that $s \circ \beta_X = N$ (plus two more computation rules we ignore).
Note that by transporting along $\mathsf{islift}$, the types of $R$ and $S$ are equivalent to

\begin{align*}
R' &
\!\begin{multlined}[t]
: \prd{a:A}{g:C(a) \to Y}{f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))}\\
\prd{f':\prd{b:B(a)} P(g(F_a(b)),\mathsf{lift}(g,f,F_a(b)))}{c:C(a)} P(g(c),\mathsf{lift}(g,f,c))
\end{multlined}
\\
S' &
\!\begin{multlined}[t]
: \prd{a:A}{g:C(a) \to Y}{f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))}\\
\prd{f':\prd{b:B(a)} P(g(F_a(b)),\mathsf{lift}(g,f,F_a(b)))}{b:B(a)} \id{R(g,f,f',F_a(b))}{f'(b)}.
\end{multlined}
\end{align*}

With this modification, the inputs of the induction principle are a judgmentally commutative square

\begin{equation}
\begin{tikzcd}
\sm{y:Y} X(y) \ar[d,"{(\idfunc[Y],\beta_X)}"'] \ar[r,"N"] & \sm{y:Y}{w:\factorhit{F}{Y}{X}(y)} P(y,w) \ar[d,"\proj1"] \\
\sm{y:Y} \factorhit{F}{Y}{X}(y) \ar[r,equals] &\sm{y:Y} \factorhit{F}{Y}{X}(y)
\end{tikzcd}\label{eq:Nsq}
\end{equation}

together with a specified dependent filler for each judgmentally commutative square of the form

\[
\begin{tikzcd}[column sep=huge]
B(a) \ar[rr,"{(g\circ F_a,\mathsf{lift}(g,f,F_a(-)),f')}"] \ar[d,"{F_a}"'] && \sm{y:Y}{w:\factorhit{F}{Y}{X}(y)} P(y,w) \ar[d,"\proj1"] \\
C(a) \ar[rr,"{(g,\mathsf{lift}(g,f,-))}"'] && \sm{y:Y} \factorhit{F}{Y}{X}(y),
\end{tikzcd}
\]

while the output of the induction principle is a dependent filler in (<ref>).

If $P:\prd{y:Y} \factorhit{F}{Y}{X}(y) \to \UU$ is such that

\[\proj1 : (\sm{y:Y}{w:\factorhit{F}{Y}{X}} P(y,w)) \to \sm{y:Y} \factorhit{F}{Y}{X}\]

is right orthogonal to $F$, then

\[(-\circ \beta_X) : \Big(\prd{y:Y}{w:\factorhit{F}{Y}{X}(y)} P(y,w)\Big) \to \Big(\prd{y:Y}{x:X(y)} P(y,\beta_X(x))\Big) \]

is an equivalence.

As in <ref>, we will show that it is path-split using the induction principle of $\factorhit{F}{Y}{X}$.

First, given $h:\prd{y:Y}{x:X(y)} P(y,\beta_X(x))$, we take $P(y,w) \defeq P(y,w)$ and $N\defeq h$.
To give the remaining data $R,S$, suppose given $a:A$, $g:C(a) \to Y$, $f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))$, and $f':\prd{b:B(a)} P(g(F_a(b)),f(b))$.
Now we can apply <ref> with $l\defeq F_a$ and $f\defeq f'$: an inhabitant of (<ref>) consists exactly of the desired $R$ and $S$.

Second, given $h,k:\prd{y:Y} (\factorhit{F}{Y}{X}(y) \to P(y))$ and $p:h\circ \beta_X = k\circ \beta_X$, we take $P(y,x) \defeq (h(y,x)=k(y,x))$ and $N\defeq p$.
To give $R,S$, suppose given $a:A$, $g:C(a) \to Y$, $f:\prd{b:B(a)} \factorhit{F}{Y}{X}(g(F_a(b)))$, and

\[f':\prd{b:B(a)} h(g(F_a(b)),f(b))=k(g(F_a(b)),f(b)).\]

\begin{align*}
j(c) &\defeq h(g(c),\mathsf{lift}(g,f,c))\\
j'(c) &\defeq k(g(c),\mathsf{lift}(g,f,c))\\
q(b) &\defeq k(g(F_a(b)),f(b)).
\end{align*}

Then we can apply <ref> to the square

\[
\begin{tikzcd}
B(a) \ar[d,"F_a"'] \ar[r,"q"] & \sm{y:Y} P(y) \ar[d,"\proj1"] \\
C(a) \ar[r,"g"'] & Y.
\end{tikzcd}
\]

We have

\[ j'(F_a(b)) \jdeq k(g(F_a(b)),\mathsf{lift}(g,f,F_a(b))) = k(g(F_a(b)),f(b)) \jdeq q(b) \]

\begin{multline*}
j(F_a(b)) \jdeq h(g(F_a(b)),\mathsf{lift}(g,f,F_a(b))) = h(g(F_a(b)),f(b))\\ \overset p= k(g(F_a(b)),f(b)) \jdeq q(b),
\end{multline*}

giving two inhabitants $(j,\nameless)$ and $(j',\nameless)$ of (<ref>), which are therefore equal.
This equality consists of an equality $j=j'$, which gives precisely $R$, and an equality between the above two paths, which gives precisely $S$.

Given $F:\prd{a:A} B(a) \to C(a)$, define $\cR = F^{\perp}$ and $\cL = {}^{\perp}\cR$, and let $\hat F$ be as in <ref> and $\factorhit{\hat F}{Y}{X}$ constructed as above for $\hat F$.
Then for any $X:Y\to\UU$, the composite

\[ \Big(\sm{y:Y} X(y)\Big) \to \Big(\sm{y:Y} \factorhit{\hat F}{Y}{X}(y)\Big) \to Y \]

is an $(\cL,\cR)$-factorization.
Therefore, $(\cL,\cR)$ is an orthogonal factorization system.

By <ref>, if $\proj1$ is right orthogonal to $F$, then it is also right orthogonal to $\hat F$.
Since every function is equivalent to one of the form $\proj1$, we have $F^{\perp} = {\hat F}^{\perp}$.
Thus, since applying <ref> to $\hat F$ shows that the first factor of this factorization is in ${}^{\perp}({\hat F}^{\perp})$, it is also in ${}^{\perp}({F}^{\perp}) = \cL$.

On the other hand, the constructors $\mathsf{lift}$ and $\mathsf{islift}$ show that the second factor $\proj1 : \big(\sm{y:Y} \factorhit{\hat F}{Y}{X}(y)\big) \to Y$ of this factorization satisfies <ref><ref> for $F$, since the fibers of these maps are the types of dependent fillers against morphisms in $\hat F$.
Thus, this second factor is in $\cR$.

Finally, in <ref> we defined orthogonal factorization systems by the uniqueness of factorizations and proved from this the orthogonality of the two classes of maps; but it is easy to show that, as in classical category theory, orthogonality implies the uniqueness of factorizations when they exist, since any two factorizations must lift uniquely against each other.

§ LEFT EXACT MODALITIES

We have seen that the modal operator of any reflective subuniverse preserves products, but even for a modality it does not generally preserve pullbacks.
If it does, we call the modality “left exact” or just “lex”.

In higher topos theory, lex modalities coincide with reflective sub-toposes.
We can construct them by nullifying any family of propositions (<ref>); these correspond categorically to the “topological” localizations (in 1-topos theory, every subtopos is topological).

§.§ Lex, topological, and cotopological modalities

For a modality $\modal$, the following are equivalent.

* If $A$ is $\modal$-connected, then so is $(x=y)$ for any $x,y:A$.

* Whenever $A$ and $\sm{x:A}B(x)$ are $\modal$-connected, then so is $B(x)$ for all $x:A$.

* Any map between $\modal$-connected types is $\modal$-connected.

* Any $\modal$-modal function between $\modal$-connected types is an equivalence.

* If $f:A\to B$ is $\modal$-connected, and $g:\prd{a:A} P(a) \to Q(f(a))$ is such that $\total g:(\sm{x:A} P(x)) \to (\sm{y:B} Q(y))$ is $\modal$-connected, then $g_a:P(a)\to Q(fa)$ is also $\modal$-connected for each $a:A$.

* Given a commutative square

\begin{equation}
\begin{tikzcd}
B \ar[r,"h"] \ar[d,"g"'] & A \ar[d,"f"] \\
D \ar[r,"k"'] & C
\end{tikzcd}\label{eq:lex-commsq}
\end{equation}

in which $f$ and $g$ are $\modal$-connected, then for any $a:A$ the induced map $\hfib{h}{a} \to \hfib{k}{f(a)}$ is $\modal$-connected.

* Any commutative square (<ref>) in which $f$ and $g$ are $\modal$-connected and $h$ and $k$ are $\modal$-modal is a pullback.

* For any $f:A\to B$ and $b:B$, the evident map $\hfib{f}{b} \to \hfib{\modal f}{\modalunit b}$ is $\modal$-connected.

* For any $A$ and $x,y:A$, the induced map $\modal(x=y) \to (\modalunit[A](x) = \modalunit[A](y))$ is an equivalence.

* The functor $\modal$ preserves pullbacks.

* $\modal$-connected maps satisfy the 2-out-of-3 property.

* If $\modal f: \modal A\to \modal B$ is an equivalence, then $f$ is $\modal$-connected.

* For any $\modal$-connected type $A$ and any $P:A\to \modaltype$, there is a $Q:\modaltype$ such that $P(a)\eqvsym Q$ for all $a:A$.

When they hold, we say that $\modal$ is lex.

The equivalence <ref>$\Leftrightarrow$<ref> is easy, using the definition of $\modal$-connected maps and the fact that any function is equivalent to a fibration.
And <ref>$\Rightarrow$<ref> since $\hfib f b \jdeq \sm{a:A} (f(a)=b)$ and $\modal$-connected types are closed under $\Sigma$ (since $\modal$-connected maps are closed under composition, being the left class of a factorization system).

Condition <ref> is a special case of <ref>, since a function that is both modal and connected is an equivalence.
But assuming <ref>, if $f:A\to B$ is any function between $\modal$-connected types, then in its $(\cL,\cR)$-factorization $A\xrightarrow{e} I\xrightarrow{m} B$ the type $I$ is also connected by right cancellation.
Thus <ref> implies that $m$ is an equivalence; thus $f$, like $e$, is $\modal$-connected, giving <ref>.

Assuming <ref>, in the situation of <ref> the $3\times 3$ lemma for fiber sequences allows us to identify the fiber of $g_a$ over $q:Q(f(a))$ with the fiber over $(a,\refl{f(a)})$ of the induced map $\hfib{\total{g}}{(f(a),q)} \to \hfib{f}{f(a)}$: