conclusion.tex

\chapter{Conclusion and future works}
\label{chap:conclusion}

Let us begin this conclusion by a summary of this thesis. Homotopy
type theory is a new research domain, and consists of Martin-Löf type
theory where we give a homotopical interpretation of identity types,
together with the univalence axiom, linking equivalence of types with
their equality, and higher inductive types, giving us a way to build
non-trivial equalities. 
It seems that there exists a very strong link between higher topos
theory~\cite{lurie} and this theory. More precisely, homotopy type
theory is expected to be the internal language of
$(\infty,1)$-toposes.

In homotopy type theory, types are classified
by their {\em truncation level}, representing the complexity of its
iterated loop spaces. In particular, if $X$ is $(n+1)$-truncated, then
each $x = y$ with $x,y:X$ is $n$-truncated. We will use this property
to build an operator on all truncated types by induction on the
truncation level.

The operator we want to build is a {\em modality}. Modalities are
generalized version of localizations, which themselves are a way to
characterize equivalently the notion of subtopos; this equivalence
still holds in higher topos theory~\cite[Section 6.2.2]{lurie}. In
homotopy type theory, a modality is an operator $\modal$ on $\Type$,
together with unit maps $\eta : \prodD X \Type {X \to \modal X}$
satisfying properties. They can be seen just as idempotent monads.
Relying on the equivalence between type theory and
$(\infty,1)$-toposes, one can conjecture that modalities -- actually,
accessible left-exact modalities -- induces reflective sub-type
theories. In this thesis, we want to describe a classical type theory
(\ie{} with the law of excluded middle) a sub-type theory of homotopy
type theory, using a modality.
We already know that it is possible in topos theory: take any topos
$\mathcal T$, and the double-negation Lawvere-Tierney topology, and
build the topos of sheaves $\Sh{\lnot\lnot}(\mathcal T)$. Then the
latter is a boolean topos (\ie{} satisfying the LEM).

The main idea of our work is to notice that Lawvere-Tierney topologies
on a topos, which are operator on the subobject classifier, can be
seen, in the setting of homotopy type theory, as modalities restricted
to $\HProp$, the second layer of the stratification of
types. Moreover, the sheafification functor corresponds to extend this
truncated modality to $\HSet$, the next layer. Thus, we believed that
it was possible to extend it again to the next level, \etc{} to
finally give a modality on all truncated types. Actually, {\em modulo}
some changes in several proofs -- in particular the proof involving
kernel pairs of arrows -- and some sophistications in proofs, the
method described in the topos theoretic setting can be repeated
infinitely to build a truncated modality on all level of our
stratification.

Unfortunately, the actual management of universes by Coq does not
allow us to formalize this result completely, but most of the proof is
computer-checked.
Some parts can only be checked using the (inconsistent)
\code{type-in-type} option, allowing $\Type^i : \Type^i$, but the
whole inductive definition cannot be checked at all. However, the key
points of the definition of the functor are formalized.

Nevertheless, our work still need enhancements:
\paragraph*{Extension to Type.}
At the moment, our sheafification functor only handles truncated type,
and we have to compose it with truncations. It would be way more
satisfying to be able to define it on whole $\Type$ left-exactly. The
main issue is that some types, which are not $n$-truncated for any
$n$, are not even the limit of their
truncations~\cite{morelvv}. Therefore, there seems to be no way to
create a link between a non-truncated type and truncated types, to
extend our inductive definition.
It might be possible to have such a link using axioms such as
Whitehead's principle~\cite[Section 8.8]{hottbook} or Postnikov
principle~\cite[Section 5.5.6]{lurie}, and use it to build a real
modality on $\Type$.

\paragraph*{Lawvere-Tierney sheaves in higher topos theory.}
If we rely on the leitmotiv
\begin{quote}
  Homotopy type theory is the internal language of $(\infty,1)$-topos,
\end{quote}
we could transpose our work to higher topos theory. As there are more
tools in topos theory (\eg{} we can access the definitional equality),
it could be a first step in solving the previous future work.
This kind of ``reverse engineered'' proof has already been done for a
proof of the Blakers-Massey theorem by Charles Rezk~\cite{rezk-BM},
inspired by the homotopy-type-theoretic proof by Peter LeFanu
Lumsdaine, Eric Finster and Dan Licata.

\paragraph*{Lawvere-Tierney subsumes Grothendieck?}
In topos theory, there are two different notions of sheaves: the
Grothendieck sheaves and the Lawvere-Tierney sheaves.
The former is a topological, geometrical concept, while the latter is
rather a logical concept.
Grothendieck sheaves are based on {\em Grothendieck
  topologies}~\cite[Chapter III]{maclanemoerdijk}, and one can show
that Lawvere-Tierney topologies on a presheaf topos
$\mathbf{Sets}^{\mathbf{C}^{\mathrm{op}}}$ correspond exactly to
Grothendieck topologies on $\mathbf{C}$. Then, we have the following:
\begin{thm}[{\cite[{Section V.4, theorem 2}]{maclanemoerdijk}}]
  \label{thm:subsume}
  Let $\mathbf{C}$ is a small category and $j$ a Lawvere-Tierney
  topology on $\mathbf{Sets}^{\mathbf{C}^{\mathrm{op}}}$, while $J$ is
  the corresponding Grothendieck topology on $\mathbf{C}$. Then a
  presheaf $P$ is a sheaf for $j$ iff $P$ is a $J$-sheaf.
\end{thm}
The concept of Grothendieck sheaf and Grothendieck sheafification
already exists in $(\infty,1)$-topos~\cite[Section 6.2.2]{lurie}. 
It would be nice to check if theorem~\ref{thm:subsume} still holds,
either in the setting of homotopy type theory or in
the setting of higher topos. The former requires to formalize
Grothendieck topologies, sheaves and sheafification from higher topos
theory to homotopy type theory, while the latter requires to work on
the previous point.





%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: