resume.tex

\begin{otherlanguage}{french}
  
\chapter{Résumé en français}

\section{Introduction}

La théorie des types homotopique est une branche nouvelle des
mathématiques et de l'informatique, exhibant un lien fort, mais
surprenant entre la théorie des $\omega$-catégories et la théorie de
types. Ce domaine se situe donc à la frontière entre les mathématiques
pures et l'informatique. Un des but de la recherche sur ce sujet est
d'utiliser la théorie des types homotopique comme une nouvelle
fondation des mathématiques, remplaçant par exemple la théorie des
ensembles de Zermelo-Fr\ae nkel. Ses liens forts avec la théorie des
types donneraient aux mathématiciens la possibilité de formaliser
leurs travaux avec un assistant de preuve comme
Coq~\cite{coq:refman:8.4}, Agda~\cite{norell2007towards} ou
Lean~\cite{lean}. En effet, les erreurs dans les articles de recherche
en mathématiques semblent inévitables~\cite{vv-univ-f}, et une preuve
vérifiée par ordinateur peut inspirer plus confiance qu'une preuve
vérifiée par un humain. Les exemples les plus célèbres de preuves
vérifiées par ordinateur sont le {\em théorème des quatre couleurs}
(pour colorier une carte telle qu'aucuns pays voisins aient la même 
couleur, il suffit de quatre couleurs) par Gonthier et
Werner~\cite{gonthier-four-color} avec Coq, le {\em théorème de
Feit-Thomson} (tout groupe fini d'ordre impair est résoluble) par
Gonthier et al.~\cite{gonthier-feit} avec Coq, la preuve originelle du 
{\em théorème de Jordan} (toute courbe simple continue fermée divise le plan
en une partie bornée ``intérieure'' et une partie non bornée
``extérieure'') par Hales~\cite{hales-jordan} avec Mizar, ou la {\em
  conjecture de Kepler} (les façons les plus compactes d'empiler des
sphères sont les empilements clos cubiques et hexagonaux) par Hales et
al.~\cite{hales-kepler} avec Isabelle et HOL Light.

Un des avantages de la théorie des types par rapport à la théorie des
ensembles est la propriété de calculabilité de la théorie des types :
tout terme est identifié avec sa forme normale. Ainsi, un assistant de
preuve permet à l'utilisateur de simplifier automatiquement toutes les
expressions, alors qu'une preuve sur papier requiert de faire toutes
ces calculs à la main. La théorie des ensembles ne partage pas cette
propriété de calculabilité, et n'est donc pas aussi pratique à
utiliser comme base théorique pour un assistant de preuve. Cependant,
cette propriété de calculabilité nous empêche d'utiliser des
propriétés classiques, telles que le tiers exclu ; en général, il est
impossible de prouver qu'une proposition est soit vraie, soit fausse.

L'ingrédient principal de la théorie des types homotopique, faisant le
lien entre les mathématiques et l'informatique, est l'isomorphisme de
Curry-Howard: on peut indifféremment parler de preuve ou de programme,
les deux décrivent les mêmes objets {\em via} une correspondance. Par
exemple, en théorie de types, la séquence de symboles $A\to B$ peut
être vue comme le type des programmes prenant un argument de type $A$
et produisant une sortie de type $B$ ou comme le type des preuves que
$A$ implique $B$. Une chose qu'implique cette correspondance est qu'il
peut exister plusieurs preuves de ``$A$ implique $B$'', puisqu'il peut
y avoir plusieurs manières de produire une sortie de type $B$ à partir
d'une entrée de type $A$. Cette propriété est appelée {\em
  proof-relevance}, alors que ZFC est considérée comme {\em
  proof-irrelevant}: si un lemme a été prouvé, la façon de le prouver
peut être oublié, elle n'a aucune importance.

À part le manque de propriétés classique, un problème de la théorie
des types est la notion d'égalité. On a deux possibilités:
\begin{itemize}
\item une égalité intentionnelle, ou définitionnelle ; deux objets
  sont égaux s'ils sont définis de la même manière, \ie{} si l'un peut
  être échangé avec l'autre sans changer le sens. Par exemple, le
  nombre naturel $1$ et le successeur du nombre naturel 0 sont
  intentionnellement égaux. En théorie des types, on ajoute des règles
  à cette égalité comme la règle $\beta$ ($(\lambda\ x,\ f\ x)y = f\
  y$) and $\eta$.
\item une égalité extensionnelle, ou propositionelle ; deux objets
  sont considérés égaux s'ils se comportent de la même façon. Par
  exemple, étant donnés deux nombres naturels $a$ and $b$, $a+b$ et
  $b+a$ sont extensionnellement mais pas intentionnellement égaux ; on
  a besoin de le prouver.
