introduction.tex

\chapter{Introduction}
\label{chap:intro} \epigraph{In anticipation of the coming of our
overlords computers, we redo math as computers understand it.}{Andrej
Bauer}

Homotopy type theory is a brand new branch of mathematics and computer
science, exhibiting a strong, but surprising link between the theory
of $\omega$-categories and type theory. This topic hence lives at the
borderline between pure mathematics and computer science. One of the
goals of researches on this topic is to use homotopy type theory as a
new foundation for mathematics, replacing for example Zermelo-Frænkel
set theory. Its strong links with type theory would allow
mathematicians to formalize their work with a proof assistant such as
Coq~\cite{coq:refman:8.4}, Agda~\cite{norell2007towards} or
Lean~\cite{lean}. Indeed, errors in mathematical research papers seem
to be inevitable~\cite{vv-univ-f}, and a computer-checked proof might
be more trustable than a human-checked proof.  The most famous
examples of computer-checked results are the {\em Four Colour Theorem}
(to color a map such that any adjacent countries does not have the
same color, four colors are sufficient) by Gonthier and
Werner~\cite{gonthier-four-color} in Coq, the {\em Feit-Thomson
Theorem} (every finite group of odd order is solvable) by Gonthier and
al.~\cite{gonthier-feit} in Coq, the original proof of {\em Jordan curve
theorem} (any continuous simple closed curve divides the plane into an
``interior'' bounded region and an ``exterior'' unbounded region) by
Hales~\cite{hales-jordan} in Mizar, or the {\em Kepler conjecture}
(the most compact ways to arrange spheres are the cubic and hexagonal
close packings) by Hales and al.~\cite{hales-kepler} in Isabelle and
HOL Light.

One advantage of type theory over set theory is the computation
property of type theory: any term is identified with its normal
form. Thus, a proof assistant allows its user to simplify
automatically all expressions, while a proof on paper requires all
computations to be done ``by hand''. Set theory does not share this
computation property, and is thus not convenient to use as a formal
basis for a proof assistant. However, this computation property
prevents us to use classical facts, such as excluded middle ; in the
general case, it is not provable that a proposition is either true or
false.

The main ingredient in homotopy type theory, linking mathematics and
computer science, is the Curry-Howard isomorphism: one can speak
equivalently about proofs or about programs, they describe the same
objects {\em via} a correspondence. For example, in type theory, the
sequence of symbols $A\to B$ can be seen as the type of programs
taking an argument of type $A$ and producing an output of type $B$ as
well as the types of proofs that $A$ implies $B$. Something implied by
this correspondence is that there might exist different proofs of
``$A$ implies $B$'', since there are probably several ways to
construct an output of type $B$ from an input of type $A$. This
property is called {\em proof-relevance}, while ZFC is considered as
{\em proof-irrelevant}: if a lemma has been proved, the way it was
proved can be forgotten, as it does not matter at all.

Other than the lack of classical facts, one issue with type theory is
the notion of equality. Two possibilities arise:
\begin{itemize}
\item an intentional, or definitional, equality ; two objects are
equal if they are defined in the same way, \ie{} if one can be
exchanged with the other without changing the meaning. For example,
the natural number 1 and the successor of the natural number 0 are
intentionally equal. In type theory, we add some rules to this
equality such as $\beta$ ($(\lambda\ x,\,f\ x)y = f\ y$) and $\eta$.
\item an extensional, or propositional, equality ; two objects are
considered equal if they behave in the same way. For example, given
two abstract natural numbers $a$ and $b$, $a+b$ and $b+a$ are
extensionally, but not intentionally equal, \ie{} we need a proof of
this.
\end{itemize} In set theory, we usually use an extensional equality,
asserting that two sets are equal if they have the same elements. In
type theory, the intentional equality is a meta-theoretic notion ;
only the type-checker (like Coq) can access it. It cannot be expressed
in the theory itself, as it is known that extensional type theory is
not decidable~\cite{hofmann1995extensional} (given and term $p$ and a
type $P$, it might be undecidable to check if $p$ is indeed a proof of
$P$). The propositional equality is an internal concept defined as an
inductive family
\[ \mathrm{Id} (A:\Type) (a:A) : A \to \Type
\] generated by only one constructor
\[ \idpath : \mathrm{Id}_A(a,a),
\] and the type $\mathrm{Id}(A,a,b)$ will be denoted $a=_Ab$ or $a=b$.
This identity type is actually not satisfactory. The idea of
Martin-Löf was to mimic mathematical equality, where identity types
fail. Indeed, one issue with this equality is that types $a=b$ can be
inhabited in several ways -- at least, it is not provable that for all
$p,q:a=b$, $p=q$ ; this property, called uniqueness of identity proofs
(UIP) has been proven in~\cite{Hofmann96thegroupoid} independent of
intentional type theory.  Another issue is that this equality is
defined above all types, and does not behave well with some type
constructors ; for example, functional extensionality, asserting that
two functions are equal as soon as they are pointwise equal, cannot be
derived.

