sheaves.tex

\chapter{Sheaves in homotopy type theory}
\label{chap:sheaf}
\epigraph{Reductio ad absurdum, which Euclid loved so much, is one of
  a mathematician's finest weapons. It is a far finer gambit than any
  chess gambit: a chess player may offer the sacrifice of a pawn or
  even a piece, but a mathematician offers the game.}{Godfrey Harold Hardy}


In topos theory, sheafification can be seen as a way to transform a
topos into another one. It is used, for example, to build, from any
topos $\mathcal{T}$, a boolean topos (\ie{} satisfying the excluded
middle property) satisfying the axiom of choice and negating the
continuum hypothesis~\cite[Theorem VI.2.1]{maclanemoerdijk}.
This is actually an adaptation of a slightly older method, in set
theory, to change a model $\mathfrak M$ of ZFC into a model $\mathfrak
M[G]$ of ZFC, satisfying other principles, called {\em forcing}. It's
most famous application is the proof of consistency of ZFC with the
negation of the continuum hypothesis, by Paul Cohen~\cite{cohen1966},
answering (neither negatively nor positively) the first Hilbert's
problem. Indeed, Gödel proved in 1938 the consistency of ZFC with
continuum hypothesis~\cite{godel1938} using the constructible model
$\mathfrak L$.
The global idea of this technique is to add to the theory
ZFC partial information about the witness of $\lnot$CH. 
Then, supposing that ZFC is coherent, it is provable that ZFC together
with a finite number of approximation of the desired object is still
consistent. Then, the compactness theorem allows to prove the
consistency of ZFC with {\em all} approximations, \ie{} with a witness
of $\lnot$HC.

Then, forcing has been adapted to the setting of topos theory by Myles
Tierney~\cite{tierney1972}, through the notion of sheaves. Note that,
in topos theory, there are two different kind of sheaves: Grothendieck
sheaves, which only exists on a presheaf topos, and Lawvere-Tierney
sheaves. One can show that Lawvere-Tierney sheaves, when considered on
a presheaf topos, are exactly the Grothendieck sheaves; thus,
Lawvere-Tierney sheaves can be seen as a generalization of
Grothendieck sheaves.  Given a topos $\mathcal T$, one can build
another topos -- the topos of sheaves $\Sh{}(\mathcal T)$ -- together
with geometric embedding from $\Sh{}(\mathcal T)$ to $\mathcal T$
called sheafification.  Depending on the sheaves we chose to treat,
the topos $\Sh{}(\mathcal T)$ satisfies new principles. The
construction of the geometric embedding is done in \cite[Section
V.3]{maclanemoerdijk}, and briefly recalled in
section~\ref{sec:sheaf_topos}.

The development of higher topos theory (and more generally, higher
category theory) leads to wonder if a notion of sheafification still
exists in this setting. This question is answered positively
in~\cite{lurie}, where the author build a sheafification functor, but
only for Grothendieck sheaves. Surprisingly, sheafification in a higher
topos is just an iteration of the process of sheafification in topos
theory. It seems that Lawvere-Tierney sheaves were not considered in
this new setting.

Similar questions have been considered around the Curry-Howard
isomorphism, to extend a programming language close to type theory
with new logical or computational principle while keeping consistency
automatically.
%
For instance, much efforts have been done to provide a computational
content to the law of excluded middle in order to define a
constructive version of classical logic. This has lead to various
calculi, with most notably the $\lambda \mu$-calculus of
Parigot~\cite{parigot1993classical}, but this line of work has not
appeared to be fruitful to define a new version of type theory with
classical principles.
%
Other works have tried to extend continuation-passing-style (CPS)
transformation to type theory, but they have been faced with the
difficulty that the CPS transformation is incompatible with (full) dependent
sums~\cite{barthe2002cps}, which puts emphasis on the tedious link
between the axiom of choice and the law of excluded middle in type theory.
%
Nevertheless the axiom of choice has shown to be realizable by
computational meaning in a classical setting by techniques turning
around the notion of (modified) bar induction~\cite{berardi1998computational}, Krivine's
realizability~\cite{krivine2003dependent} and even more recently with
restriction on elimination of dependent sums and lazy
evaluation~\cite{herbelin2012constructive}.
The work on forcing in type theory~\cite{jaber2012extending,forcing2016} also
gives a computational meaning to a type theory enriched with new
logical or computational principle.

Section~\ref{sec:sheaf_hott} presents a definition of the
sheafification functor in the setting of homotopy type
theory. Actually, this construction is entirely complementary to
forcing in type theory, as forcing corresponds to the presheaf
construction while Lawvere-Tierney sheafification corresponds to the
topological transformation that allows to go from the presheaf
construction to the sheaf construction.

\section{Sheaves in topoi}
\label{sec:sheaf_topos}

In this section, we will work in an arbitrary topos rather than in type theory. The next section will present a
generalization of the results presented here.

Let us fix for the whole section a topos $\mathcal E$, with subobject
classifier $\Omega$. A {\em Lawvere-Tierney topology} on $\mathcal E$
is a way to modify slightly truth values of $\mathcal E$. It allows to
speak about {\em locally true} things instead of {\em true} things.

\begin{defi}[Lawvere-Tierney topology~\cite{maclanemoerdijk}]\label{defi:LT}
  A Lawvere-Tierney topology is an endomorphism $j:\Omega \to \Omega$
  preserving $\True$ ($j \ \True = \True$), idempotent ($j\circ j =
  j$) and commuting with products ($j \circ \wedge = \wedge \circ (j,j)$).
\end{defi}

A classical example of Lawvere-Tierney topology is given by double
negation. Other examples are given by Grothendieck topologies, in the
sense of the following theorem:
\begin{thm}[{\cite[Theorem V.1.2]{maclanemoerdijk}}]
  Every Grothendieck topology $J$ on a small category $\mathbf C$ determines a
  Lawvere-Tierney topology $j$ on the presheaf topos
  $\mathbf{Sets}^{\mathbf C^{\mathbf{op}}}$.
\end{thm}

Any Lawvere-Tierney topology $j$ on $\mathcal E$ induces a closure operator
$A \mapsto \closure{A}$ on subobjects. If we see a subobject $A$ of $E$
as a characteristic function $\Char{A}$, the closure $\closure{A}$
corresponds to the subobject of $E$ whose characteristic function is 
%
\[
\Char{\closure{A}} = j \circ \Char{A}.
\]%
%
A subobject $A$ of $E$ is said to
be dense when $\closure{A} = E$.

Then, we are interested in objects of $\mathcal E$ for which it is
impossible to make a distinction between objects and their dense
subobjects, \ie{} for which ``true'' and ``locally true''
coincide. Such objects are called {\em sheaves}, and are defined as

\begin{defi}[Sheaves{\cite[Section V.2]{maclanemoerdijk}}]
  On object $F$ of $\mathcal E$ is a sheaf (or $j$-sheaf) if for every
  dense monomorphism $m: A \hookrightarrow E$ in $\mathcal E$, the
  canonical map $\Hom{\mathcal E}(E,F) \rightarrow \Hom{\mathcal E}(A,F)$ is an
isomorphism.
\end{defi}

One can show that $\Sh{\mathcal E}$, the full sub-category of
$\mathcal E$ given by
sheaves, is again a topos, with classifying object
%
\[
\Omega_j = \{ P \in \Omega \ | \ j P  = P \}.
\]

Lawvere-Tierney sheafification is a way to build a left adjoint $\mathbf{a}_j$ to the
inclusion $\mathcal E \hookrightarrow \Sh(\mathcal E)$, exhibiting
$\Sh{}(\mathcal E)$ as a reflective subcategory of $\mathcal E$. In
particular, that implies that logical principles valid in $\mathcal E$
are still valid in $\Sh{}(\mathcal E)$.

For any object $E$ of $\mathcal E$, $\mathbf{a}_j(E)$ is defined as in
the following diagram
\[
  \xymatrix{ 
    E \ar[rr]^{\{\cdot\}_E} \ar@{->>}[d]_{\theta_E} && \Omega^E \ar[d]^{j^E}\\
    E' \ar@{^{(}->}[rr] \ar[dr]_{\text{closure}} && \Omega_j^E \\
    & \mathbf{a}_j(E) \ar[ur]&
  }
\]

The proof that $\mathbf a_j$ defines a left adjoint to the inclusion
can be found in~\cite{maclanemoerdijk}.

One classical example of use of sheafification is the construction,
from any topos, of a boolean topos negating the continuum
hypothesis. More precisely:

\begin{thm}[Negation of CH~{\cite[Theorem VI.2.1]{maclanemoerdijk}}]
  There exists a Boolean topos satisfying the axiom of choice, in
  which the continuum hypothesis fails.
\end{thm}

The proof actually follows almost exactly the famous proof of the
construction by Paul Cohen of a model of ZFC negating the continuum
hypothesis~\cite{cohen1966}. Together with the model of constructible
sets $\mathfrak L$ by Kurt Gödel~\cite{godel40}, it proves that CH is
independent of ZFC, solving first Hilbert's problem.


\section{Sheaves in homotopy type theory}
\label{sec:sheaf_hott}

The idea of this section is to consider sheafification in topoi as
only the first step towards sheafification in type theory. 
We note that axioms for a Lawvere-Tierney topology on the subobject
classifier $\Omega$ of a topos are very close to
those of a modality on $\Omega$. We will extensively use this idea,
applying it to every subobject classifier $\Type_n$ we described
in~\ref{sec:hott}. The subobject
classifier $\Omega$ of a topos is seen as the {\em truth values} of the
topos, which corresponds to the type $\HProp$ in our setting ; the
topos is considered proof irrelevant, corresponding to our
$\HSet$. Sheafification in topoi is thus a way, when translated to the
setting of homotopy type theory, to build, from a left-exact modality on
$\HProp$, a left-exact modality on $\HSet$. Our hope in this section
is to iterate this construction by applying it to the subobject
classifier $\HSet$ equipped with a left-exact modality, to build a new
left-exact modality on $\Type_1$, and so on. 

The first thing we can
note is that such a construction will not allow to reach every type:
it is known that there exists types with no finite truncation
level~\cite[Example 8.8.6]{hottbook}. Even worse, it seems that some types are not
even the limit of its successive truncations, even in a hypercomplete
setting~\cite{morelvv}. It suggests that defining a sheafification
functor for all truncated types won't give (at least easily) a
sheafification functor on whole $\Type$.
Another issue that can be pointed is the complexity of proofs. If, in
a topos-theoretic setting, everything is proof-irrelevant, it won't be
the case for higher settings, forcing us to prove results that were
previously true on the nose. This will oblige us to write long and
technical proofs of coherence, and more deeply, to modify completely
some lemmas, such as Proposition~\cite[Theorem IV.7.8]{maclanemoerdijk},
stating that epimorphisms are coequalizers of their kernel pair.

The main idea is thus to follow as closely as possible the
topos-theoretic construction, and change it as few times as possible to
make it work in our higher setting.

Note that the principles we want to add are added directly from the
$\HProp$ level, the extension to all truncated types is automatic. The
choice of the left-exact modality on $\HProp$ is thus crucial. For the
rest of the section, we fix one, noted $\modal_{-1}$. The reader can
think of the double negation $\modal_{\lnot\lnot}$ defined
in~\ref{ssec:notnot}. We will define, by induction on the truncation
level, left-exact modalities on all $\Type_n$, as in the following
theorem.

\begin{thm}\label{thm:main}
  The sequence defined by induction by
  \[ \begin{array}{l}
   \modal : \forall \ (n : nat), \ \Type_n \to \Type_n 
   \\
    \modal_{-1\phantom{n}}(T) \defeq \mathop{j} T \\

      \displaystyle{\modal_{n+1}(T)} \defeq  
      \displaystyle{\sum_{u:T \to \Type_n^\modal} \!\!\!\!\modal_{-1} 
      \left\|
      \sum_{a:T} u= (\lambda t,~\modal_n (a=t))
      \right\|}
    \end{array}
\]
defines a sequence of left-exact modalities, coherent with each others
in the sense that the following diagram commutes for any $P:\Type_n$,
where $\hat P$ is $P$ seen as an inhabitant of $\Type_{n+1}$.
\[ \xymatrix{
    P \ar@{->}^{\sim}[r] \ar[d]_{\eta_{n}} & \widehat P \ar[d]^{\eta_{n+1}} \\
    \modal_{n} P \ar@{->}^{\sim}[r] & \modal_{n+1} \widehat P 
  } \]
\end{thm}

\subsection{Sheaf theory}
\label{ssec:sheaves}

Let $n$ be a truncation index greater that $-1$, and $\modal_n$ be the
left-exact modality given by our induction hypothesis. As in the
topos-theoretic setting, we will define what it means for a type to be
a $n$-sheaf (or just ``sheaf'' if the context is clear), and consider
the reflective subuniverses of these sheaves ; the reflector will
exactly be the sheafification functor.
The main issue to give the ``good'' definition is the choice of the
subobject classifier in which dense subobjects will be chosen: two
choices appears, $\HProp$ and $\Type_n$ ; we will actually use
both. What guided our choice is the crucial property that the type of
all $n$-sheaves has to be a $(n+1)$-sheaf.

From the modality $\modal_n$, one can build a {\em closure operator}.

\begin{defi}[(\code{cloture},\code{closed},\code{EnJ})]
  Let $E$ be a type. 
  \begin{itemize}

  \item The {\em closure} of a subobject of $E$ with
  n-truncated homotopy fibers (or $n$-subobject of $E$, for short),
  classified by $\chi : E \to \Type_n$, is the subobject of $E$
  classified by $\modal_n \circ \chi$.

  
\item An $n$-subobject of $E$ classified by $\chi$ is said to be {\em
    closed in $E$} if it is equal to its closure, \ie{} if
  $\chi = \modal_n \circ \chi$.

  
\item An $n$-subobject of $E$ classified by $\chi$ is said to be {\em
    dense in $E$} if its closure is $E$, \ie{} if 
  $\modal_n \circ \chi = \lambda e, \one$ 
  \end{itemize}
\end{defi}


Topos-theoretic sheaves are characterized by a property of existence
and uniqueness, which will be translated, as usual, into a proof that
a certain function is an equivalence.

\begin{defi}[Restriction (\code{E\_to\_$\chi$mono\_map}, \code{E\_to\_$\chi$\_map})]
  Let $E,F:\Type$ and $\chi:E\to\Type$. We define the {\em
    restriction map} $\Phi_E^\chi$ as
  \[
    \fonction{\Phi_E^\chi}{E\to F}{\sumD e E {\chi e} \to F}{f}{f\circ \pi_1}.
  \]