\end{itemize}
En théorie des ensembles, on utilise traditionnellement une égalité
extensionnelle, en affirmant que deux ensembles sont égaux si et
seulement s'ils ont les mêmes éléments. En théorie des types,
l'égalité intentionnelle est une notion meta-théorique ; seul le
type-checker (comme Coq) peut y accéder. On ne peut pas l'exprimer
dans la théorie elle-même car on sait que la théorie des types
extensionnelle est indécidable~\cite{hofmann1995extensional} (étant
donnés un terme $p$ et un type $P$, il peut être indécidable de
vérifier que $p$ est bien une preuve de $P$). L'égalité
propositionnelle est un concept interne à la théorie, définie comme un
type inductif
inductive type
\[ \mathrm{Id} (A:\Type) (a:A) : A \to \Type
\] généré par un seul constructeur
\[ \idpath : \mathrm{Id}_A(a,a),
\] 
et le type $\mathrm{Id}(A,a,b)$ sera noté $a=_A b$ ou $a=b$. Ce type
identité n'est en fait pas satisfaisant. L'idée de Martin-Löf était de
copier l'égalité mathématique, mais le type identité n'y arrive
pas. En effet, un problème avec cette égalité est que les types $a=b$
peuvent être habités de différents manières -- au moins, il n'est pas
prouvable que pour tous $p,q:a=b$, $p=q$ ; cette propriété, appelée
UIP (unicité des preuves d'égalité) a été prouvée
dans~\cite{Hofmann96thegroupoid} être indépendante de la théorie des
types intentionnelle. Un autre problème est que cette égalité est
définie pour tous les types, et ne se comporte pas bien vis-à-vis de
certains constructeurs de types ; par exemple, l'extensionalité
fonctionnelle, affirmant que deux fonctions sont égales dès qu'elles
sont égales point-à-point, ne peut pas être montrée.

Cependant, il ne faut pas jeter les types identité. Vers 2006,
Vladimir Voevodsky, et Steve Awodey et Michal
Warren~\cite{awodey-warren} ont donné indépendamment une nouvelle
interprétation des types identité : les types sont maintenant vus
comme des espaces topologiques, les habitants des types comme des
points, et un élément $p:\mathrm{Id}(A,a,b)$ peut être lu comme
\begin{quotation}
  Dans l'espace $A$, $p$ est une homotopie (ou un chemin continu)
  entre les points $a$ et $b$.
\end{quotation}
Avec cette interprétation, il paraît normal de ne pas satisfaire UIP :
il peut y avoir plusieurs (\ie{} non homotopiques) chemins entre deux
points (on peut penser à un beignet). Le second problème a été résolu
vers 2009, quand Vladimir Voevodsky a énoncé l'axiome d'univalence:
deux types sont égaux exactement quand ils sont isomorphes. De façon
surprenante, cette axiome implique la compatibilité des types identité
avec certains constructeurs de types: il implique l'extensionalité
fonctionnelle, et il semble qu'il implique aussi que le type identité
sur les {\em streams} coïncide avec la
bisimulation~\cite{licata14uafs}.

Le projet originel de Voevodsky~\cite{vv-nsf} était de donner un outil
aux mathématiciens pour qu'il puissent vérifier leurs preuves sur
ordinateur. La théorie des types homotopique semble être une bonne
base pour ça, mais il manque le {\em tiers-exclu}, un des principes
préférés des mathématiciens :
\begin{quotation}
  Toute proposition est soit vraie, soit fausse.
\end{quotation}
Le but principal de cette thèse est d'ajouter ce principe à la théorie
des types homotopique, sans perdre certaines propriétés (décidabilité,
canonicité, constructivisme).

Commençons par remarquer qu'on sait déjà transformer une logique
intuitionniste en une logique classique, avec la traduction de
Gödel-Gentzen définie dans la figure~\ref{fig:GG-trans-fr}
\begin{figure}[ht]
  \centering

  \[x^N \defeq \lnot\lnot x\text{ quand $x$ est atomique}\]
  \[(\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{Traduction de Gödel-Gentzen}
  \label{fig:GG-trans-fr}
\end{figure}

Un théorème de correction affirme qu'une formule $\phi$ est
classiquement prouvable si et seulement si $\phi^N$ est
intuiitionnistiquement prouvable. Bien que cette traduction ne
fonctionne qu'avec la logique, la même idée peut être utilisée pour
toute la théorie des types, comme dans
\cite{jaber2012extending,forcing2016}.
L'idée derrière une traduction est, en partant d'une théorie source
(compliquée) $\mathcal S$, de traduire tous les termes $t$ de
$\mathcal S$ en des termes $[t]$ d'une théorie source $\mathcal T$,
supposée sue consistante. La propriété fondamentale d'une traduction
est sa correction, ie{} si on peut prouver un théorème de correction
affirmant que si un terme $x$ est de type $X$ dans $\mathcal S$, alors
la traduction $[x]$ de $x$ est de type $\Lbrack X \Rbrack$, où
$\Lbrack\cdot\Rbrack$ est la traduction des types. Cette propriété,
avec une preuve que $\Lbrack\zero\Rbrack$ n'est pas habité dans
$\mathcal T$, assure que la théorie $\mathcal S$ est consistante. On
peut dire qu'une traduction correcte est un moyen de donner un nom
dans la théorie cible $\mathcal T$ aux objets de $\mathcal S$ inconnus
de $\mathcal T$.

Les théoriciens de ensembles peuvent remarquer que c'est très proche
de la méthode de {\em forcing}, inventée en 1962 par Paul
Cohen~\cite{cohen1966}. Son application historique, et la plus connue,
la preuve d'indépendance de la négation de l'hypothèse du continu avec
ZFC. De la même façon que les traductions, le forcing ne peut montrer
que des résultats de consistance relative, \eg{} ZFC+$\lnot$HC est
consistant si ZFC est consistent. Cette méthode est aujourd'hui un
ingrédient clef des théoriciens de ensembles.

Nous savons déjà qu'adapter des résultats de théorie des ensembles à
la théorie des types n'est pas facile, ces deux théories étant très
différents. La théorie des types est plus proche de la théorie des
topoi, et la théorie des types homotopique encore plus proche de la
théorie des topoi supérieurs. Heureusement, Myles Tierney a donné en
1972 un équivalent du forcing en théorie des topoi~\cite{tierney1972},
en utilisant la notion de faisceaux. À l'origine, les faisceaux
n'existaient que sur des topoi de préfaisceaux (les topoi de foncteurs
d'une catégorie $\mathbf C$ vers la catégorie $\mathbf{Sets}$). Ces
faisceaux sont appelés faisceaux de Grothendieck, et correspondent aux
objets $F$ tels que toute fonction $X \to F$ peut être définie de
façon équivalence soit sur $X$ tout entier, soit sur tous les objets
d'un recouvrement ouvert de $X$. Ce concept a été étendu par William
Lawvere et Myles Tierney, autorisant les objets de n'importe quel
topos à être des faisceaux. Ils correspondent alors aux objets $F$
tels que toute fonction $X\to F$ peut être définie de façon
équivalente soit sur $X$ tout entier, soit sur un sous-objet dense de
$X$. L'existence d'un {\em foncteur de faisceautisation} de n'importe
quel topos $\mathcal T$ vers son topos de faisceau $\Sh{}(\mathcal
T)$, adjoint à gauche de l'inclusion, permet de construire une topos
satisfaisant plus de propriétés que le topos de départ. Les faisceaux
proviennent d'une topologie fixée au départ, qui peut être vue comme
un opérateur sur la ``logique'' du topos (le classifiant des
sous-objets), idempotent, préservant $\top$ et commutant avec les
produits. La double négation est en fait une topologie sur n'importe
quel topos $\mathcal T$, et alors le topos $\Sh{\lnot\lnot}(\mathcal
T)$ satisfait de bonnes propriétés il est booléen (\ie{} satisfait le
tiers exclu), et la négation de l'hypothèse du continu est vraie dans
ce topos~\cite{maclanemoerdijk}.

En théorie des topoi supérieurs, ce $(\infty,1)$-foncteur de
faisceautisation n'a été défini dans~\cite{lurie} que dans le cas des
faisceaux de Grothendieck, laissant la théorie de Lawvere-Tierney
inexplorée. Il y a donc un défi double dans notre quête de tiers-exclu
en théorie des types homotopique : le premier est de formaliser le
résultat de la théorie des topoi, et le second est de l'étendre au cas
de la théorie des types homotopique, en utilisant des résultats de la
théorie des $(\infty,1)$-topoi.

\paragraph*{But de la thèse}
Le but principal de cette thèse est de donner une définition du
foncteur de faisceautisation de Lawvere-Tierney dans le contexte de la
théorie des types homotopique. Pour cela, on aura d'abord besoin d'une
théorie des colimites en théorie des types homotopique. Puis, comme
notre définition de la faisceautisation sera faite inductivement sur
le niveau de troncation, on définira une version tronquée de ces
colimites, et une version tronquée des modalités exactes à gauche. 
Presque tous ces résultats sont vérifiés par ordinateur par l'assistant de
preuve Coq ; la plupart d'entre eux sont disponibles sur mon compte
Github \url{https://github.com/KevinQuirin}.

Notre étude approfondie des modalités nous a aussi amené à définir une
traduction de théorie des types associée à une modalité exacte à
gauche, et à écrire une extension pour Coq pour manipuler
automatiquement cette traduction.

\section{Théorie des types homotopique}
Dans cette section, nous allons décrire brièvement le cadre dans
lequel on se place, la théorie des types homotopique. La définition
compacte de cette théorie pourrait être
\[
  \mathrm{HoTT} = \mathrm{MLTT}+\mathrm{UA}+\mathrm{HIT}
\]
où MLTT est la théorie des types de Martin-Löf (ou théorie des types
dépendants), UA est l'axiome
d'univalence et HIT est l'abréviation des types inductifs supérieurs.
Pour une description plus complète de MLTT, le lecteur pourra se référer
à~\cite{hofmann1997syntax} ou \cite{hottbook}.

Dans la théorie des ensembles de Zermelo-Frank\ae l, la formule
logique la plus basique est
\[ x\in E\]
où $x$ et $E$ sont des ensembles. En théorie des types dépendants, un
jugement similaire serait 
\[ a : A\]
qui doit être lu comme ``$a$ est de type $A$''. La différence
principale avec la relation d'appartenance est qu'un élément $a$
n'appartient qu'à un et un seul type, alors qu'il est possible
d'écrire $x\in E$ et $x\in F$ en théorie des ensembles (c'est la
définition de $x\in E\cap F$).

La théorie des types dépendants est basée sur la correspondance de
Curry-Howard, ou principe de ``proposition comme des types''. En
effet, on ne fait pas de différence entre les proposition et les
types ; $a:A$ sera lu indifféremment ``$a$ est de type $A$'' si $A$
est vu comme un type ou ``$a$ est une preuve de $A$'' quand $A$ est vu
comme une proposition. 

On ne rappelle pas dans ce résumé les règles d'introduction et
d'élimination des types, mais on donne le tableau suivant rappelant
les différents types existants:

\renewcommand{\arraystretch}{2}
 
\begin{tabular}{|l|l|l|}
  \hline
  Nom & Notation & \shortstack{Propositions comme \\ des types} \\
  \hline\hline
  Zéro & $\displaystyle{\zero}$ & $\displaystyle{\bot}$ \\
  \hline
  Un & $\displaystyle{\one}$ & $\displaystyle{\top}$ \\
  \hline
  Coproduit, sum & $\displaystyle{A+B}$ & $\displaystyle{A\lor B}$ \\
  \hline
  Fonction & $\displaystyle{A\to B}$ & $\displaystyle{A\To B}$ \\
  \hline
  Fonction dépendante, type Pi & $\displaystyle{\prodD x A {B\, x}}$ & $\displaystyle{\forall x,\,
                                                       B\, x}$ \\
  \hline
  Produit & $\displaystyle{A\times B}$ & $\displaystyle{A\land B}$ \\
  \hline
  Somme dépendante, type Sigma & $\displaystyle{\sumD x A {B\, x}}$ & $\displaystyle{\exists x,\, B\,
                                                    x}$ \\
  \hline
  Égalité, identité, chemin & $\displaystyle{a =_A b}$ & $\displaystyle{a = b}$
  \\
  \hline
\end{tabular}
\renewcommand{\arraystretch}{1}

Revenons simplement sur les types identité. Ils sont très utiles pour
affirmer l'égalité propositionnelle entre des objets. On note qu'ils
ne caractérisent pas l'égalité jugementale, qu'on considère comme
appartenant à la méta-théorie. Les types identités donnent à tout type
une structure d'$\omega$-groupoïde, \ie{} la structure d'une
$\omega$-catégorie où toutes les flèches sont inversibles. En
particulier, ils vérifient la réflexion, la transitivité, la symétrie,
l'associativité, le pentagone de Maclane, \etc{}

Les types identités se comportent bien vis-à-vis des fonctions. Si
$f:A\to B$ est une fonction, alors pour tous $x,y:A$, il existe une
fonction 
\[\ap f: x=y \to f(x) = f(y)\]
compatible avec la structure d'$\omega$-groupoïde. 

Avant de lier les
type identités avec les types d'équivalence, définissons d'abord les
équivalences.
\begin{defifr}
  Soient $A,B:\Type$ et $f:A\to B$. On dit que $f$ est une
  équivalence, noté $\IsEquiv(f)$ s'il existe
  \begin{itemize}
  \item une fonction $g:B\to A$, appelée inverse de $f$
  \item un terme $\displaystyle{\retr_f: \prodD x A {g(f(x)) = x}}$,
    appelé la rétraction de l'équivalence
  \item un terme $\displaystyle{\sect_f: \prodD x A {f(g(x)) = x}}$,
    appelé la section de l'équivalence
  \item un terme $\displaystyle{\adj_f: \prodD x A {\ap f {\retr_f x} =
        \sect_f(f\, x)}}$, appelé l'adjonction de l'équivalence.
  \end{itemize}
  On dit que $A$ et $B$ sont équivalents, noté $A\simeq B$ s'il existe
  $f:A\to B$ qui soit une équivalence. 
\end{defifr} 

On note que si $A=B$, alors il existe une équivalence canonique entre
$A$ et $B$, et on note $\mathrm{idtoequiv}:A = B \to A \simeq B$.
On peut alors énoncer l'axiome d'univalence:
\begin{axfr}
  Pour tous types $A$ et $B$, la fonction
  \[ \mathrm{idtoequiv} : A = B \to A\simeq B \]
  est une équivalence.
\end{axfr}
 
Avec cet axiome, il semble que les types identité sont compatibles
avec tous les constructeurs de types: 
\begin{itemize}
\item l'égalité dans les produits correspond à l'égalité des
  composantes
\item l'égalité dans les sommes dépendantes correspond à l'égalité
  des composantes, la deuxième transportée par la première
\item l'égalité dans les fonctions (dépendantes ou non) correspond à
  l'égalité point à point
\end{itemize}

Pour obtenir la théorie des types homotopiques, il reste à rajouter un
moyen de construire des types dont on contrôle -- en partie -- les
espaces de chemins itérés~: les types inductifs supérieurs (HIT). Les
HIT fonctionnent de la même manière que les types inductifs de Coq,
mais on peut aussi rajouter des constructeurs pour les espaces de
chemins.

\begin{exmfr}
  Le premier exemple est le cercle $\Sone$. Il est généré par les
  constructeurs
  \[ \left| 
      \begin{array}{lll}
        \baseS & : & \Sone \\
        \loopS & : & \baseS = \baseS
      \end{array}
    \right.
  \]
  On peut le représenter par
  \[
    \xymatrix@R=0.1em{ \bullet \ar@(ur,ul)[]_\loopS \\ \baseS}
  \]
\end{exmfr}

Comme pour les types inductifs, on donne aussi des éliminateurs pour
les HIT.

\begin{exmfr}
  Donnons l'éliminateur non-dépendant de $\Sone$. Si $P$ est un type,
  $b:P$ et $p:b=b$, alors il existe une fonction 
  \[\Sone_{\mathrm{rec}} : \Sone \to P\]
  tel que $\Sone_{\mathrm{rec}}(\baseS) \equiv b$ et
  $\ap{\Sone_{\mathrm{rec}}}(\loopS) = p$.

  L'éliminateur dépendant est un peu plus compliqué. Si
  $P:\Sone\to\Type$ est une famille de type sur $\Sone$, $b:(P\baseS)$
  et $p:\transport_P^\loopS(b) = b$, alors il existe un terme
  \[ \Sone_{\mathrm{ind}} : \prodD x \Sone {P\, x}\]
  tel que $\Sone_{\mathrm{ind}}(base) \equiv b$ et
  $\ap{\Sone_{\mathrm{ind}}}(\loopS) = p$.
\end{exmfr}

\section{Colimites}

On voit dans~\cite{lumsdaine} que la présence des sommes dépendantes
en théorie des types permet de construire des limites sur des
graphes. Cependant, alors que ce n'est qu'une notion duale, on ne sait
pas traiter le cas des colimites dans MLTT.  On va voir dans cette
partie que les types inductifs supérieurs permettent de gérer les
colimites au-dessus de graphes, et même au-dessus de catégories dans
certains cas.

Commençons par rappeler les définitions de graphes et diagrammes.


\begin{defifr}[Graphe]
  Un {\em graphe} $G$ est la donnée de
  \begin{itemize}
  \item un type $G_0$ de sommets ;
  \item pour tous $i,j:G_0$, un type $G_1(i,j)$ d'arêtes.
  \end{itemize}
\end{defifr}

\begin{defifr}[Diagramme]
  Un {\em diagramme} $D$ sur un graphe $G$ est la donnée de
  \begin{itemize}
  \item pour tous $i:G_0$, un type $D_0(i)$ ;
  \item pour tous $i,j:G_0$ et tous $\phi : G_1(i,j)$, une flèche $D_1(\phi)
    : D_0(i) \to D_0(j)$
  \end{itemize}
\end{defifr}

Comme dans le contexte catégorique, on va essayer de définir une
colimite comme un type qui forme un cocone sur le graphe désiré, de
façon universelle. Dans la suite, on se fixe un graphe $G$ et un
diagramme $D$ au-dessus de $G$.

\begin{defifr}
  Soit $Q$ un type. Un cocone sur $D$ dans $Q$ est la donnée de
  flèches $q_i : D_i \to Q$, et pour tous $i,j:G$ et $g:G(i,j)$, une
  homotopie $q_j \circ D(g) \homot q_i$.
\end{defifr}

On peut postcomposer les cocones par des flèches. Plus précisément, si
$Q$ et $Q'$ sont des types, $f:Q \to Q'$ et $C$ un cocone sur $D$ dans
$Q$, alors il existe un cocone sur $D$ dans $Q'$ qui consiste à
postcomposer toutes les flèches de $C$ par $f$. Cela donne une flèche
\newcommand{\postcomposecocone}{\mathrm{postcompose}_{\mathrm{cocone}}}
\[\postcomposecocone : \cocone_D(Q) \to (Q':\Type) \to (Q \to Q') \to
  \cocone_D(Q') \]
L'autre sens correspond à notre définition de colimite:

\begin{defifr}[Colimite]
  Un type $Q$ est une colimite de $D$ s'il existe un cocone $C$ sur
  $D$ dans $Q$, qui est universel, \ie{} tel que
  $\postcomposecocone(C,Q')$ soit une équivalence.
\end{defifr}

Les colimites sont compatibles avec différentes opérations sur les
diagrammes, que nous n'expliciterons pas ici. On notera simplement que
deux diagrammes équivalents ont des colimites équivalentes, donnant
par suite l'unicité à équivalence près des colimites.

Regardons un cas particulier de colimites qui nous intéressera plus
tard~: les constructions de Van Doorn et de Boulier.
Elles généralisent le théorème de théorie des topoi affirmant que tout
épimorphisme est la colimite de sa kernel pair. En théorie des topoi
supérieurs, le résultat reste vrai en remplaçant ``kernel pair'' par
``nerf de \v{C}ech''. Cependant, on ne sait pas définir en
théorie des types les nerf de
\v{C}ech, qui sont une version particulière d'objets simpliciaux. On
va donc donner un autre diagramme dépendant d'une fonction dont la
colimite est l'image de la fonction. On commence par la construction
de Van Doorn, qui correspond à une fonction $A\to\one$, et donnant la
$(-1)$-troncation comme colimite d'un diagramme.



\begin{prop}[Construction de Van Doorn]

  Soit $A:\Type$. On définit le type inductif supérieur $TA$ comme la
  colimite (le coégaliseur) de
  \[ \xymatrix{ A\times A \ar@<-.5ex>[r]_-{\pi_2}
      \ar@<.5ex>[r]^-{\pi_1} & A }.\]
  Alors la colimite de
  \[ \xymatrix{
      A \ar[r]^-q& TA \ar[r]^-q& TTA \ar[r]^-q& TTTA \ar[r]^-q& \dots
    }\]
  est $\|A\|_{-1}$.
\end{prop}

Maintenant, soient $A,B:\Type$ et $f:A\to B$. On définit la kernel pair de $f$
comme la colimite de \[ \xymatrix{ A\times_B A \ar@<-.5ex>[r]_-{\pi_2}
      \ar@<.5ex>[r]^-{\pi_1} & A }.\]
en d'autres termes, $\KP(f)$ est le type inductif supérieur généré par
\[\left|
    \begin{array}{lll}
      \kp &:& A\to \KP(f) \\
      \alpha &:& \displaystyle{\prodD {x,y}{A}{f\, x = f\, y \to kp\,x=\kp\,y}}
    \end{array}
  \right.\]
En utilisant l'éliminateur des colimites, on peut construire une
fonction $\widehat
f:\KP(f) \to B$, telle que le digramme suivant commute
\[\xymatrix{
    A \ar[r]^-{\kp} \ar[rd]_-f & \KP(f) \ar[d]^-{\widehat f} \\
    &B
}\]
On peut alors construire
$KP(\widehat f)$ et une fonction $\widehat{\widehat
  f}:\KP(\widehat f) \to B$, \etc{}
On a le résultat suivant
\begin{prop}[Construction de Boulier]
  Pour tout $f:A\to B$, $\im(f)$ est la colimite de la kernel pair
  itérée de $f$
\[\xymatrix{
  A \ar[r] & \KP(f) \ar[r] & \KP\left(\widehat f\right) \ar[r]& \KP\left(\widehat{\widehat f}\right) \ar[r]& \cdots
}\]
En particulier, si $f$ est une surjection, la colimite de ce diagramme
est $B$.
\end{prop}

Un problème de ces deux constructions est qu'ils ne préservent pas le
niveau de troncation (resp. les plongements). Si $A$ est un $\HProp$,
$TA$ peut avoir un niveau de troncation élevé (resp. si $f$ est un
plongement, $\widehat f$ ne l'est pas forcément). Ce problème peut
être résolu en considérant des graphes avec compositions, et en
définissant les deux types suivants
\[
  TA~\left|
    \begin{array}{lll}
      q&:& A\to TA \\
      \alpha&:& \displaystyle{\prodD {x,y} A {q\, x = q\, y}} \\
      \alpha_1&:& \displaystyle{\prodD x A {\alpha(x,x) = 1}}
    \end{array}
  \right.
  \quad \quad
  \KP(f)~\left|
    \begin{array}{lll}
      \kp&:&A\to \KP(f) \\
      \alpha&:& \displaystyle{\prodD {x,y} A {f\, x = f\, y \to q\, x = q\, y}} \\
      \alpha_1&:& \displaystyle{\prodD x A {\alpha(x,x,1) = 1}}
    \end{array}    
  \right.
\]
Les deux résultats énoncés précédemment restent vrais. Cependant, les
niveaux d'homotopie plus élevés ne sont pas préservés.
Comme pour construire le foncteur de faisceautisation, nous travaillerons à
niveau de troncation fixé, il nous faut un moyen de tronquer les
colimites.

On appelera $n$-colimite d'un diagramme $D$ un type $Q$ qui forme un
cocone sur $D$ et qui est universel par rapport à tous les
$n$-types. On a alors le résultat
\begin{lemfr}
  Soit $D$ un diagramme et $Q$ une colimite de $D$. Alors $\|Q\|_n$
  est une $n$-colimite de $\|D\|_n$, le diagramme où on a $n$-tronqué
  tous les types de $D$.
\end{lemfr}

\section{Modalités}

Comme dit dans l'introduction, le but principal de notre travail est
de construire, à partir d'un modèle $\mathfrak M$ de la théorie des
types homotopique, un autre modèle $\mathfrak M'$ qui satisfait 
de nouveaux principes.
On va utiliser un analogue aux modèles internes~\cite{kunen} de la
théorie des ensembles, représentés ici par des modalités exactes à
gauche.

Le papier~\cite{RijkeShulmanSpitters} en préparation est une
excellente référence pour les modalités en théorie des types homotopiques.

\begin{defifr}
  % \label{def:modality}
  Une modalité exacte à gauche est la donnée de
  \begin{enumerate}[(i)]
  \item Un prédicat $P:\Type \to \HProp$
  \item Pour tout type $A$, un type
    $\modal A$ tel que $P(\modal A)$
  \item Pour tout type $A$, une fonction $\eta_A:A \to
    \modal A$
  \end{enumerate}
  tels que
  \begin{enumerate}[(i)]
    \setcounter{enumi}{3}
  \item Pour tous types $A$ et $B$, si $P(B)$ alors
    \[ \left\{
        \begin{array}{rcl}
          (\modal A \to B) & \to & (A \to B) \\
          f & \mapsto & f \circ \eta_A
        \end{array} \right. \] %
    est une équivalence.
  \item pour tous $A:\Type$ et $B:A \to \Type$ tels que $P(A)$
    et $\prod_{x:A} P(B x)$, alors $P\left( \sum_{x:A} B(x)\right)$
  \item pour tous $A:\Type$ et $x,y:A$, si $\modal A$ est
    contractible, alors $\modal (x=y)$ est contractible.
  \end{enumerate}
  Les conditions (i) à (iv) définissent un {\em sous-univers réflexif}, (i) à
  (v) une {\em modalité}.
\end{defifr}

Les modalités exactes à gauche ont de bonnes propriétés, notemment la
stabilité par produit, produit dépendant, et une version dépendante de
l'éliminateur (iv). De plus, elles préservent les niveaux de
troncation, \ie{} si $P$ est un $n$-type, alors $\modal P$ aussi.

Les troncations sont une classe d'exemples de modalités (mais pas
exactes à gauche), de même que la modalité de la double-négation.

De la même façon que pour les colimites, on définit aussi une version
tronquée des modalités, \ie{} avec un réflecteur $\modal : \Type_n \to
\Type_n$. La majorité des propriétés des modalités restent vérifiées.

À toute modalité exacte à gauche et accessible (admettant une une petite
famille de générateur), on peut associer une traduction de théorie des
types, définie de la façon suivante~:

\begin{itemize}
\item Pour les types
\[
\begin{array}{lcl}
  \left[ \Type\right] &\defeq& (\Type^\modal,\pi_{\Type^\modal})
\end{array}
\]
où $\pi_{\Type^\modal}$ est une preuve que $\Type^\modal$ est lui-même modal.
Pour simplifier, on introduit la notation
  \[ 
  \Lbrack A \Rbrack \defeq \pi_1 \left[ A \right]\]

\item Pour les sommes dépendantes
\[
\begin{array}{lcl}
\left[ \sumD x A B \right] &\defeq&  \left( \sumD x{\Lbrack A \Rbrack}
                                  {\Lbrack B\Rbrack} , \pi_\Sigma^{[A],[B]}
                                \right)\\[0.5em]
  \left[  (x,y)\right] &\defeq& ([x],[y]) \\[0.5em]
  \left[  \pi_i t\right] &\defeq& \pi_i [t] \\[0.5em]
\end{array}
\]
où $\pi_{\Sigma}^{A,B}$ est une preuve que $\sumD x A B$ est modale quand
$A$ et $B$ le sont.
\item Pour les produits dépendants
\[
\begin{array}{lcl}
 \left[ \prod_{x:A} B \right] &\defeq& \left( \prod_{x:\Lbrack A \Rbrack}
                                   \Lbrack B\Rbrack , \pi_{\Pi}^{[A],[B]}
                                  \right)\\[0.5em]
\left[  \lambda\, x:A,~M \right] &\defeq&\lambda\,x:\Lbrack A
                                     \Rbrack,~[ M ]
  \\[0.5em]
  \left[ t \, t' \right] &\defeq& [t] [t'] \\[0.5em]
\end{array}
\]
où $\pi_{\Pi}^{A,B}$ est une preuve que $\prodD x A B$ est modal quand $B$ l'est.
\item Pour les chemins
\[
\begin{array}{lcl}
\left[  A=B \right] &\defeq& \left( [A] = [ B] , \pi_=^{[A],[B]}
                             \right)\\[0.5em]
\left[ 1 \right] &\defeq& 1\\[0.5em]
\left[ J \right] &\defeq& J \\[0.5em]
\end{array}
\]
où $\pi_{=}^{A,B}$ est une preuve que $A=B$ est modal quand
$A$ et $B$ le sont, si $A,B:\Type$, ou une preuve que $A=B$ est modal
dès que leur type est modal si $A,B:X$.
\item Pour les types positifs (on traite le cas du coproduit comme exemple)
\[
\begin{array}{lcl}
\left[  A+B \right] &\defeq& \left( \modal(\Lbrack A \Rbrack + \Lbrack B
                        \Rbrack); \pi_\modal(\Lbrack A \Rbrack + \Lbrack B
                        \Rbrack)\right)\\[0.5em]
\left[  \mathrm{in}_\ell t \right] &\defeq& \eta (\mathrm{in}_\ell [t]) \\[0.5em]
\left[  \mathrm{in}_r t \right] &\defeq& \eta (\mathrm{in}_r [t]) \\[0.5em]
\left[ \langle f ,g\rangle\right] &\defeq& \modal_{\mathrm{rec}}^{\Lbrack A\Rbrack +
                                      \Lbrack B\Rbrack} \langle
                                      [f],[g]\rangle\\[0.5em]
\end{array}
\]
\item Pour les troncations ($i\leqslant n$)
\[
\begin{array}{lcl}
  \left[  \|A\|_i \right] &\defeq& (\modal \| \Lbrack A\Rbrack  \|_i;
                                   \pi_\modal(\| \Lbrack A\Rbrack
                                   \|_i)) \\[0.5em]
  \left[ |t|_i \right] &\defeq& \eta |[t]|_i \\[0.5em]
  \left[ |f|_i \right] &\defeq& \modal_{\mathrm{rec}}^{\| \Lbrack
                                  A\Rbrack  \|_i} | [f] |_i
\end{array}
\]
\end{itemize}

Plus simplement, la traduction traverse les produits dépendants, les
sommes dépendantes et les chemins, et modalise par 
$\modal$ les autres types. Les contextes sont traduits
points-à-points.

On a alors un théorème de correction
\begin{prop}
  Soient $\Gamma$ un contexte valide, $A$ un type et $t$ un terme.
  Si $\Gamma \vdash t : A$, alors 
  \[\Lbrack \Gamma \Rbrack \vdash [t] : \Lbrack A \Rbrack. \]
\end{prop}

Une implémentation de cette traduction a été partiellement faite sous
la forme d'une extension pour Coq, gérant automatiquement cette
traduction. La traduction des inductifs et de leurs constructeurs
reste incomplète.

\section{Faisceaux}

En théorie des topoi, la faisceautisation peut être vue comme un moyen
de transformer un topos en un autre. Elle est utilisée, par exemple,
pour construire à partir de n'importe quel topos $\mathcal T$ un topos
booléen (\ie{} qui satisfait la propriété du tiers-exclu),
satisfaisant l'axiome du choix et la négation de l'hypothèse du
continu~\cite[Theorem VI.2.1]{maclanemoerdijk}.
C'est en fait une adaptation d'une méthode un peu plus ancienne de
théorie des ensembles, permettant de changer un modèle de ZFC en un
autre satisfaisant de nouveaux principes, appelée {\em forcing}. Son
application la plus connue est la preuve de consistance de ZFC avec la
négation de l'hypothèse du continu, par Paul Cohen~\cite{cohen1966},
résolvant (ni positivement, ni négativement) le premier problème de
Hilbert. En effet, Gödel a prouvé en 1938 la consistance de ZFC avec
l'hypothèse du continu~\cite{godel1938} en utilisant son modèle
constructible.
L'idée générae de cette méthode est d'ajouter à la théorie ZFC des
informations partielles à propos du témoin de $\lnot$HC. Puis, en
supposant que ZFC est cohérent, on peut prouver que ZFC avec un nombre
fini de ces approximations est toujours cohérente. Finalement, le
théorème de compacité nous permet de prouver que ZFC avec toutes les
approximations, \ie{} avec le témoin désiré, est consistante.

Le forcing a ensuite été adapté au contexte de la théorie des topoi
par Myles Tierney~\cite{tierney1972}, à travers la notion de
faisceau. On note qu'en théorie des topoi, il existe deux types de
faisceaux~: les faisceaux de Grothendieck, qui n'existent que sur les
topoi de préfaisceaux, et les faisceaux de Lawvere-Tierney. On peut
prouver que les faisceaux de Lawvere-Tierney, quand ils sont pris sur
un topos de préfaisceaux, correspondent exactement aux faisceaux de
Grothendieck ; on peut donc voir les premiers comme une généralisation
des seconds.
Étant donné un topos $\mathcal T$, on peut construire un nouveau topos
-- le topos des faisceaux $\Sh{}(\mathcal T)$ -- avec un plongement
géométrique de $\Sh{}(\mathcal T)$ dans $\mathcal T$, appelé
faisceautisation. Selon les faisceaux que l'on traite, le topos
$\Sh{}(\mathcal T)$ satisfait de nouveaux principes. La construction
du plongement géométriqe est faite dans~\cite[Section
V.3]{maclanemoerdijk}.

Le développement de la théorie des topoi supérieurs (et plus
généralement de la théorie des catégories supérieures) amène à se
demander si une notion de faisceautisation existe toujours dans ces
structures. Cette question est répondue positivement
dans~\cite{lurie}, où l'auteur construit un foncteur de
faisceautisation, mais seulement pour les faisceaux de
Grothendieck. Étonnamment, la faisceautisation dans un topos supérieur
est juste une itération du processus de faisceautisation dans un
topos. Il semble que les faisceaux de Lawvere-Tierney n'ont pas été
traités dans ce nouveau contexte.

Des questions similaires ont été considérées autour de l'isomorphisme
de Curry-Howard, pour étendre un langage de programmation proche de la
théorie des types avec de nouveaux principes logiques ou
calculatoires, en gardant la consistance automatiquement.
Par exemple, beaucoup de travaux ont été menés pour donner un contenu
calculatoire à la loi du tiers-exclu pour donner une version
constructive de la logique classique. Ces travaux ont mené à
différents calculs, notemment le $\lambda\mu$-calcul de
Parigot~\cite{parigot1993classical}, mais ces travaux n'ont pas porté
leurs fruits pour définir une nouvelle version de la théorie des types
avec des principes classiques.
D'autres travaux ont essayé d'étendre les transformations CPS à la
théorie des types, mais se sont confrontés au fait que ces
transformations sont incompatibles avec les sommes
dépendantes~\cite{barthe2002cps}, ce qui montre le lien étroit entre
l'axiome du choix et la loi du tiers-exclu en théorie des
types. Cependant, on a montré que l'axiome du choix est réalisable par
des moyens calculatoires dans un contexte classique par des méthodes
proches de la notion de l'''induction
barre''~\cite{berardi1998computational}, la réalisabilté de
Krivine~\cite{krivine2003dependent} et plus récemment avec la
restrication sur l'élimination des sommes dépendantes et évaluation
paresseuse~\cite{herbelin2012constructive}.
Les travaux sur le forcing en théorie des
types~\cite{jaber2012extending,forcing2016} 
donnent aussi un contnue calculatoire à une théorie des types enrichie
par de nouveaux principes logiques ou calculatoires.

Notre idée dans cette partie est de considérer la faisceautisation
dans les topoi seulement comme la première étape de la
faisceautisation en théorie des types. Les axiomes d'une topologie de
Lawvere-Tierney sont très proches de ceux d'une modalité. On utilisera
cette idée en l'appliquant à chaque classifiant des sous-objets
$\Type_n$.
Le classifiant $\Omega$ d'un topos est vu comme l'ensemble des {\em
  valeurs de vérité} du topos, ce qui correspond donc au type $\HProp$
dans notre contexte ; le topos, considéré comme proof irrelevant,
correspond à notre $\HSet$. La faisceautisation est donc un moyen
d'étendre une modalité exacte à gauche sur $\HProp$ à $\HSet$. On va
donc essayer d'itérer cette construction en l'appliquant au
classifiant $\HSet$ pour étendre la modalité à $\Type_1$, \etc{}

La première chose qu'on remarque est que cette construction ne peut
pas atteindre tous les types : on sait qu'il existe des types qui
n'ont pas un niveau de troncation fini~\cite[Example
8.8.6]{hottbook}. Certains types ne sont même pas la limite de leurs
troncations successives, même avec un axiome d'hypercomplétude. Ceci
nous indique que définir un foncteur de faisceautisation pour tous les
types tronqués ne donnera pas (facilement) un foncteur de
faisceautisation sur tout $\Type$.
On note aussi que les principes qu'on veut ajouter le sont directement
depuis le niveau $\HProp$, l'extension à tous les types tronqués étant
automatique. Le choix de la modalité exact à gauche sur $\HProp$ est
donc crucial. Dans la suite, on en fixe une, notée $\modal_{-1}$.
On va alors définir, par induction sur le niveau de troncation, des
modalités exacte à gauche sur tous les $\Type_n$, prouvant le théorème
suivant:

\begin{thmfr}
  La suite définie par induction par
  \[ \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}
  \]
  définit une suite de modalités exactes à gauche, cohérentes les unes
  avec les autres dans le sens où le diagramme suivant commute pour
  tout $P:\Type_n$ ($\hat P$ est $P$ vu comme habitant de $\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{thmfr}

Dans la suite, nous donnons une idée de la preuve. Soit donc
$\modal_n$ une modalité exacte à gauche sur $\Type_n$, compatible avec
$\modal_{-1}$. On commence par définir une notion de clôture par cette
modalité.

\begin{defifr}
  Soit $E$ un type.
  \begin{itemize}
  \item La clôture d'un sous-objet de $E$ avec des fibres
    $n$-tronquées (ou $n$-sous-objet) classifié par $\chi:
    E\to\Type_n$ est le sous-objet de $E$ classifié par $\modal_n
    \circ \chi$.
  \item Un $n$-sous-objet de $E$ classifié par $\chi$ est clos dans
    $E$ s'il est égal à sa clôture, \ie{} si $\modal_n \circ \chi =
    \chi$.
  \item Un $n$-sous-objet de $E$ classifié par $\chi$ est dense dans
    $E$ si sa clôture est $E$, \ie{} si $\modal_n \circ \chi =
    \lambda e,\one$.
  \end{itemize}
\end{defifr}

Les faisceaux seront les objets dans lesquels les flèches peuvent
n'être définies que sur un sous-objet dense. Commençons par définir
les restrictions, puis les faisceaux.

\begin{defifr}
  Soient $E,F:\Type$ et $\chi:E\to\Type_i$. On définit la fonction de
  restriction $\Phi_E^\chi$ par
  \[
  \fonction{\Phi_E^\chi}{E\to F}{\sumD e E {\chi e} \to F}{f}{f\circ \pi_1}.
  \]
\end{defifr}
 
\begin{defifr}
  \begin{itemize}
  \item Un type $F$ de $\Type_{n+1}$ est séparé si pour tout type $E$,
    et tout $n$-sous-objet dense de $E$ classifié par $\chi$,
    $\Phi_E^\chi$ est un plongement.
  \item Un type $F$ de $\Type_{n+1}$ est un faisceau s'il est séparé, et si pour tout type $E$,
    et tout $(-1)$-sous-objet dense de $E$ classifié par $\chi$,
    $\Phi_E^\chi$ est une équivalence.
  \end{itemize}
\end{defifr}

En terme de diagrammes, un faisceau est donc un objet $F$ tel que pour
tous $E:\Type$, $\chi_n:E\to\Type_n$, $\chi_{-1}:E\to\HProp$, $f_n:
\sumD e E {\chi_n e} \to F$ et $f_{-1}:
\sumD e E {\chi_{-1} e} \to F$, les diagrammes suivants commutent
\[ \xymatrix{
  \sumD e E {\chi_n e} \ar[r]^-{f_n} \ar[d]_{\pi_1} & F \\
  E \ar@{-->}[ru]_{!}&
}
\qquad
\xymatrix{
  \sumD e E {\chi_{-1} e} \ar[r]^-{f_{-1}} \ar[d]_{\pi_1} & F \\
  E \ar@{-->}[ru]_{\exists !}&
}
\]

On a alors 
\begin{prop}
  \begin{itemize}
  \item $\Type_n^\modal$ est un $(n+1)$-faisceau.
  \item Si $A:\Type_{n+1}$ et $B:A \to \Type_{n+1}$ tels que pour tout
    $a:A$, $(B~a)$ est un faisceau, alors $\prodD a A {B\, a}$ est un faisceau.
\end{itemize}
\end{prop}

Comme dans le cas des topoi, on définit la faisceautisation en deux
étapes: à partir de n'importe quel $(n+1)$-type, on construit un
$(n+1)$-type séparé, puis à partir de n'importe quel séparé, un
faisceau.

Pour un $T:\Type_{n+1}$, on définit son séparé $\separated T$ comme
l'image de $\modal_n^T \circ \{\cdot\}_T$, comme dans
\[\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
}, \]%
où $\{\cdot\}_T$ est la flèche singleton $\lambda (t:T),~\lambda
(t':T),~t=t'$. 
%
$\separated T$ peut être donné explicitement par
%
\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*}
%
On prouve alors assez facilement que $\separated T$ est toujours
séparé, et qu'il existe une flèche $\mu_T:T\to\separated T$. Il reste à
montrer que $(\separated,\mu)$ définit une modalité. 
Seule la preuve d'universalité par rapport aux objets séparés requiert
plus d'attention, et utilise la constructiond de Boulier.
Puisque $\mu_T$ est une surjection (elle est définit par la
factorisation surjection-plongement), $\separated T$ est la colimite
de sa kernel pair itérée. Donc, pour tout type $Q$ définissant un
cocone sur $\KP(\mu_T)$, il existe une unique flèche $\separated T\to
Q$. Il reste à montrer que tout objet séparé définit un cocone sur
$\KP(\mu_T)$ ; on va en fait montrer que tout type séparé $Q$ définit
un cocone sur $\|\KP(\mu_T)\|_{n+1}$, ce qui est suffisant. On le fait
en définissant un autre diagramme $\mathring T$, équivalent à
$\|\KP(\mu_T)\|_{n+1}$, pour lequel il est facile de définir un cocone
dans $Q$.

\begin{defifr}
  Soit $X:\Type$. Soit $\mathring T_X$ le type inductif supérieur
  défini par
  \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}

  On voit $\mathring T$ comme le coégaliseur de
  \[
    \xymatrix{\displaystyle{\sumD {a,b}{\|X\|_{n+1}} {\modal (a=b)}} \ar@<-.5ex>[r]_-{\pi_2} \ar@<.5ex>[r]^-{\pi_1}
      & \|X\|_{n+1}
    }\]%
  préservant $\eta_{a=a} 1$.

  On considère alors le diagramme $\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{defifr}

Les diagrammes $\mathring T$ et $\|\KP(\mu_T)\|_{n+1}$ sont
équivalents, et on a donc
\begin{lemfr}
  Soit $T:\Type_{n+1}$. Alors $\separated T$ est la $(n+1)$-colimite
  du diagramme $\mathring T$.
\end{lemfr}
Cela suffit pour affirmer que $(\separated,\mu)$ est une modalité.

Passons maintenant à la deuxième étape.
Pour $T:\Type_{n+1}$, on définit $\modal_{n+1}T$ comme la clôture de
$\separated T$ vu comme sous-objet de $T\to\Type_n^\modal$.
$\modal_{n+1}T$ peut être donné explicitement par
\[
\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\|.
\]%

$\modal_{n+1}T$ est bien un faisceau, car objet clos dans un
faisceau, et $\modal_{n+1}$ est bien une modalité car composée de deux
modalités (la séparation, et la clôture).
On peut facilement montrer que $\modal_{n+1}$ est exacte à gauche, et
on a donc bien étendu notre modalité sur $\Type_n$ à une modalité sur $\Type_{n+1}$.

On peut facilement étendre cette modalité à $\Type$ tout entier, en
prenant la modalité $\modal_i$ au niveau désiré, et en composant avec
la troncation $\|\cdot\|_i$. Cependant, on perd évidemment
l'exactitude à gauche.

\section{Conclusion}
Commençons par un résumé de la thèse. La théorie des types homotopique
est un nouveau domaine de recherche, et se compose de la théorie des
types de Martin-Löf où on voit les types identité comme des
homotopies, à laquelle on ajoute l'axiome d'univalence, liant les
équivalences et les égalités, et les types inductifs supérieurs,
permettant de construire des types avec des égalités non-triviales.
Il semble exister un lien fort entre cette théorie et celle des topoi
supérieurs. Plus précisément, il semble qu'on puisse voir la théorie
des types homotopique comme le langage interne des $(\infty,1)$-topoi.

En théorie des types homotopiques, les types sont classifiés par leur
niveau de troncation, représentant la complexité de ses espaces de
boucles itérés. En particulier, si $X$ est $(n+1)$-tronqué, alors tous
les $x=y$ avec $x,y:X$ sont $n$-tronqués. On utilise cette propriété
pour construire un opérateur sur tous les types tronqués par induction
sur le niveau de troncation.

L'opérateur qu'on veut construire est une modalité. Les modalités sont
une version généralisée des localisations, qui sont elles-mêmes un
moyen de caractériser de façon équivalence la notion de sous-topos ;
cette équivalence est toujours vraie en théorie des topos
supérieurs~\cite[Section 6.2.2]{lurie}. En théorie des types
homotopique, une modalité est un opérateur $\modal$ sur $\Type$, muni
d'unités $\eta:\prodD X \Type {X\to\modal X}$ satisfaisant de bonnes
propriétés. Elles peuvent simplement être vue comme des monades
idempotentes. En se basant sur l'équivalence entre la théorie des
types et les $(\infty,1)$-topoi, on peut conjecturer que ces modalités
-- en fait, les modalités accessibles et exacte à gauche -- induisent
des sous-théories de types réflexives. Dans cette thèse, on veut
décrire une théorie des types classique (\ie{} qui satisfait le
principe du tiers-exclu) comme uns sous-théorie de la théorie des
types homotopique, en utilisant une modalité. On sait déjà que c'est
possible en théorie des topoi: en prenant n'importe quel topos
$\mathcal T$, et la topologie de Lawvere-Tierney de la double
négation, on peut construire le topos $\Sh{\lnot\lnot}(\mathcal T)$,
qui est booléen.

L'idée principale de notre travail est de remarquer que les topologies
de Lawvere-Tierney sur un topos, qui sont des opérateurs sur le
classifiant des sous-objets, peuvent être vues en théorie des types
homotopique comme des modalités sur $\HProp$, la deuxième couche de la
stratification des types. De plus, le foncteur de faisceautisation
correspond à étendre cette modalité tronquée à $\HSet$, la couche
suivante. On a donc cru possible d'étendre à nouveau à la couche
suivante, \etc{} pour finalement donner une modalité sur tous les
types tronqués. En fait, {\em modulo} quelque changements dans
plusieurs preuves -- en particulier la preuve impliquant des {\em
  kernel pair} de flèches -- et quelque sophistications dans les
preuves, la méthode décrite dans le cadre des topoi peut être répétée
indéfiniment pour construire une modalité sur tous les niveaux de
notre stratification.

Malheureusement, la gestion actuelle des univers par Coq ne nous
permet pas de formaliser complètement ce résultat ; cependant, une
grosse partie est vérifiée par ordinateur. Certaines parties ne
peuvent être vérifiées qu'en utilisant l'option (inconsistante)
\code{type-in-type} de Coq, autorisant à avoir $\Type^i : \Type^i$,
mais la définition complète ne peut pas être vérifiée complètement. 

\end{otherlanguage}


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