Nevertheless, we should not throw away identity types. Around 2006,
Vladimir Voevodsky, and Steve Awodey and Michael
Warren~\cite{awodey-warren} gave independently a new interpretation of
identity types: types are now seen as topological spaces, inhabitants
of types as points, and an element $p:\mathrm{Id}(A,a,b)$ can be read as
\begin{quotation} In the space $A$, $p$ is an homotopy (or a
continuous path) between points $a$ and $b$.
\end{quotation} Under this interpretation, it seems normal not to
satisfy UIP: there can be several (\ie{} non-homotopic) paths between
two points (think of a doughnut). The second issue was solved around
2009, when Vladimir Voevodsky stated the {\em univalence axiom}: two
types are equal exactly when they are isomorphic. It surprisingly
implies compatibility of identity paths with some type constructors:
it implies functional extensionality,
and it seems to imply that identity types of streams coincide with bisimulation~\cite{licata14uafs}.

The original project of Voevodsky~\cite{vv-nsf} was to give a tool so
that mathematicians can check their proofs with the help of
computers. Homotopy type theory seems to be a good setting for this,
but it lacks the {\em law of excluded middle}, one of the
mathematician's favourite thing:
\begin{quotation}
  Any proposition is either true or false.
\end{quotation}
The main goal of this thesis is to add this principle to homotopy type
theory, without losing all desired properties (decidability,
canonicity, constructivity).

Note that we already know how to change an intuitionistic logic into a
classical one, through the Gödel-Gentzen translation defined in
figure~\ref{fig:GG-trans}.
\begin{figure}[ht]
  \centering

  \[x^N \defeq \lnot\lnot x\text{ when $x$ is atomic}\]
  \[(\phi \land \psi)^N \defeq \phi^N \land \psi^N \qquad
  (\phi\lor \psi)^N \defeq \lnot (\lnot\phi^N \land \lnot \psi^N)\]
  \[(\phi \to \psi)^N \defeq \phi^N \to \psi^N \qquad
    (\lnot \psi)^N \defeq \lnot \phi^N\]
  \[(\forall\ x,\ \phi)^N \defeq \forall\ x,\ \psi^N \qquad
  (\exists\ x,\ \phi)^N \defeq \lnot\forall\ x\,\ \lnot\phi^N\]
  \caption{Gödel-Gentzen translation}
  \label{fig:GG-trans}
\end{figure}
A soundness theorem states that a formula $\phi$ is classically
provable if and only if $\phi^N$ is intuitionistically
provable. Although this translation only works with the logic, the
same idea can be applied to the whole type theory, as it is done
in~\cite{jaber2012extending,forcing2016}. The idea behind a
translation is, from a source (complex) theory $\mathcal S$, to translate every
term $t$ of $\mathcal S$ into a term $[t]$ of a target theory
$\mathcal T$, known to be consistent. The desired property of a
translation is its soundness, \ie{} if we can prove a
soundness theorem asserting that if a term $x$ is of type $X$ in
$\mathcal S$, then the translation $[x]$ of $x$ is of type $\Lbrack
X\Rbrack$, where $\Lbrack\cdot\Rbrack$ stands for the translation of
types. Such a statement, together with a proof that $\Lbrack \zero
\Rbrack$ is not inhabited in $\mathcal T$, ensures that the theory
$\mathcal S$ is consistent. 
One could say that a sound translation is a way to give a name in the
target theory $\mathcal T$ to objects of $\mathcal S$ unknown to
$\mathcal T$.

Set theorists will notice that this is very close to the method of
forcing, invented in 1962 by Paul Cohen~\cite{cohen1966}. Its
historical and most famous application is the proof of the
Independence of the negation of the continuum hypothesis with ZFC.
In the same way, forcing can only prove relative consistency, \eg{}
ZFC+$\lnot$CH is consistent if ZFC is consistent. This method is now
one of the most used ingredient of set theorists.