\end{defi}

Here, we need to distinguish between
dense $(-1)$-subobjects, that will be used in the definition of
sheaves, and dense $n$-subobjects, that will be used in the definition
of separated types. 

\begin{defi}[Separated Type (\code{separated})]
  A type $F$ in $\Type_{n+1}$ is {\em separated} if for any type $E$, and
  all dense $n$-subobject of $E$ classified by $\chi$,
  $\Phi_E^\chi$ is an embedding.
\end{defi}

With topos theory point of view, it means that given a map $\sum_{e:E}
\chi\, e \to F$,
if there is an extension $\tilde f:E\to F$, then it is unique, as in
 \[ \xymatrix{
    \sumD e E {\chi e} \ar[r]^-f \ar[d]_{\pi_1} & F \\
    E \ar@{-->}[ru]_{!}&
  }\]
\begin{defi}[Sheaf (\code{Snsheaf\_struct})]
  A type $F$ of $\Type_{n+1}$ is a {\em $(n+1)$-sheaf} if it is
  separated, and for any type $E$ and all dense $(-1)$-subobject of
  $E$ classified by $\chi$, $\Phi_E^\chi$ is an
  equivalence.
\end{defi}

In topos-theoretic words, it means that given a map $f : \sum_{e:E}
\chi\, e\to F$, one can
extend it uniquely to $\tilde f:E \to F$, as in 
 \[ \xymatrix{
    \sumD e E {\chi e} \ar[r]^-f \ar[d]_{\pi_1} & F \\
    E \ar@{-->}[ru]_{\exists !}&
  }\]

Note that these definitions are almost the same as the ones
in~\cite{maclanemoerdijk}. The main difference is that {separated}
is defined for $n$-subobjects, while {sheaf} only for
$(-1)$-subobjects. It might seem bizarre to make such a distinction,
but the following proposition gives a better understanding of the situation.
\begin{prop}[(\code{nj\_paths\_separated})]
  A type $F$ is $\Type_{n+1}$ is separated if, and only if all its
  path types are $n$-modal, ie
  \[ \prodD {x,y} F {\left( \modal_n(x=y) \right) = (x=y)}.\]
\end{prop}

A $(n+1)$-sheaf is hence just a type satisying the usual property of sheaves
(\ie{} existence of uniqueness of arrow extension from dense
$(-1)$-subobjects), with the condition that all its path types are
$n$-sheaves. It is a way to force the compatibility of the modalities we
are defining.

One can check that the property $\issep$ (resp. $\issheaf$) is $\HProp$:
given a $X:\Type_{n+1}$, there is at most one way for it to be separated
(resp. a sheaf). In particular, when needed to prove equality between
two sheaves, it suffices to show the equality between the underlying
types.

As said earlier, these definitions allow us to prove the fundalemental
property that the type of all $n$-sheaves is itself a $(n+1)$-sheaf
(this can be viewed as an equivalent definition of left-exactness).

\begin{prop}[(\code{nType\_j\_Type\_is\_SnType\_j\_Type})]
\label{prop:sheaf-is-sheaf}
  $\Type_n^\modal$ is a $(n+1)$-sheaf.
\end{prop}

\begin{proof}
  We have two things to prove here : separation, and sheafness.
  \begin{itemize}
  \item Let $E:\Type$ and $\chi:E\to\Type$, dense in $E$. 
    Let $\phi_1,\phi_2:E \to
    \Type_n^\modal$, such that $\phi_1 \circ \pi_1 = \phi_2 \circ
    \pi_1$ and let $x:E$. We show $\phi_1(x) = \phi_2(x)$ using
    univalence.
    
    As $\chi$ is dense, we have a term $m_x : \modal_n(\chi\, x)$.
    But as $\phi_2(x)$ is modal, we can obtain a term $h_x : \chi\,
    x$. 
    As $\phi_1$ and $\phi_2$ are equal on $\sumD e E {\chi\, e}$, we
    have an arrow $\phi_1(x) \to \phi_2(x)$.
    The same method leads to an arrow $\phi_2 (x) \to \phi_1 (x)$, and
    one can
    prove that they are each other inverse.
  \item Now, we prove that $\Type_n^\modal$ is a sheaf. Let $E:\Type$ and
  $\chi:E \to \HProp$, dense in $E$. Let $f:\sum_{e:E} \chi\, e \to
  \Type_n^\modal$. We want to extend $f$ into a map $E \to \Type_n^\modal$.

  We define $g$ as $g(e) = \modal_n \left( \fib \phi {e} \right)$,
  where
  \[ \phi : \sum_{b:\sumD e E {\chi\, e}} (f\,
    b) \to E\]
  defined by $\phi(x) = (x_1)_1$.
  Using the following lemma, one can prove that the map $f\mapsto g$
  defines an inverse of $\Phi_E^\chi$.
  \begin{lem}[(\code{nj\_fibers\_compose})]
    Let $A,B,C:\Type_n$, $f:A\to B$ and $g:B\to C$.
    Then
    if all fibers of $f$ and $g$ are $n$-truncated, then
      \[\prodD c C {\left( \modal_n(\fib {g \circ f} c) \right) \simeq
      \modal_n \left(  
        \sumD w {\fib g c} {\modal_n (\fib f {w_1})}
      \right)}.\]
  \end{lem}
  \begin{prooflem}
    This is just a modal counterpart of the property characterizing
    fibers of composition of function.
  \end{prooflem}
  \end{itemize}
\end{proof}

Another fundamental property on sheaves we will need is that the type of (dependent)
functions is a sheaf as soon as its codomain is a sheaf.

\begin{prop}[(\code{dep\_prod\_SnType\_j\_Type})]
\label{prop:sheaf-forall}
  If $A:\Type_{n+1}$ and $B:A \to \Type_{n+1}$ such that for any
  $a:A$, $(B~a)$ is a sheaf, then $\prodD a A {B\, a}$ is a sheaf.
\end{prop}
\begin{proof}
  Again, when proving equivalences, we will only define the maps. The
  proofs of section and retraction are technical, not really
  interesting, and present in the formalisation.
  \begin{itemize}
  \item {\em Separation:} Let $E:\Type$ and $\chi:E \to \Type_n$ dense
    in $E$. Let $\phi_1,\phi_2:E\to \prodD a A {B\, a}$ equal on
    $\sumD e E{\chi\, e}$ \ie{} such that $\phi_1\circ \pi_1 = \phi_2\circ
    \pi_1$.
    Then for any $a:A$, $(\lambda x:E,~\phi_1(x, a))$
    and $(\lambda x:E,~\phi_2(x,a))$
    coincide on $\sum_{e:E}(\chi\, e)$, and as $B\, a$ is separated,
    they coincide also on all $E$.
  \item {\em Sheaf:} Let $E:\Type$, $\chi:E\to \HProp$ dense in $E$ and
    $f:\sumD e E {\chi\, e}\to \prodD a A{B\,a}$. Let $a:A$ ; the
    map $(\lambda x,~f(x,a))$ is valued in the sheaf $B\, a$, so it
    can be extended to all $E$, allowing $f$ to be extended to all
    $E$.
  \end{itemize}
\end{proof}

