abstract.tex

\begin{abstract}
  The main goal of this thesis is to define an extension of Gödel
  not-not translation to all truncated types, in the setting of
  homotopy type theory. 
  This goal will use some existing theories, like Lawvere-Tierney
  sheaves theory in toposes, we will adapt in the setting of homotopy
  type theory. In particular, we will define a Lawvere-Tierney
  sheafification functor, which is the main theorem presented in this
  thesis.

  To define it, we will need some concepts, either already defined in
  type theory, either not existing yet. In particular, we will define
  a theory of colimits over graphs as well as their truncated version,
  and the notion of truncated modalities, based on the existing
  definition of modalities.

  Almost all the result presented in this thesis are formalized with
  the proof assistant Coq together with the library~\cite{hottlib}.

\end{abstract}

\begin{otherlanguage}{french}
  
\begin{abstract}
  Le but principal de cette thèse est de définir une extension de la
  traduction de double-négation de Gödel à tous les types tronqués,
  dans le contexte de la théorie des types homotopique.
  Ce but utilisera des théories déjà existantes, comme la théorie des
  faisceaux de Lawvere-Tierney, que nous adapterons à la théorie des
  types homotopiques. En particulier, on définira le fonction de
  faisceautisation de Lawvere-Tierney, qui est le principal théorème
  présenté dans cette thèse.

  Pour le définir, nous aurons besoin de concepts soit déjà définis
  en théorie des types, soit non existants pour l'instant. En
  particulier, on définira une théorie des colimits sur des graphes,
  ainsi que leur version tronquée, et une notion de modalités
  tronquées basée sur la définition existante de modalité.

  Presque tous les résultats présentés dans cette thèse sont
  formalisée avec l'assistant de preuve Coq, muni de la
  librairie~\cite{hottlib}.
\end{abstract}  

\end{otherlanguage}