But we know that adapting things of set theory to type theory is not
easy, as those are very different theories. Type theory is known to be
closer to topos theory, and even to higher topos theory for homotopy
type theory. 
Fortunately, Myles Tierney gave a topos-theoretic counterpart of
forcing in 1972~\cite{tierney1972}, through the notion of
sheaves. Originally, sheaves only existed on presheaf topos (the
topos of functor from a category $\mathbf C$ to the category
$\mathbf{Sets}$). These sheaves are called Grothendieck sheaves, and
corresponds to objects $F$ such that any function $X\to F$ can be
defined equivalently on whole $X$ or on each subsets of an open cover
of $X$.
This concept had been extended by William Lawvere and Myles Tierney,
allowing objects of any topos to be sheaves. They correspond to object
$F$ such any function $X \to F$ can be defined equivalently on whole
$X$ or on any dense subobject of $X$.
The existence of a {\em sheafification functor} from any topos
$\mathcal T$ to the topos of sheaves $\Sh{}(\mathcal T)$, left adjoint
to the inclusion functor, allows to build a topos satisfying more
properties than the base topos. 
Sheaves come from a fixed topology, which is an operator on the
``logic'' of the topos (the subobject classifier), idempotent,
preserving $\True$ and commuting with products. Double negation is
actually a topology on any topos $\mathcal T$, and the topos of
sheaves $\Sh{\lnot\lnot}(\mathcal T)$ satisfies good properties: it is
boolean, \ie{} its internal logic satisfies the law of excluded
middle, and the negation of the continuum hypothesis holds in this
topos~\cite{maclanemoerdijk}.

In higher topos theory, this sheafification $(\infty,1)$-functor has
only been defined in~\cite{lurie} for Grothendieck sheaves, leaving
the theory of Lawvere-Tierney sheaves unexplored. There is thus a
double challenge in our quest for excluded middle in homotopy type
theory: the first is to formalize the topos theoretic result, and see
how to extend it to the setting of homotopy type theory, using if
needed $(\infty,1)$-topos' concepts.

\paragraph*{Aims of the thesis} The main goal of this thesis is to
give a definition of a Lawvere-Tierney sheafification functor in the
setting of homotopy type theory. In order to do this, we need first to develop a theory of colimits in homotopy type theory. Then, as our definition of sheafification is done inductively
on the truncation levels, we need to define a truncated version of the
just defined theory of colimits, as well as a truncated version of
left-exact modalities.  All these developments have been
computer-checked by the proof assistant Coq; most of them are
available on my Github account \url{https://github.com/KevinQuirin}.

Our deep study of modalities also leads us to
define the translation of type
theories associated to a (left-exact) modality, and write a Coq plugin
to handle automatically that translation.


\paragraph*{Plan of the thesis}

Let us describe the contents of this thesis. Chapter~\ref{chap:hott}
recalls the basic definitions in homotopy type theory. It is mainly
based on~\cite{hottbook}\footnote{Note that, to ease the reading, some
references are shortcutted by their usual names: \cite{hottbook} is
the Homotopy Type Theory book, \cite{hottlib} is the Coq/HoTT library,
\cite{lurie} is Lurie's monograph Higher topos theory, \etc}, and
serves more as a way for us to introduce notations to be consistent in
the whole thesis. If the reader is not supposed to know anything about
homotopy type theory before reading this thesis, this short
introduction might be not enough to understand this setting, and they are
strongly encouraged to take a look at~\cite{hottbook} before.

Chapter~\ref{chap:modalities} introduces in its first part the theory
of modalities as explained in~\cite{hottbook}. Then, we describe what
we will call a {\em truncated modality}, which is a restricted version
of modalities. Finally, we exhibit the translation of type theories
induced by a left-exact modality.

In Chapter~\ref{chap:colim}, we describe a basic theory of colimits
over graphs, and discuss an extension defining colimits over ``graphs
with compositions''. This chapter, in a large part, has been
formalized by Simon Boulier in a library available at
\url{https://github.com/SimonBoulier/hott-colimits}.

The central (and last) chapter of this thesis is
Chapter~\ref{chap:sheaf}. It describes our construction of the
Lawvere-Tierney sheafification functor, which is a way to extend the
not-not Gödel translation, valid only on h-propositions, to all
truncated types. This result is the main contribution of the thesis.
This chapter uses almost all the theory defined in previous chapters,
and thus can hardly be read on its own. This section as been (almost)
fully formalized, in a library available at
\url{https://github.com/KevinQuirin/sheafification}.


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