\subsection{Sheafification}
\label{ssec:sheafification}

The sheafification process will be defined in two steps. The first
one will build, from any $T:\Type_{n+1}$, a separated object $\separated
T:\Type_{n+1}$ ; one can show that $\separated$ defines a modality on
$\Type_{n+1}$. The second step will build, from any separated type
$T:\Type_{n+1}$, a sheaf $\modal_{n+1}(T)$ ; one can show that
$\modal_{n+1}$ is indeed the left-exact modality we are searching.

Let $n$ be a fixed truncation index, and $\modal_n$ a left-exact
modality on $\Type_n$, compatible with $\modal_{-1}$ as in
\begin{cond}\label{cond:hprop}
  For any mere proposition $P$ (where $\widehat P$ is $P$ seen as a
  $\Type_n$),  $\modal_n \widehat P = \modal_{-1} P$ and the
  following coherence diagram commutes
  \[\xymatrix{
    P \ar@{->}^{\sim}[r] \ar[d]_{\eta_{-1}} & \widehat P \ar[d]^{\eta_n} \\
    \modal_{-1} P \ar@{->}^{\sim}[r] & \modal_n \widehat P 
  }\]
\end{cond}

\subsubsection{From types to separated types}
\label{sssec:type_to_sep}


Let $T : \Type_{n+1}$. We define $\separated T$ as the image of
$\modal_n^T \circ \{\cdot\}_T$, as in
\[\xymatrix{
    T \ar[r]^{\{\cdot\}_T} \ar[d]_{\mu_T} & \left(\Type_n\right)^T \ar[d]^{\modal_n^T} \\
  \separated T \ar[r]& \left( \Type_n^\modal \right)^T
}, \]%
where $\{\cdot\}_T$ is the singleton map $\lambda (t:T),~\lambda
(t':T),~t=t'$. 
%
$\separated T$ can be given explicitly by
%
\begin{align*}
\separated T &\defeq \im (\lambda~t:T,~\lambda~ t',~ \modal_n (t = t')) \\
          &\defeq \sumD u{T \to \Type_n^\modal} {\left\| \sumD a A
            {(\lambda t,~\modal_n (a=t)) = u}\right\|}.
\end{align*}
%
This corresponds to the free separated object used in the topos-theoretic construction, but using $\Type_n^\modal$ instead of the
$j$-subobject classifier $\Omega_j$.
%
\begin{prop}[(\code{separated\_Type\_is\_separated})]
  For any $T:\Type_{n+1}$, $\separated T$ is separated.  
\end{prop}

\begin{proof}
We use the following lemma:
\begin{lem}[(\code{separated\_mono\_is\_separated})]
\label{lem:embed-sep}
  A $(n+1)$-truncated type $T$ with an embedding $f : T \to U$
  into a separated $(n+1)$-truncated type $U$ is itself separated.
\end{lem}
\begin{prooflem}
  Let $E:\Type$ and $\chi:E\to\Type_n$ dense in $E$. Let
  $\phi_1,\phi_2:\sumD e E {\chi\, e} \to T$ such that $\phi_1 \circ
  \pi_1 \homot \phi_2 \circ \pi_1$. Postcomposing by $f$ yields an homotopy $f \circ \phi_1 \circ
  \pi_1 \homot f \circ \phi_2 \circ \pi_1$. As $f\circ\phi_1,f\circ
  \phi_2 : \sumD e E {\chi\, e} \to U$, and $U$ is separated, we can
  deduce $f \circ \phi_1 \homot f \circ \phi_2$. As $f$ is an
  embedding, $\phi_1 \homot \phi_2$.
\end{prooflem}
As $\separated T$ embeds in $\left( \Type_n^\modal \right)^T$, we only
have to show that the latter is separated. But it is the case because
$\Type_n^\modal$ is a sheaf (by Proposition~\ref{prop:sheaf-is-sheaf})
and a function type is a sheaf as soon
as its codomain is a sheaf (by Proposition~\ref{prop:sheaf-forall}).
\end{proof}

We will now show that $\separated$ defines a modality, with unit map
$\mu$. The left-exactness of $\modal_{n+1}$ will come from the second
part of the process.
The first thing to show that $\separated T$
is universal among separated type below $T$. 
In the topos-theoretic sheafification, it comes easily from the fact
that epimorphims are coequalizers of their kernel pairs. As it is not
true anymore in our setting, we will use its generalization,
proposition~\ref{prop:cech}.
Here is a sketch of the proof:
as $\mu_T$ is a surjection (it is defined by the surjection-embedding
factorization), $\separated T$ is the colimit of its iterated kernel
pair. Hence, for any type $Q$ defining a cocone on $\KP(\mu_T)$, there
is a unique arrow $\separated T\to Q$. What remains to show is any
separated type $Q$ defines a cocone on $\KP(\mu_T)$ ; we will actually
show that any separated type $Q$ defines a cocone on
$\|\KP(\mu_T)\|_{n+1}$, which is enough. We do it by
defining another diagram $\mathring T$, equivalent to $\|\KP(\mu_T)\|_{n+1}$, for
which it is easy to define a cocone into any separated type $Q$.


This comes from the
following construction which connects $\separated T$ to the colimit of
the iterated kernel pair of $\mu_T$.

\begin{defi}[(\code{OTid})]
  Let $X:\Type$. Let $\mathring T_X$ be the higher inductive type
  generated by
  \begin{itemize}
  \item $\mathring t:~\|X\|_{n+1} \to \mathring T_X$
  \item $\mathring \alpha:~\forall a\, b:\|X\|_{n+1},~\modal (a=b) \to
    \mathring t(a) = \mathring t(b)$
  \item $\mathring \alpha_1:~\forall a:\|X\|_{n+1},~
    \mathring \alpha(a , a, \eta_{a=a} 1) = 1$
  \end{itemize}

  We view $\mathring T$ as the coequalizer of
  \[
    \xymatrix{\displaystyle{\sumD {a,b}{\|X\|_{n+1}} {\modal (a=b)}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1}
      & \|X\|_{n+1}
    }\]%
  preserving $\eta_{a=a} 1$.

  We consider the diagram $\mathring T$ :
  \[\xymatrix{\|X\|_{n+1} \ar[r] & \|\mathring T_{X}\|_{n+1} \ar[r] & \|\mathring
  T_{\mathring T_X} \|_{n+1} \ar[r] & \cdots} \]%
\end{defi}


The main result we want about $\mathring T$ is the following:
\begin{lem}[(\code{separation\_colimit\_OTtelescope})]
\label{lem:sepiscolim}
  Let $T:\Type_{n+1}$. Then $\separated T$ is the $(n+1)$-colimit of the
  diagram $\mathring T$.
\end{lem}

The key point of the proof is that diagrams $\mathring T$ and $\|\KP(\mu_T)\|_{n+1}$
are equivalent.
We will need the following lemma:

\begin{lem}[(\code{OT\_Omono\_sep})]
\label{lem:Omono}
  Let $A,S:\Type_{n+1}$, $S$ separated, and $f:A \to S$. Then if 
  \begin{equation}
    \label{eq:Omono}
    \forall a,b:A,~f (a) = f (b) \simeq \modal (a=b),
  \end{equation}
  then
  \[\forall a,b:\|\KP_f\|_{n+1},~|\tilde f|_{n+1} (a) = |\tilde f|_{n+1} (b) \simeq \modal (a=b).\]
\end{lem}

\begin{proof}[Sketch of proof]
  By induction on truncation, we need to show that 
  \[\forall a,b:\KP_f,~\tilde f (|a|_{n+1}) = \tilde f (|b|_{n+1} )\simeq
  \modal (|a|_{n+1}=|b|_{n+1}).\]%
  We use the encode-decode~\cite[Section 8.9]{hottbook} method to characterize $\tilde f (|a|_{n+1})
  = x$, and the result follows. We refer to the formalization for details.
\end{proof}

This lemmas allows to prove that, in the iterated kernel pair diagram
of $f$
\[
  \xymatrix{
    X \ar[r] \ar[rrd]_f & \KP(f) \ar[r] \ar[rd]^{f_1} & \KP(f_1)
    \ar[r] \ar[d]_{f_2} & \KP(f_2) \ar[r] \ar[ld]^{f_3}& \cdots \\
    && S &&
  }
\]
if $f$ satisties~\ref{eq:Omono}, then each $|f_i|_{n+1}$ does.

\begin{rmq}
It is clear that if $A$ and $B$ are equivalent types, and $\forall a,b:A,~f (a) = f (b) \simeq \modal
(a=b)$, then 
\[
    \mathrm{Coeq}_1 \left( 
      \xymatrix{
        \displaystyle{\sumD {a,b} A {f a = f b}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1} & A
      }
    \right)
    \simeq \mathrm{Coeq}_1 \left( 
      \xymatrix{\displaystyle{\sumD {a,b} B {\modal (a=b)}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1} & B}
    \right)
  \]
\end{rmq}

\begin{proof}[Proof of lemma~\ref{lem:sepiscolim}]
  As said, it suffices to show that $\|C(\mu_T)\|_{n+1} =
  \mathring T$.

  \[
    \xymatrix{%
     \|\KP^0(\mu_T)\|_{n+1} \ar[r] \ar[d]^*[@]{\hbox to 0pt{\hss$\sim$\hss}}&
     \|\KP^1(\mu_T)\|_{n+1} \ar[r] \ar[d]^*[@]{\hbox to
       0pt{\hss$\sim$\hss}} & 
     \|\KP^2(\mu_T)\|_{n+1} \ar[r] \ar[d]^*[@]{\hbox to
       0pt{\hss$\sim$\hss}} & \cdots \\
     \mathring T_0 \ar[r] & \mathring T_1 \ar[r] &  \mathring T_2
     \ar[r] &\cdots
    }
  \]
  The first equivalence is trivial. Let's then start with the
  second. What we need to show is
  \[ \|\KP(\mu_T)\|_{n+1} \simeq \|\mathring T_T\|_{n+1}, \]
  \ie{}
  \[
    \mathrm{Coeq}_1 \left( 
      \xymatrix{
        \displaystyle{\sumD {a,b} T {\mu_T a = \mu_T b}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1} & T
      }
    \right)
    \simeq \mathrm{Coeq}_1 \left( 
      \xymatrix{\displaystyle{\sumD {a,b} T{\modal (a=b)}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1} & T}
    \right).
  \]
  
  By the previous remark, it suffices to show that $\mu_T$ satisfies condition~(\ref{eq:Omono}),
  \ie{} $\forall a,b:T$, $\modal_n (a=b) = (\mu_T a =
  \mu_T b)$. By univalence, we want arrows in both ways, forming an
  equivalence.
  \begin{itemize}
  \item Suppose $p : (\mu_T a = \mu_T b)$. Then projecting $p$ along
    first components yields $q : \prodD t T {\modal_n(a=t)} = \modal_n (b=t)
    $.
    Taking for example $t=b$, we deduce $\modal_n (a=b) = \modal_n(b=b)$,
    and the latter is inhabited by $\eta_{b=b} 1$.
  \item Suppose now $p : \modal_n(a=b)$. Let $\iota$ be the first
    projection from $\separated T \to (T \to \Type_n^\modal)$. $\iota$ is
    an embedding, thus it suffices to prove $\iota (\mu_T a) = \iota
    (\mu_T b)$, \ie{} $\prodD t T{\modal_n (a=t) = \modal_n (b=t)}$. The latter
    remains true by univalence.
  \end{itemize}
  The fact that these two form an equivalence is technical, we refer to
  the formalization for an explicit proof.


  Let's show the other equivalences by induction. Suppose that, for a
  given $i:\N$, $\|\KP^i(\mu_T)\|_{n+1} \simeq \mathring T_i$. We want
  to prove $\|\KP^{i+1}(\mu_T)\|_{n+1} \simeq \mathring T_{i+1}$, \ie{}

  \[
    \begin{split}
    \left\|\mathrm{Coeq}_1 \left( 
      \xymatrix{
        \displaystyle{\sumD {a,b}{\KP^i(\mu_T)} {f_{i} a = f_{i} b}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1} & \KP^i(\mu_T)
      }
    \right)\right\|_{n+1}
    \\ \simeq 
    \left\|\mathrm{Coeq}_1 \left( 
      \xymatrix{\displaystyle{\sumD {a,b} {\|\mathring T_i\|_{n+1}} {\modal (a=b)}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1} & \|\mathring T_i\|_{n+1}}
    \right)\right\|_{n+1}
    \end{split}
  \]
  where $f_{i}$ is the map $\KP^i(\mu_T) \to \separated T$. But
  lemma~\ref{lem:Omono} just asserted that $f_i$
  satisfies~\ref{eq:Omono}, hence the previous nota yields the result.
  
  One would need to show that, modulo these equivalences, the arrows
  of the two diagrams are equal. We leave that to the reader, who can
  refer to the formalization if needed.
\end{proof}

Now, let $Q$ be any separated $\Type_{n+1}$, and $f:X \to Q$. Then the
following diagram commutes

\[\xymatrix{
\|X\|_{n+1} \ar[r] \ar[rd] & \|\mathring T_{X}\|_{n+1} \ar[r] \ar[d] & \|\mathring
  T_{\mathring T_X} \|_{n+1} \ar[ld] \ar[r] & \cdots \\
  & Q &&
} \]% 

But we know (lemma~\ref{lem:sepiscolim}) that $\separated T$ is the
$(n+1)$-colimit of the diagram $\mathring T$, thus there is an universal
arrow $\separated T \to Q$.
%
This is enough to state the following proposition.
\begin{prop}[(\code{separation\_reflective\_subuniverse})]
\label{prop:sep-subu}
  $(\separated,\mu)$ defines a reflective subuniverse on $\Type_{n+1}$.
\end{prop}

To show that $\separated$ is a modality, it remains to show that
separation is a property stable under sigma-types.
%
Let $A:\Type_{n+1}$ be a separated type and $B:A \to \Type_{n+1}$ be a
family of separated types. We want to show that $\sumD x A {B\, x}$ is separated. Let $E$
be a type, and $\chi:E\to\Type_n$ a dense subobject of E.

Let $f,g$ be two maps from $\sumD e E {\chi\,e}$ to $\sumD x A
{B\, x}$, equal when precomposed with $\pi_1$.
\[\xymatrix @R=4em @C=4em{
  \sumD e E {\chi\, e} \ar@<-2pt>[r]_{g\circ\pi_1}
  \ar@<2pt>[r]^{f\circ \pi_1} \ar[d]_{\mathrm{dense}}& \sumD x A {B\, x} \\
  E \ar@<-2pt>[ru]_{g} \ar@<2pt>[ru]^{f}&
}\]%
We can restrict the previous diagram to 
\[\xymatrix @R=4em @C=5em{
  \sumD e E {\chi\, e} \ar@<-2pt>[r]_{\pi_1\circ g\circ\pi_1} \ar@<2pt>[r]^{\pi_1\circ f\circ \pi_1} \ar[d]_{\mathrm{dense}}& A \\
  E \ar@<-2pt>[ru]_{\pi_1\circ g} \ar@<2pt>[ru]^{\pi_1\circ f}&
}\]%
and as $A$ is separated, $\pi_1\circ f = \pi_1 \circ g$.
For the second components, let $x:E$. Notice that 
$\sumD y E {x = y}$ has a dense $n$-subobject, $\sumD y {\sumD e E {\chi\,
  e}} {x=y_1}$:

\[\xymatrix@C=8em@R=4em{
  \sumD y {\sumD e E {\chi\,
  e}} {x=y_1} \ar@<2pt>[r]^{\qquad \pi_2\circ f\circ\pi_1\circ \pi_1}
\ar@<-2pt>[r]_{\qquad \pi_2\circ g\circ \pi_1\circ \pi_1}
\ar[d]_{\mathrm{dense}}& B\,x \\
  \sumD y E {x = y} \ar@<2pt>[ur]^{\pi_2\circ f\circ \pi_1} \ar@<-2pt>[ur]_{\pi_2\circ g\circ \pi_1}&
}\]%
Using the separation property of $B\,x$, one can show that second
components, transported correctly along the first components equality,
are equal. The complete proof can be found in the formalization.
This proves the following proposition
\begin{prop}[(\code{separated\_modality})]
\label{prop:sep-mod}
  $(\separated,\mu)$ defines a modality on $\Type_{n+1}$.
\end{prop}

As this modality is just a step in the construction, we do not need to
show that it is left exact, we will only do it for the sheafification
modality.

\subsubsection{From Separated Type to Sheaf}
\label{sssec:separated-to-sheaf}

%\nt{put the definition of $\modal_{n+1}$ upfront}
For any $T$ in $\Type_{n+1}$, 
$\modal_{n+1}T$ is defined as the closure of $\separated T$,
seen as a subobject of $T \to \Type_n^\modal$. 
%
$\modal_{n+1}T$ can be given explicitly by
\[
\modal_{n+1} T \ \defeq \sum_{u:T \to \Type_n^\modal} \modal_{-1}\left\| \sum_{a:T} 
            (\lambda t,~\modal_n (a=t)) = u\right\|.
\]%

To prove that $\modal_{n+1} T$ is a sheaf for any $T:\Type_{n+1}$, we
use the following lemma.
\begin{lem}[(\code{closed\_to\_sheaf})]
  Any closed $(-1)$-subobject of a sheaf is a sheaf.
  % Let $X:\Type_{n+1}$ and $U$ be a sheaf. If $X$ embeds
  % in $U$, and is closed in $U$, then $X$ is a sheaf.
\end{lem}
\begin{proof}
  Let $U$ be a sheaf, and $\kappa:U\to \HProp$ be a closed
  $(-1)$-subobject. 
  Let $E:\Type$ and
  $\chi:E\to\HProp$ dense in $E$. Let $\phi:\sumD e E {\chi\, e} \to
  \sumD u U {\kappa\, u}$. As $\pi_1 \circ \phi$ is a map $\sumD e E
  {\chi\, e} \to U$ and $U$ is a sheaf, it can be extended into
  $\psi:E\to U$. As $\kappa$ is closed, it suffices now to prove
  $\prodD e E {\modal_n(\kappa\, (\psi\, e))}$ to obtain a map
  $E\to\sumD u U {\kappa\, u}$.

  Let $e:E$. As $\chi$ is dense, we have a term $w:\modal_n(\chi\,e)$,
  and by $\modal_n$-induction, a term $\widetilde w:\chi\, e$.
  Then, by retraction property, $\psi(e) = \phi(e,\widetilde w)$, and by $\pi_2
  \circ \phi$, we have hence our term of type $\kappa(\psi\, e)$.



  % Let $f:X\to U$ be the considered embedding. We have already seen in
  % lemma~\ref{lem:embed-sep} that, as $U$ is separated, $X$ is too.

  % Let $E:\Type$ and
  % $\chi:E\to\HProp$ dense in $E$. Let $\phi:\sumD e E {\chi\, e} \to
  % X$. Then $f\circ \phi$ can be extended to a map $g:E\to U$.
\end{proof}
As $T\to \Type_n^\modal$ is a sheaf, and $\modal_{n+1}T$ is closed in
$T\to \Type_n^\modal$, $\modal_{n+1}T$ is a sheaf. We now prove that
it forms a reflective subuniverse.

\begin{prop}[(\code{sheafification\_subu})]
  $(\modal_{n+1},\nu)$ defines a reflective subuniverse.
\end{prop}
\begin{proof}
  Let $T,Q:\Type_{n+1}$ such that $Q$ is a sheaf. Let $f:T\to Q$.
  Because $Q$ is a sheaf, it is in particular separated;
  % 
  thus we can extend $f$ to $\separated f:\separated T\to Q$.

  But as $\modal_{n+1} T$ is the closure of $\separated T$, $\separated T$ is dense
  into $\modal_{n+1} T$, so the sheaf property of $Q$ allows to extend
  $\separated f$ to $\modal_{n+1} f:\modal_{n+1} T \to Q$.

  As all these steps are universal, the composition is.
\end{proof}

% Using the same technique as in proposition~\ref{prop:sep-mod}, we
% have
The next step is the closure under dependent sums, to state:
\begin{prop}[(\code{sheafification\_modality})]
  $(\modal_{n+1},\nu)$ defines a modality.
\end{prop}
\begin{proof}
  The proof uses the same ideas as in
  subsection~\ref{sssec:type_to_sep}. Let $A:\Type_{n+1}$ a sheaf and
  $B:A\to\Type_{n+1}$ a sheaf family. By
  proposition~\ref{prop:sep-mod}, we already know that $\sumD a A {B\,
    a}$ is separated. Let $E$ be a type, and $\chi:E\to \HProp$ a
  dense subobject. Let $f:\sumD e E {\chi\, e} \to \sumD x A {B\, x}$
  ; we want to extend it into a map $E\to \sumD x A {B\, x}$.

  \[
    \xymatrix{
      \sumD e E {\chi\, e} \ar[r]^f \ar[d] & \sumD x A {B\, x} \\
      E \ar@{.>}[ru]&
    }
  \]

  As $A$ is a sheaf, and $\pi_1\circ f:\sumD e E {\chi\, e}
  \to A$, wa can recover an map $g_1:E \to A$. We then want to show
  $\prodD e E {B(g_1\, e)}$. Let $e:E$. As $\chi$ is dense, we have a
  term $w:\modal_n(\chi\, e)$, and as $B(g_1\, e)$ is a sheaf, we can
  recover a term $\widetilde w:\chi\, e$. Then $g_1(e) =
  f(e,\widetilde w)$, and $\pi_2\circ f$ gives the result.
\end{proof}

It remains to show that $\modal_{n+1}$ is left exact and is compatible
with $\modal_{-1}$. To do that, we need to extend the notion of
compatibility and show that actually every modality $\modal_{n+1}$ is
compatible with $\modal_n$ on lower homotopy types.
\begin{prop} \label{prop:compatibility}
  If $T:\Type_n$, then $\modal_{n+1} \widehat T = \modal_n T$, where $\widehat T$ is $T$ seen as a
  $\Type_{n+1}$.
\end{prop}
\begin{proof}
  We prove it by induction on $n$:
  \begin{itemize}
  \item For $n=-1$: Let $T:\HProp$. Then
    \begin{align*}
      \modal_{0} \widehat T &\defeq \sum_{u:T \to \Type_n^\modal} \modal_{-1}\left\| \sum_{a:T} 
      (\lambda t,~\modal_{-1} (a=t)) = u\right\|_{-1} \\
      &= \sum_{u:T \to \Type_n^\modal} \modal_{-1}\left( \sum_{a:T} 
      (\lambda t,~\modal_{-1} (a=t)) = u\right)
    \end{align*}
    because the type inside the truncation is already in $\HProp$.
    Now, let define $\phi : \modal_{-1} T \to \modal_0T$ by
    \[\phi t = (\lambda t',\, \one
      ;\kappa)\]%
    where $\kappa$ is defined by $\modal_{-1}$-induction on
    $t$. Indeed, as $T$ is an $\HProp$, $(a=t) \simeq \one$. 
    Let $\psi : \modal_0T\to \modal_{-1} T$ by obtaining the
    witness $a:T$ (which is possible because we are trying to inhabit
    a modal proposition), and letting $\psi (u;x) = \eta_T a$.
    These two maps form an equivalence (the section and retraction are
    trivial because the equivalence is between mere propositions).
  \item Suppose now that $\modal_{n+1}$ is compatible with all $\modal_k$ on
    lower homotopy types. Let $\modal_{n+2}$ be as above, and let
    $T:\Type_{n+1}$. Then, as $\modal_{n+1}$ is compatible with $\modal_{n}$, and
    $(a=t)$ is in $\Type_n$,
    \[
      \modal_{n+2} \widehat T= \hspace{-1em} \sum_{u:T \to
        \Type_{n+1}^\modal} 
      \hspace{-1em} \modal_{-1}\left\| \sum_{a:T} 
        (\lambda t,~\modal_{n} (a=t)) = u\right\|_{-1}.
    \]%
    It remains to prove that for every $(u,x)$ inhabiting the
    $\Sigma$-type above, $u$ is in $T\to\Type_n^\modal$, \ie{} that for
    every $t:T$, $\IsType n (u\, t)$.  But for any truncation index
    $p$,
    the type $\IsType p X:\HProp$ is a sheaf as soon as $X$ is, so we can get rid
    of $\modal_{-1}$ and of the truncation, which tells us that for
    every 
    $t:T$, $u\, t = \modal_n(a=t) : \Type_n$. \qedhere
  \end{itemize}
\end{proof}
This proves in particular that $\modal_{n+1}$ is compatible with
$\modal_{-1}$ in the sense of condition~\ref{cond:hprop}.

The last step is the left-exactness of $\modal_{n+1}$. Let $T$ be in
$\Type_{n+1}$ such that $\modal_{n+1} T$ is contractible.  Thanks to the just
shown compatibility between $\modal_{n+1}$ and $\modal_n$ for
$\Type_n$, left exactness means that for any $x,y: T$,
$\modal_n(x=y)$ is contractible.

Using a proof by univalence as we have done for proving $\modal_n (a=b) \simeq (\mu_T(a) =
\mu_T (b))$ in Proposition~\ref{lem:sepiscolim}, we can show that:
\begin{prop}[(\code{good\_sheafification\_unit\_paths\_are\_nj\_paths})]
  For all $a,b:T$, $\modal_n(a=b) \simeq (\nu_T a = \nu_T b)$.
\end{prop}

As $\modal_{n+1} T$ is contractible, path spaces of $\modal_{n+1} T$ are
contractible, in particular $(\nu_T a=\nu_T b)$, which proves left
exactness.

\subsection{Summary}
\label{ssec:summary}

Starting from any left-exact modality $\modal_{-1}$ on $\HProp$, we
have defined for any truncation level $n$, a new left-exact modality
$\modal_n$ on $\Type_n$, which corresponds to $\modal_{-1}$ when
restricted to $\HProp$.


When $\modal_{-1}$ is consistent (in the sense of
proposition~\ref{prop:consistent}), 
$\modal_{n}\zero=\modal_{-1}\zero$ is also not inhabited, hence
$\modal_n$ is consistent. 
%
In particular, the modality induced by the double negation modality on
$\HProp$ is consistent.

In topos theory, the topos of Lawvere-Tierney sheaves for the double
negation topology is a boolean topos. In homotopy type theory, this
result can be expressed as:

\begin{prop}
  Taking $(\modal_{\lnot\lnot})_n$, the modality obtained by
  sheafification of the double negation modality,
  the following holds
  \[
    \prodD P {\HProp} {\modal_{\lnot\lnot} (P + \lnot P)}.
  \]
\end{prop}
\begin{proof}
 Let $P:\HProp$, and pose $Q \defeq P + \lnot P$. Then, as
  $P$ and $\lnot P$ are disjoint h-propositions, $P + \lnot P$ is
  itself a h-proposition~\cite[\texttt{ishprop\_sum}]{hottlib}.
  Thus, $\modal_{\lnot\lnot} Q \simeq \lnot\lnot Q$, and the latter is
  inhabited by the usual
  \[
    \lambda\, (x:\lnot Q),\, x(\inr (\lambda\, y:P,\, x(\inl y))).
  \]
\end{proof}


% Combined with forcing in type theory~\cite{jaber2012extending}, it
% should be possible to lift the proof of independence of the continuum
% hypothesis to a classical setting, which is where the continuum hypothesis is
% really meaningful.  However, we haven't worked out the details and left
% this for future work.


\subsection{Extension to Type}
\label{ssec:extension-type}

In the previous section, we have defined a (countably) infinite family of
modalities $\Type_i \to \Type_i$. One can extend them to whole
$\Type$ by composing with truncation:

\begin{lem}\label{lem:type}
  Let $\modal_i:\Type_i \to \Type_i$ be a modality. Then $\modal
  \defeq \modal_i
  \circ \|\cdot\|_i : \Type \to \Type$ is a modality in the sense
  of section~\ref{sec:modalities}
\end{lem}

If $\modal_{-1}$ is the double negation modality on $\HProp$ and
$i=-1$, $\modal$ is exactly the double negation modality on $\Type$
described in~\ref{ssec:notnot}.
Chosing $i\geqslant 0$ is a refinement of this double negation
modality on $\Type$: it will collapse every type to a $\Type_i$,
instead of an $\HProp$.

Obviously, as truncation modalities are not left-exact~\cite[Exercise
7.11]{hottbook}, $\modal$ isn't either. But in the following sense, when
restricted to $i$-truncated types, it is:
\begin{lem}
  Let $A:\Type_i$. Then if $\modal(A)$ is contractible, for any $x,y:A$,
  $\modal(x=y)$ is contractible.
\end{lem}
\begin{proof}
  For $i$-truncated types, $\modal = \modal_i$, and $\modal_i$ is left-exact.
\end{proof}

The compatibility between the modalities $\modal_n$ and between the
modalities $\|\cdot \|_n$ allow us to chose the truncation index as
high as desired.
Taking it as a non-fixed parameter allows to work in an
universe where the new principle ({\em e.g.} mere excluded middle) is
true for any explicit truncated type. Indeed, $i$ can be chosen
dynamically along a proof, and thus be increased as much as needed,
without changing results for lower truncated types.

% By proposition~\ref{prop:consistent}, these left-exact modalities
% induces a consistent type theory. 
Furthermore, the univalence remains
true in this new type theory in the following sense:
\begin{prop}\label{prop:univalence}
  Let $n$ be a given truncation index, and $\modal$ the modality
  associated to $n$ as defined in lemma~\ref{lem:type}. Then, for
  any type $A,B:\Type_n^\modal$, if $\varphi$ is the canonical arrow
  $$A = B \to A\simeq B,$$
  then $\IsEquiv(\varphi)$ is modal.
\end{prop}
\begin{proof}
  The first thing to notice is that, if $X$ and $Y$ are modal, and
  $f:X \to Y$, then the mere proposition $\IsEquiv f$ is also modal.
  Therefore, it suffices to show that both $A=B$ and $A\simeq B$ are
  modal. By proposition~\ref{prop:mod_prop}, $A=B$ is modal. 
  Moreover, $(A\simeq B) \simeq \sum_{f:A\to B} \IsEquiv
  f$. Therefore, as $A$ and $B$ are modal, $A\simeq B$ is too. 

  Hence, $\IsEquiv \varphi$ is modal.
\end{proof}

We can view sheafification in terms of model of type theory but
because of the resulting modality on $\Type$ is not left exact, we
need to restrict ourselves to a type theory with only one universe.
%
Let $\mathfrak M$ be a model of homotopy type theory with one
universe.
%
Using the modality $\modal_{\lnot \lnot}$ (for any level $n$) associated to the
sheafification, there is a model $\modal_{\lnot \lnot} \mathfrak M$ of type theory
with one universe (using results in
Section~\ref{sec:translation}), where excluded middle is true, and
which is univalent (as shown in Proposition~\ref{prop:univalence}).
%

\section{Formalization}
\label{sec:sheaf-formalization}

A Coq formalization of the sheafification process based on the
Coq/HoTT library~\cite{hottlib} is available at
\url{https://github.com/KevinQuirin/sheafification}.

After reviewing the content and some statistics about the
formalization in Section~\ref{ssec:cont-form}, we present the
limitations of our formalization in Section~\ref{ssec:limit-form}, in
particular the issues relative to universe polymorphism. 

\subsection{Content of the formalization}
\label{ssec:cont-form}

We provide a more detailed insight of the structure of our formalization:
\begin{itemize} 
\item Colimits and iterated kernel pairs are formalized in
\texttt{Limit}, \texttt{T.v}, \texttt{OT.v}v \texttt{OT\_Tf.v}, \texttt{T\_telescope.v},\\ \texttt{Tf\_Omono\_sep.v}.% (552 lines).
\item
Reflective subuniverses and modalities are formalized in\\
\texttt{reflective\_subuniverse.v}, \texttt{modalities.v}. % (1053 lines).
\item 
%
  The definition of the dense topology as a left exact modality on
  $\HProp$ is given in \texttt{sheaf\_base\_case.v}. % (186 lines).
\item
Section~\ref{ssec:sheaves} is formalized in
\texttt{sheaf\_def\_and\_thm.v}. % (1029 lines).
\item
Section~\ref{ssec:sheafification} is formalized in
\texttt{sheaf\_induction.v}. % (2340 lines).
\end{itemize}

Overall, % with other files containing technical lemmas,
the project
contains 8000 lines, and it could be reduced a bit by improving the
way Coq tries to rewrite and apply lemmas automatically. 
The \texttt{coqwc} tool counts 1600 lines of specifications
(definitions, lemmas, theorems, propositions) and 5500 lines of proof
script.
%
This constitutes a significant amount of work but the part dedicated
to sheaves and sheafification is only 2200 lines of proof script,
which seems quite reasonable and encouraging, because it suggests
that homotopy type theory provides a convenient tool to formalize some
part of the theory of higher topoï. 

\subsection{Limitations of the formalization}
\label{ssec:limit-form}

In the formalization, we had to use the \texttt{type-in-type} option, to handle
the universe issues we faced. However, a lot of the code compiles
without this flag, but need universe polymorphism. 

Universes are used in type theory to ensure consistency by checking
that definitions are well-stratified according to a certain hierarchy.
%
Universe polymorphism~\cite{sozeau2014universe} supports generic
definitions over universes, reusable at different levels.
%
Although the presence of universe polymorphism is mandatory for our
formalization, its implementation is still too rigid to allow a
complete formalization of our work for the following reasons.

%
If Coq handles cumulativity on $\Type$ natively, it is not
the case for the $\Sigma$-type $\Type_n$, which require propositional
resizing. 
%
This issue could be solved by adding an axiom of cumulativity
for $\Type_n$ with an explicit management of universes. 
%
But as it would not have any computational content, such a solution
would really complicate the proofs as the axiom would appear
everywhere cumulativity is needed and it would need explicit
annotations for universe levels everywhere in the formalization.
%
% Note that we also could have resolved the issue by giving explicitely
% the universe levels we wanted, like in the Coq/HoTT library\cite{hottlib}.

One issue with universe polymorphism lies in the management of
recursive definitions. Indeed, the following recursive definition of
sheafification
%
% \vspace{-0.05em}
\[ \begin{array}{l}
   \modal : \forall \ (n : nat), \ \Type_n \to \Type_n 
   \\
    \modal_{-1\phantom{n}}(T) \defeq\lnot\lnot T \\

      \displaystyle{\modal_{n+1}(T)} \defeq  
      \displaystyle{\sum_{u:T \to \Type_n^\modal} \!\!\!\!\modal_{-1} 
      \left\|
      \sum_{a:T} u= (\lambda t,~\modal_n (a=t))
      \right\|}
    \end{array}
% \vspace{-0.3em}
\]
%
is not allowed. 
%
This is because Coq forces the universe of the first $\Type_n$
occurring in the definition to be the same for every $n$, whereas the
universe of the first $\Type_{n+1}$ occurring in $\modal_{n+1}$ should be at
least one level higher as the one of $\Type_n$ occurring in
$\modal_{n}$ because of the use of $\Sigma$-type over
$T \to \Type_n^\modal$ and equality on the return type of $\modal_n$.
%
% \nt{explain why it is an issue.}
%
Thus, the induction step presented in this paper has been formalized,
but the complete recursive sheafification can not be defined for the
moment.
%
Note that the same increasing in the universe levels occurs in the
Rezk completion for categories~\cite{rezk}. In the definition of the
completion, they use the Yoneda embedding and representable functors,
which is similar to our use of characteristic functions.
 
%
This restriction in our formalization may be solved by
generalizing the management of universe polymorphism for recursive definition
%
or by the use of general ``resizing axiom'' which is still under
discussion in the community.


% \section{Forcing in type theory}
% \label{sec:forcing}
% \todo[inline]{Try to write something smart about connections with
%   forcing}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: