Kevin Quirin

Lawvere-Tierney

Reader, M Martín Escardó

Professor, M André Hirschowitz

Professor, M Pierre Cointe

M Matthieu Sozeau

Lawvere-Tierney sheafification in Homotopy Type Theory

Keywords: Théorie des types, homotopie, faisceautisation, Coq Type theory, homotopy, sheafification, Coq

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 [HoTT/Coq].

Résumé

Le but principal de cette thèse est de définir une extension de la traduction de doublené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 [HoTT/Coq].

1

Résumé en français

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 ω-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-Fraenkel. 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 [START_REF]The Coq development team[END_REF], Agda [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF] ou Lean [START_REF] Mendonça De Moura | The Lean Theorem Prover (System Description)[END_REF]. En effet, les erreurs dans les articles de recherche en mathématiques semblent inévitables [START_REF] Voevodsky | Univalent Foundations[END_REF], 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 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 [START_REF] Gonthier | Formal proof-the four-color theorem[END_REF] avec Coq, le théorème de Feit-Thomson (tout groupe fini d'ordre impair est résoluble) par Gonthier et al. [START_REF] Gonthier | A machine-checked proof of the odd order theorem[END_REF] avec Coq, la preuve originelle du 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 [START_REF] Thomas | Jordan's proof of the Jordan curve theorem[END_REF] avec Mizar, ou la 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. [START_REF] Hales | A formal proof of the Kepler conjecture[END_REF] 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 via une correspondance. Par exemple, en théorie de types, la séquence de symboles A → 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 proof-relevance, alors que ZFC est considérée comme 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 :

• une égalité intentionnelle, ou définitionnelle ; deux objets sont égaux s'ils sont définis de la même manière, i.e. 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 β ((λ x, f x)y = f y) and η.

• 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.

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 [START_REF] Hofmann | Extensional concepts in intensional type theory[END_REF] (é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 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 [START_REF] Hofmann | The Groupoid Interpretation of Type Theory[END_REF] ê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 [START_REF] Awodey | Homotopy theoretic models of identity types[END_REF] 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 : Id(A, a, b) peut être lu comme blè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 streams coïncide avec la bisimulation [Lic].

Le projet originel de Voevodsky [START_REF] Voevodsky | Univalent Foundations Project[END_REF] é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 tiers-exclu, un des principes préférés des mathématiciens :

Toute proposition est soit vraie, soit fausse.

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 1.1

x N def = ¬¬x quand x est atomique Un théorème de correction affirme qu'une formule φ est classiquement prouvable si et seulement si φ 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 [START_REF] Jaber | Extending type theory with forcing[END_REF][START_REF] Jaber | The Definitional Side of the Forcing[END_REF]. L'idée derrière une traduction est, en partant d'une théorie source (compliquée) S , de traduire tous les termes t de S en des termes [t] d'une théorie source 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 S , alors la traduction [x] de x est de type [X], où [•] est la traduction des types. Cette propriété, avec une preuve que [0] n'est pas habité dans T , assure que la théorie S est consistante. On peut dire qu'une traduction correcte est un moyen de donner un nom dans la théorie cible T aux objets de S inconnus de T .

(φ ∧ ψ) N def = φ N ∧ ψ N (φ ∨ ψ) N def = ¬(¬φ N ∧ ¬ψ N ) (φ → ψ) N def = φ N → ψ N (¬ψ) N def = ¬φ N (∀ x, φ) N def = ∀ x, ψ N (∃ x, φ) N def = ¬∀ x ¬φ N
Les théoriciens de ensembles peuvent remarquer que c'est très proche de la méthode de forcing, inventée en 1962 par Paul Cohen [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF]. 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, e.g. ZFC+¬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 [START_REF] Tierney | Sheaf theory and the continuum hypothesis[END_REF], 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 C vers la catégorie Sets). Ces faisceaux sont appelés faisceaux de Grothendieck, et correspondent aux objets F tels que toute fonction X → 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 → 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 foncteur de faisceautisation de n'importe quel topos T vers son topos de faisceau Sh(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 ⊤ et commutant avec les produits. La double négation est en fait une topologie sur n'importe quel topos T , et alors le topos Sh ¬¬ (T ) satisfait de bonnes propriétés il est booléen (i.e. satisfait le tiers exclu), et la négation de l'hypothèse du continu est vraie dans ce topos [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF].

En théorie des topoi supérieurs, ce (∞, 1)-foncteur de faisceautisation n'a été défini dans [HTT] 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 (∞, 1)-topoi.

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 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.

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 HoTT = MLTT + UA + HIT

THÉORIE DES TYPES HOMOTOPIQUE

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 à [START_REF] Hofmann | Syntax and semantics of dependent types[END_REF] ou [HoTT].

Dans la théorie des ensembles de Zermelo-Frankael, la formule logique la plus basique est

0 ⊥ Un 1 ⊤ Coproduit, sum A + B A ∨ B Fonction A → B A ⇒ B
Fonction dépendante, type Pi

x:A B x ∀x, B x Produit A × B A ∧ B Somme dépendante, type Sigma x:A B x ∃x, B x
Égalité, identité, chemin a = A b a = b 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'ω-groupoïde, i.e. la structure d'une ω-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 → B est une fonction, alors pour tous x, y : A, il existe une fonction x:A g(f (x)) = x, appelé la rétraction de l'équivalence

ap f : x = y → f (x) = f (y)
• un terme sect f :

x:A f (g(x)) = x, appelé la section de l'équivalence

• un terme adj f : Avec cet axiome, il semble que les types identité sont compatibles avec tous les constructeurs de types :

x:A ap f retr f x = sect f (f x), appelé l'adjonction de l'équivalence. On dit que A et B sont équivalents, noté A ≃ B s'il existe f : A → B qui
• l'égalité dans les produits correspond à l'égalité des composantes • l'égalité dans les sommes dépendantes correspond à l'égalité des composantes, la deuxième transportée par la première

• l'égalité dans les fonctions (dépendantes ou non) correspond à l'égalité point à point 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.

Exemple

Colimites

On voit dans [START_REF] Avigad | Homotopy limits in type theory[END_REF] 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.

Définition 1.3 : Graphe

Un graphe G est la donnée de

• un type G 0 de sommets ;

• pour tous i, j : G 0 , un type G 1 (i, j) d'arêtes.

Définition 1.4 : Diagramme

Un diagramme D sur un graphe G est la donnée de

• pour tous i : G 0 , un type D 0 (i) ;

• pour tous i, j :

G 0 et tous φ : G 1 (i, j), une flèche D 1 (φ) : D 0 (i) → D 0 (j)
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.

Définition 1.5 Soit Q un type. Un cocone sur D dans Q est la donnée de flèches q i : D i → Q, et pour tous i, j : G et g : G(i, j), une homotopie q j • D(g) ∼ q i .
On peut postcomposer les cocones par des flèches. Plus précisément, si 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.

Q et Q ′ sont des types, f : Q → 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 postcompose cocone : cocone D (Q) → (Q ′ : Type) → (Q → Q ′ ) → cocone D (Q ′ ) L'
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 Čech". Cependant, on ne sait pas définir en théorie des types les nerf de Č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 → 1, et donnant la (-1)-troncation comme colimite d'un diagramme.

Proposition 1.7 : Construction de Van Doorn

Soit A : Type. On définit le type inductif supérieur T A comme la colimite (le coégaliseur) de

A × A π 2 G G π 1 G G A .

Alors la colimite de

A q G G T A q G G T T A q G G T T T A q G G . . . est A -1 .
Maintenant, soient A, B : Type et f : A → B. On définit la kernel pair de f comme la colimite de

A × B A π 2 G G π 1 G G A .
en d'autres termes, KP(f ) est le type inductif supérieur généré par

kp : A → KP(f ) α : x,y:A f x = f y → kp x = kp y
En utilisant l'éliminateur des colimites, on peut construire une fonction f : KP(f ) → B, telle que le digramme suivant commute

A kp G G f 4 4 KP(f ) f B
On peut alors construire KP( f ) et une fonction f : KP( f ) → B, etc. On a le résultat suivant Proposition 1.8 : Construction de Boulier Pour tout f : A → B, Im(f ) est la colimite de la kernel pair itérée de f

A G G KP(f ) G G KP f G G KP f G G • • •
En particulier, si f est une surjection, la colimite de ce diagramme est B.

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, T A peut avoir un niveau de troncation élevé (resp. si f est un plongement, 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

T A q : A → T A α :
x,y:A q x = q y α 1 :

x:A α(x, x) = 1 KP(f ) kp : A → KP(f ) α :
x,y:A f x = f y → q x = q y α 1 :

x:A α(x, x, 1) = 1
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 Lemme 1.9 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.

Modalités

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

Le papier [RSS] en préparation est une excellente référence pour les modalités en théorie des types homotopiques. Les conditions (i) à (iv) définissent un sous-univers réflexif, (i) à (v) une modalité.

( A → B) → (A → B) f → f • η A
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, i.e. si P est un n-type, alors 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, i.e. avec un réflecteur : Type n → 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 :

• Pour les types [Type] def = (Type , π Type )
où π Type est une preuve que Type est lui-même modal. Pour simplifier, on introduit la notation

[A] def = π 1 [A]
• Pour les sommes dépendantes [ x: A B] def =

x: [A] [B], π

[A],[B] Σ [(x, y)] def = ([x], [y]) [π i t] def = π i [t] où π A,
[ x:A B] def = x:[A] [B], π [A],[B] Π [λ x : A, M] def = λ x : [A], [M] [t t ′ ] def = [t][t ′ ] où π A,B
Π est une preuve que x:A B est modal quand B l'est.

• Pour les chemins

[A = B] def = [A] = [B], π [A],[B] = [1] def = 1 [J ] def = J où π 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.

• Pour les types positifs (on traite le cas du coproduit comme exemple)

[A + B] def = ( ([A] + [B]); π ([A] + [B])) [in ℓ t] def = η(in ℓ [t]) [in r t] def = η(in r [t]) [ f , g ] def = [A]+[B] rec [f ], [g] • Pour les troncations (i n) [ A i ] def = ( [A] i ; π ( [A] i )) [|t| i ] def = η|[t]| i [|f | i ] def = [A] i rec |[f ]| i
Plus simplement, la traduction traverse les produits dépendants, les sommes dépendantes et les chemins, et modalise par les autres types. Les contextes sont traduits points-à-points.

On a alors un théorème de correction Proposition 1.11 Soient Γ un contexte valide, A un type et t un terme. Si Γ ⊢ t : A, alors

[Γ] ⊢ [t] : [A].
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.

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 T un topos booléen (i.e. qui satisfait la propriété du tiers-exclu), satisfaisant l'axiome du choix et la négation de l'hypothèse du continu [MM92, Theorem VI.2.1]. 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 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 [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF], 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 [Göd38] 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 ¬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, i.e. 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 [START_REF] Tierney | Sheaf theory and the continuum hypothesis[END_REF], à 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 T , on peut construire un nouveau topos -le topos des faisceaux Sh(T ) -avec un plongement géométrique de Sh(T ) dans T , appelé faisceautisation. Selon les faisceaux que l'on traite, le topos Sh(T ) satisfait de nouveaux principes. La construction du plongement géométriqe est faite dans [MM92, Section V.3].

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 [HTT], 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 λµ-calcul de Parigot [START_REF] Parigot | Classical proofs as programs[END_REF], 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 [START_REF] Barthe | CPS translating inductive and coinductive types[END_REF], 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" [START_REF] Berardi | On the computational content of the axiom of choice[END_REF], la réalisabilté de Krivine [START_REF] Krivine | Dependent choice,'quote'and the clock[END_REF] et plus récemment avec la restrication sur l'élimination des sommes dépendantes et évaluation paresseuse [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. Les travaux sur le forcing en théorie des types [JTS12 ; Jab+16] 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-

: ∀ (n : nat), Type n → Type n -1 (T ) def = j T n+1 (T ) def = u:T →Type n -1 a:T u = (λt, n (a = t))
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 ( P est P vu comme habitant de Type n+1 )

P ∼ G G η n P η n+1 n P ∼ G G n+1 P
Dans la suite, nous donnons une idée de la preuve. Soit donc n une modalité exacte à gauche sur Type n , compatible avec -1 . On commence par définir une notion de clôture par cette modalité. Définition 1.12 Soit E un type.

• La clôture d'un sous-objet de E avec des fibres n-tronquées (ou n-sous-objet) classifié par χ : E → Type n est le sous-objet de E classifié par n • χ.

• Un n-sous-objet de E classifié par χ est clos dans E s'il est égal à sa clôture, i.e. si n • χ = χ.

• Un n-sous-objet de E classifié par χ est dense dans E si sa clôture est E, i.e. si n •χ = λe, 1.

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.

Définition 1.13 Soient E, F : Type et χ : E → Type i . On définit la fonction de restriction

Φ χ E par Φ χ E : E → F -→ e:E χe → F f -→ f • π 1 .
Définition 1.14 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é n+1 T comme l'image de T n • {•} T , comme dans

T {•} T G G µ T (Type n ) T T n n+1 T G G Type n T , où {•} T est la flèche singleton λ(t : T ), λ(t ′ : T ), t = t ′ . n+1 T peut être donné explicitement par n+1 T def = Im(λ t : T , λ t ′ , n (t = t ′ )) def = u:T →Type n a:A (λt, n (a = t)) = u .
On prouve alors assez facilement que n+1 T est toujours séparé, et qu'il existe une flèche µ T : T → n+1 T . Il reste à montrer que ( n+1 , µ) 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 µ T est une surjection (elle est définit par la factorisation surjection-plongement), n+1 T est la colimite de sa kernel pair itérée. Donc, pour tout type Q définissant un cocone sur KP(µ T ), il existe une unique flèche n+1 T → Q. Il reste à montrer que tout objet séparé définit un cocone sur KP(µ T ) ; on va en fait montrer que tout type séparé Q définit un cocone sur KP(µ T ) n+1 , ce qui est suffisant. On le fait en définissant un autre diagramme T , équivalent à KP(µ T ) n+1 , pour lequel il est facile de définir un cocone dans Q. Définition 1.16 Soit X : Type. Soit TX le type inductif supérieur défini par

• t : X n+1 → TX • α : ∀a b : X n+1 , (a = b) → t(a) = t(b) • α1 : ∀a : X n+1 , α(a, a, η a=a 1) = 1 On voit T comme le coégaliseur de a,b: X n+1 (a = b) π 2 G G π 1 G G X n+1 préservant η a=a 1.
On considère alors le diagramme T : On peut facilement étendre cette modalité à Type tout entier, en prenant la modalité i au niveau désiré, et en composant avec la troncation • i . Cependant, on perd évidemment l'exactitude à gauche.

X n+1 G G TX n+1 G G T TX n+1 G G • • • Les diagrammes T et KP(µ T ) n+1 sont

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 (∞, 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 [HTT, Section 6.2.2]. En théorie des types homotopique, une modalité est un opérateur sur Type, muni d'unités η : X:Type X → 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 (∞, 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 (i.e. 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 T , et la topologie de Lawvere-Tierney de la double négation, on peut construire le topos Sh ¬¬ (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, modulo quelque changements dans plusieurs preuves -en particulier la preuve impliquant des 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) 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.

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 ω-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-Fraenkel set theory. Its strong links with type theory would allow mathematicians to formalize their work with a proof assistant such as Coq [START_REF]The Coq development team[END_REF], Agda [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF] or Lean [START_REF] Mendonça De Moura | The Lean Theorem Prover (System Description)[END_REF]. Indeed, errors in mathematical research papers seem to be inevitable [START_REF] Voevodsky | Univalent Foundations[END_REF], and a computer-checked proof might be more trustable than a human-checked proof. The most famous examples of computer-checked results are the 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 [START_REF] Gonthier | Formal proof-the four-color theorem[END_REF] in Coq, the Feit-Thomson Theorem (every finite group of odd order is solvable) by Gonthier and al. [START_REF] Gonthier | A machine-checked proof of the odd order theorem[END_REF] in Coq, the original proof of Jordan curve theorem (any continuous simple closed curve divides the plane into an "interior" bounded region and an "exterior" unbounded region) by Hales [START_REF] Thomas | Jordan's proof of the Jordan curve theorem[END_REF] in Mizar, or the Kepler conjecture (the most compact ways to arrange spheres are the cubic and hexagonal close packings) by Hales and al. [Hal+15] 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 via a correspondence. For example, in type theory, the sequence of symbols A → 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 proof-relevance, while ZFC is considered as 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:

• an intentional, or definitional, equality ; two objects are equal if they are defined in the same way, i.e. 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 β ((λ x, f x)y = f y) and η.

• 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, i.e. we need a proof of this.

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 [START_REF] Hofmann | Extensional concepts in intensional type theory[END_REF] (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 Id(A : Type)(a : A) : A → Type generated by only one constructor idpath :

Id A (a, a),
and the type Id(A, a, b) will be denoted a = A b 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 [START_REF] Hofmann | The Groupoid Interpretation of Type Theory[END_REF] 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 [START_REF] Awodey | Homotopy theoretic models of identity types[END_REF] gave independently a new interpretation of identity types: types are now seen as topological spaces, inhabitants of types as points, and an element p : Id(A, a, b) can be read as In the space A, p is an homotopy (or a continuous path) between points a and b.

Under this interpretation, it seems normal not to satisfy UIP: there can be several (i.e. nonhomotopic) paths between two points (think of a doughnut). The second issue was solved around 2009, when Vladimir Voevodsky stated the 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 [Lic].

The original project of Voevodsky [START_REF] Voevodsky | Univalent Foundations Project[END_REF] 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 law of excluded middle, one of the mathematician's favourite thing:

Any proposition is either true or false.

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 2.1. A soundness theorem states that a formula

x N def = ¬¬x when x is atomic (φ ∧ ψ) N def = φ N ∧ ψ N (φ ∨ ψ) N def = ¬(¬φ N ∧ ¬ψ N ) (φ → ψ) N def = φ N → ψ N (¬ψ) N def = ¬φ N (∀ x, φ) N def = ∀ x, ψ N (∃ x, φ) N def = ¬∀ x ¬φ N Figure 2.1: Gödel-Gentzen translation
φ is classically provable if and only if φ 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 [JTS12; Jab+16]. The idea behind a translation is, from a source (complex) theory S , to translate every term t of S into a term [t] of a target theory T , known to be consistent.

The desired property of a translation is its soundness, i.e. if we can prove a soundness theorem asserting that if a term x is of type X in S , then the translation [x] of x is of type [X], where [•] stands for the translation of types. Such a statement, together with a proof that [0] is not inhabited in T , ensures that the theory S is consistent. One could say that a sound translation is a way to give a name in the target theory T to objects of S unknown to T . Set theorists will notice that this is very close to the method of forcing, invented in 1962 by Paul Cohen [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF]. 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, e.g. ZFC+¬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 [START_REF] Tierney | Sheaf theory and the continuum hypothesis[END_REF], through the notion of sheaves. Originally, sheaves only existed on presheaf topos (the topos of functor from a category C to the category Sets). These sheaves are called Grothendieck sheaves, and corresponds to objects F such that any function X → 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 → F can be defined equivalently on whole X or on any dense subobject of X. The existence of a sheafification functor from any topos T to the topos of sheaves Sh(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 ⊤ and commuting with products. Double negation is actually a topology on any topos T , and the topos of sheaves Sh ¬¬ (T ) satisfies good properties: it is boolean, i.e. its internal logic satisfies the law of excluded middle, and the negation of the continuum hypothesis holds in this topos [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF].

In higher topos theory, this sheafification (∞, 1)-functor has only been defined in [HTT] 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 (∞, 1)-topos' concepts.

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 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.

Plan of the thesis Let us describe the contents of this thesis. Chapter 3 recalls the basic definitions in homotopy type theory. It is mainly based on [HoTT] 1 , 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 [HoTT] before.

Chapter 4 introduces in its first part the theory of modalities as explained in [HoTT]. Then, we describe what we will call a 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 5, 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 https://github.com/SimonBoulier/hottcolimits.

The central (and last) chapter of this thesis is Chapter 6. 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 https://github.com/KevinQuirin/sheafification.

Homotopy type theory

Mathematics is the art of giving the same name to different objects.

Henri Poincaré

This chapter is an overview of the setting we will use in the rest of the thesis, homotopy type theory. The first part describes the formal system dependent type theory, which is a formal basis for homotopy type theory. This description is not intended to form a complete introduction to type theory accessible by anyone, but rather to clarify the formal system we use. A neophyte willing to read this thesis should read first a complete introduction to type theory, [START_REF] Hofmann | Syntax and semantics of dependent types[END_REF] for an extensive one, but [HoTT] might be more accessible, and sufficient for the thesis. As we will see, we can view homotopy type theory as in HoTT = MLTT + UA + HIT.

UA stands for univalence axiom, and is introduced in the second part of this chapter. HIT is the usual abbreviation for higher inductive types, which is a way, extensively discussed in [HoTT], to build new type, by giving constructors for the type as well as for its identity types. General principles will not be discussed here ; we rather present usual examples of HIT in section 3.3.

Finally, the last section of this chapter presents our point of view on identity paths, leading to the terminology homotopy type theory. This section also introduces the notion of truncation level, which plays a central role in the thesis.

Dependent type theory

In Zermelo-Frankael set theory, the most basic assertion is

x ∈ E where x and E are sets. In dependent type theory, a similar judgement can be a : A, to be read as "a is of type A". The main difference with membership relation is that an element a has one and only one type, while we can say x ∈ E and x ∈ F for the same element x in set theory (it is the definition of x ∈ E ∩ F).

Dependent (or Martin-Lóf, due to its inventor [START_REF] Martin-Löf | An intuitionistic theory of types[END_REF]) type theory is based on the Curry-Howard correspondance [START_REF] Howard | The formulas-as-types notion of construction[END_REF], or "propositions as types" principle. Indeed, we do not need to make a difference between types an propositions. Hence a : A will be read "a is of type A" when A is seen as a type, and "a is a proof of A" when A is seen as a proposition. In the rest of this section 3.1, we present the different types used to build dependent type theory. It is not intended to be complete ; for example we sometimes only give the non-dependent elimination rules to ease the reading. The reader can refer to [START_REF] Nordström | Martin-Löf's type theory, Handbook of logic in computer science: Volume 5: Logic and algebraic methods[END_REF] or [HoTT] for a more detailed introduction.

Universes

In dependent type theory, types are also terms of a universe Type. Of course, we want the universe Type to be itself a type, and the Russel's paradox1 is close here. We solve the problem by using a cumulative hierarchy of universes Type 0 : Type 1 : Type2 : • • • where every universe Type i is of type Type i+1 . Cumulativity means that if A : Type k and k < m, then A : Type m . The handling of universes level can be done automatically 2 by proof assistants such as Coq, and we will thus use only a "type of all type" Type, to be understood in a polymorphic way.

Empty and Unit types

The first two types we will see are the Empty type (denoted 0) and the Unit type (denoted 1). These are respectively the types with zero and one elements (named ⋆). Those two types are dual to each other:

• having a term of type 0 in the context allows to prove anything, while having a term of type 1 in the context is useless

• dually, giving a term of type 1 is trivial, while giving a term of type 0 is impossible (if the theory if consistent).

Here are the (non-trivial) introduction and elimition rules for these types:

Γ ⊢ x : 0 X : Type 0-elim Γ ⊢ 0 rec : X 1-intro Γ ⊢ ⋆ : 1
Under the propositions-as-types principle, 0 is the type always false, and 1 the type always true. With a categorical point of view, 0 is an initial object and 1 is a terminal object.

Coproduct

The coproduct of A and B, noted A + B, is seen as the disjoint sum of A and B. It is described by the inductive type generated by inl :

A → A + B inr : B → A + B
The introduction and elimination rules of coproduct are:

Γ ⊢ a : A +-intro L Γ ⊢ inl a : A + B Γ ⊢ b : B +-intro R Γ ⊢ inr b : A + B Γ ⊢ p : A + B Γ, x : A ⊢ c A : C Γ, x : B ⊢ c B : C +-elim Γ, ⊢ sum_rect(p, c A , c B ) : C
Under the propositions-as-types principle, A + B is seen as the disjunction of A and B.

Dependent product

One of the things both mathematicians and computer scientists love to do is to define functions. If A and B are types, one can consider the type A → B of functions from A to B, taking an inhabitant of type A (called the source type) and giving an inhabitant of type B (the target type). What is new in dependent type theory is that the target type is allowed to depend on the argument of the function.

Example

For example, one can consider a function taking a natural number n and giving a natural number greater than n. The target type depends indeed of n.

Γ ⊢ f : x:A B Γ ⊢ a : A -elim Γ ⊢ f (a) : B[a/x]
Under the propositions-as-types, type of non-dependent functions A → B is seen as implication A ⇒ B, and type of dependent functions x:A B x is seen as universally quantified formulas ∀x, B x. As for functions, dependent type theory allows the second type to depend on the first type. Thus, the type of pairs where the first element x is in type A and the second element y is in type B x is called "dependent sum over B" (or sigma-type over B), noted x:A B x.

Dependent sum

The introduction and elimination rules are:

Γ, x : A ⊢ B : Type Γ ⊢ a : A Γ ⊢ b : B[a/x] -intro Γ ⊢ (a, b) : x:a B Γ ⊢ p : x:A B -intro 1 Γ ⊢ π 1 p : A Γ ⊢ p : x:A B -intro 2 Γ ⊢ π 2 p : B[π 1 p/x]
The projections π 1 and π 2 will sometimes be noted, when applied to a term u, u 1 and u 2 .

Nota

We note that the terminology might be confusing: the dependent generalization of products are dependent sums, while dependent products are generalization of functions.

Under the propositions-as-types principle, A×B is seen as the conjonction A∧B, and x:A B a is seen as the existentially quantified formula ∃x B x.

If In [START_REF] Avigad | Homotopy limits in type theory[END_REF], we see that dependent sums allow to build (homotopy) limits over graphs in homotopy type theory. Chapter 5 will present a way to build (homotopy) colimits over graphs.

Inductive types

Dependent type theory actually allows us to define any inductive type. An inductive type is a type defined only by its introduction rules, in a free way. Its elimination rules are automatically determined. We have already seen examples of inductive types: Empty, Unit and Coproduct.

The most basic example of inductive types might be the type N of naturals. Its introduction rules are N-intro 0 0 : N Γ ⊢ n : N N-intro S Γ ⊢ S n : N We also say that its constructors are 0 : N and S : N → N. N is thus the free type generated by 0 and S. The elimination rule for N is the famous induction principle

Γ, x : N ⊢ P : Type Γ ⊢ n : N Γ ⊢ c 0 : C[0/x] Γ, n : N, y : C ⊢ c S : C[S n/x] N-elim Γ ⊢ nat_ind(C, c 0 , c S (n, y), n) : C[n/x]
This elimination rule allows us to define basic operations on natural numbers: addition, multiplication, order, etc.

For a reader interested by the theory of general inductive types, we refer him to [START_REF] Awodey | Inductive types in homotopy type theory[END_REF].

Paths type

One of the most powerful tool in dependent type theory might be the identity types. They allow us to talk about propositional equality between inhabitants of a type. The identity type over A will be noted a = A b or a = b if A can be inferred from context . What is great about identity type over A is that its definition does not depend on the type A. If a, b : A, a = A b is defined as the inductive type whose only constructor is idpath :

a:A a = A a
(idpath x will sometimes be just noted 1 x , or even 1). Then by path-induction, it suffices to define Q(x, x). The latter is clearly inhabited by idmap P x .

Γ ⊢ a : A =-intro Γ ⊢ idpath a : a = A a Γ ⊢ a, b : A Γ ⊢ q : a = A b Γ, x : A, y : A, p : x = A y ⊢ P : Type Γ, z : A ⊢ w : P[z, z, 1/x, y, p] =-elim Γ ⊢ path_ind q P (w) : P[a, b, q/x,
Path-induction might be the most powerful tool we can use. For example, most of the lemmas we will see in section 3.4 can be proved using path-induction.

Summary

We can summarize the situation in the following array:

Name

Notation Proposition-as-types

Empty 0 ⊥ Unit 1 ⊤ Coproduct, sum A + B A ∨ B Function A → B A ⇒ B
Dependent function, pi-type

x:A B x ∀x, B x Product A × B A ∧ B
Dependent sum, sigma-type

x:A B x ∃x, B x

Identity types and Univalence axiom

Identity types are very useful to assert propositional equalities between object. Note that it does not characterize judgemental equality, which we consider here as belonging to the metatheory (some theories, as Voevodsky's Homotopy Type System [HTS], try to handle internally this equality). One can prove that identity types give each type a structure of a ω-groupoid, i.e. the structure of a ω-category where all arrows are invertible. For example, identity types over a type A satisfies:

• Reflexivity: for all x : A,

1 x : x = x
• Transitivity: for all x, y, z : A, p : x = y and q : y = z, p • q : x = z

• Symmetry: for all x, y : A and p : x = y, p -1 : y = x

• Reflexivity and symmetry behave well together: for all x, y : A and p :

x = y, p • p -1 = 1 x and p -1 • p = 1 y
Note that these paths are respectively in types x = x and y = y.

• Reflexivity and associativity behave well together: for all x, y : A and p : x = y, p • 1 = p and 1 • p = p

IDENTITY TYPES AND UNIVALENCE AXIOM

29

• Associativity: for all w, x, y, z : A and p : w = x, q : x = y, r :

y = z, p • (q • r) = (p • q) • r
• Mac Lane's pentagon: for all v, w, x, y, z : A, p : v = w, q : w = x, r : x = y and s : y = z, the following diagram involving associativities commutes

p • (q • (r • s)) z z 6 6 (p • q) • (r • s) ' ' p • ((q • r) • s) Ó Ó ((p • q) • r) • s G G (p • (q • r)) • s
• The coherences goes on and on.

A thing one can notice here is that we work in a proof-relevant setting. The types x = y are just types, and thus can be inhabited by different objects. It might sound unfamiliar for mathematicians, but we will give in section 3.4 an interpretation of identity types justifying proof-relevance.

Identity types also have a good behavior with respect to function. Let A, B : Type and f : A → B ; then • For all x, y : A, there is a map ap f :

x = y → f (x) = f (y) • It is coherent with inverse: ap f p -1 = (ap f p) -1
• It actually is coherent with the whole ω-groupoid structure. We refer to [HoTT] for more detailed results.

The fact that the definition of identity types does not depend on the type might seem strange, but it actually allows to catch the equality one would want ; for example, we can characterize the equalities between dependent pairs: Lemma 3.2 : Paths in dependent sums Let A : Type and B : A → Type. Then, for any u, v : x:A B a, we have a term path Σ :

p:u 1 = A v 1 transport p P u 2 = v 2 → u = v.
This characterization goes even further, as we can prove that path Σ is an equivalence. Equivalences are very important objects in homotopy type theory, and are defined as Definition 3.3 : Equivalence Let A, B : Type and f : A → B. Wa say that f is an equivalence, noted IsEquiv(f ), if there are:

• a map g : B → A, called the inverse of f • a term retr f :

x:A g(f (x)) = x, called the retraction of the equivalence • a term sect f :

x:A f (g(x)) = x, called the section of the equivalence • a term adj f : Hence, path Σ allows us to prove equalities in a dependent sum x:A B x, but its inverse allows us to prove, from an equality in the dependent sum, equalities in A and in B x.

x:A ap f retr f x = sect f (f x),
Unfortunately, identity types does not allow to characterize equalities for all types. One example is paths in dependent products. In usual mathematics, one would like pointwise equality to be a sufficient (actually, a necessary and sufficient) property to state equality between function. In type theory, that would be phrased

x:A f x = g x → f = g. (3.1)
But one can prove (see [START_REF] Streicher | Investigations Into Intensional Type Theory[END_REF] for a semantical proof) that this property, called functional extensionality cannot be proved from rules of dependent type theory. All we can say is that the backward function of 3.1 can be defined, called happly:

happly : f = g → x:A f x = g x.
Functional extensionality will thus be stated as the axiom:

Axiom 3.4 : Functional extensionality For any A : Type and B : A → Type, the arrow happly is an equivalence.

In a way, that could solve our problem. But dependent products are not the only types for which we cannot characterize identity types; the same problem arises with identity types of the universe. An answer was proposed first by Martin Hofmann and Thomas Streicher in 1996 in [START_REF] Hofmann | The Groupoid Interpretation of Type Theory[END_REF], and later (around 2005) by Vladimir Voevodsky: the univalence axiom. As for functional extensionality, it asserts that a certain arrow is an equivalence. Axiom 3.5 : Univalence axiom For any types A, B : Type, the function

idtoequiv : A = B → A ≃ B is an equivalence.
What is great about univalence axiom is that is seems to imply all other characterization of identity types. For example:

Lemma 3.6 : [BL11][Lic]
Univalence axiom implies functional extensionality.

Another example the reader can think of is the type of streams (and more generaly coindutive) extensionality: we want two streams (infinite list) to be equal when they are pointwise equal. It seems that univalence axiom implies it [Lic].

The main issue with univalence is that it clearly oblige us to work in a proof-relevant setting ; indeed, there are for examples two distinct proofs of 1 + 1 = 1 + 1: the identity, and the function swapping left and right.

Higher Inductives Types

As seen in section 3.1.6, one can define a type by giving only its constructors ; but we also saw in section 3.2 that our setting is proof-relevant. It means that a type is characterized not only by its objects, but also by its identity types between these objects, and identity types of these identity types, etc. Hence, we would like to be able, like for inductive types, to define a type by giving constructors for the objects, and constructors for the identity types, etc. Then, the constructed type is the type freely generated by the constructors, and whose identity types are freely generated by the constructors, etc. Unlike inductive types, it is not known if elimination rules of higher inductive type can easily (and automatically) be infered from the constructors. At the moment, we prefer to express them explicitly. As a general theory of higher inductive types would be very hard, we will only give some fundamental examples.

The circle

The most basic example of higher inductive type is the circle S 1 . The circle consists of just a point, with a non-trivial path above this point. It is defined as the higher inductive type generated by base : S It says that if in P you can find a "copy" of S 1 , then there is a "good" function S 1 → P. The dependent eliminator is a bit more complicated, but still understandable. The most famous result about the circle is the computation of its homotopy group π 1 (S 1 ).

Proposition 3.9 : Fundamental group of

S 1 [LS13]
There is an equivalence (base = base) ≃ Z

where

Z def = N + N + 1.

Coequalizers

Another example of higher inductive type is the computation of coequalizers. In category theory, a coequalizer of two objects a and b with arrow

f , g ∈ Hom(a, b) is a c ∈ Obj together with an arrow q ∈ Hom(b, c) such that a f G G g G G b q G G c commutes,
and which is universal with respect to this property, in the sense that for any other object c ′ ∈ Obj with q ′ ∈ Hom(b, c ′ ), there is an unique arrow d : Hom(c, c ′ ). It might be seen as the diagram

a f G G g G G b q G G q ′ 1 1 c ! d c ′
In homotopy type theory, the coequalizer of two functions f , g : A → B is defined as the higher inductive type Coeq f ,g generated by

q : B → Coeq f ,g α : x:A q • f (x) = q • g(x)
Its elimination principles are:

Lemma 3.10 : Elimination of coequalizer Let A, B, f , g be as above.

• Let P : T ype. If there are terms q ′ : B → P and α ′ :

x:A q ′ • f (x) = q ′ • g(x), then there is a map Coeq f ,g rec : Coeq f ,g → P such that for all b : B, Coeq f ,g rec (q b) ≡ q ′ b and ap Coeq f ,g rec (α b) = α ′ b.
• Let P : Coeq f ,g → Type. If there are terms q ′ : b:B P(q b) and It satisfies the desired universal property in the following sense:

α ′ : b:B transport αb P (q ′ • f (b)) = q ′ • g(b),
• If Q is a type and ϕ : Coeq f ,g → Q, then one can define a map ψ : B → Q such that for all b : B, q • f (b) = q • g(b).
• One can prove that the map φ → ψ is an equivalence: from any other type such that the diagram commutes, there is an unique arrow Coeq f ,g → Q.

Some results about coequalizers in homotopy type theory can be found in the form of Coq code in the HoTT/Coq library [HoTT/Coq].

Suspension

There is a way to see any type A as the identity type of another type: the suspension of A, noted ΣA. It is the higher inductive type generated by

N : ΣA S : ΣA merid : A → (N = S)
Its elimination principle are: Lemma 3.11 : Elimination of suspension Let A be a type.

• Let P : Type. If there are n, s : B and m : A → (n = s), then there is a map The first thing we can notice is that Σ(1 + 1) ≃ S 1 [HoTT, Lemma 6.5.1]. Actually, we can define the sequence of n-spheres inductively by

Σ A rec : ΣA → B such that Σ A rec (N ) ≡ n, Σ A rec (
S 0 def = 1 + 1 S n+1 def = ΣS n

Introduction to homotopy type theory

It is now time to really introduce homotopy type theory: it is the sum of sections 3.1, 3.2 and 3.3. In other words, homotopy type theory is just dependent type theory, augmented with univalence axiom and higher inductive types. We promised in section 3.2 an interpretation of identity types. In homotopy type theory, we view types as topological spaces and inhabitants of types as points of these spaces. Then, if x, y : A, the identity type x = y is viewed as the topological space of paths (or continuous maps f : [0, 1] → A such that f (0) = x and f (1) = y) between points x and y in A. As said, x = y is itself a topological space, thus we can iterate the analogy. A path r : p = q where p, q : x = y are themselves paths is called a homotopy ; a path between paths between paths is called a 2-homotopy, etc. The situation can be depicted as in figure 3.1. Indeed, that interpretation allows to explain all properties of identity types. • The equality 1 x is just the constant path

1 x : [0, 1] -→ A t -→ x • The inverse • -1 is the function changing a path f into g : [0, 1] -→ A t -→ f (1 -t) • The concatenation • • • is the function changing paths f and g into h : [0, 1] -→ A t -→ f (2t) if t ∈ [0, 1 /2] g (2t -1) if t ∈ [ 1 /2, 1]
• A path between paths f and g between points x and y is a continuous function

H : [0, 1] 2 -→ A (u, v) -→ H(u, v)
such that H(t, 0) = f (t), H(t, 1) = g(t), H(0, s) = x and H(1, s) = y. A homotopy is then a continuous deformation of f into g, fixing the ending points x and y.

The table 3.1 summarize the three points of view (type theoretic, groupoidal, homotopy theoretic). In the rest of the thesis, we will use any of the following name (e.g. we will talk about "points of a type", "path betwenn inhabitants", etc.).

What homotopy theorists love to do is to compute fundamental groups (i.e. the group of paths between two points) of different spaces ([WX10] [START_REF] Hutchings | Introduction to higher homotopy groups and obstruction theory[END_REF]). We can then categorized spaces with the level at which their homotopy groups become trivial. Voevodsky has realized that this notion admits a compact inductive definition internal to type theory, given by Definition 3.12 : Truncated types Is-n-type is defined by induction on n -2: • Is-(-2)-type(X) if X is a contractible type, i.e. X is inhabited by c : X, and every other point in X is connected to c.

• Is-(n + 1)-type(X) def = x,y:X Is-n-type(x = y).

Then, Type n def = X:Type Is-n-type(X).

For the first values of n, there are different names: (-2)-truncated types are called contractible types, (-1)-truncated types are called h-propositions, 0-truncated types are called h-sets (the "h" stands for "homotopy"). Following this, Is-(-2)-type is just Contr, Is-(-1)-type is just IsHProp and Type -1 is HProp, and Is-0-type is just IsHSet and Type 0 is HSet. An explanation of this terminology might be helpful. Contractible types are types, inhabited by a center c, with paths between any point and c. A kind of magic thing about contractible types is the lemma Lemma 3.13 If A : Type is contractible, then for any x, y : A, the type x = y is contractible.

Inductively, it means that paths types of any level over a contractible type is contractible. It can be seen as the fact that a contractible type contains only one point c, for which there is only one path c = c, etc. The canonical example of contractible type is 1, and actually, any contractible type is equivalent to 1. Then, h-propositions are types where any two points are connected by a path. The only difference with contractible types is that we allow the type not to be inhabited. h-propositions are then proof-irrelevant types, in the sense that under the propositions-as-types principle, any points x and y in an HProp are equal, with a unique equality, which is thus irrelevant.

Lemma 3.14 : Example of h-propositions

The following types are h-propositions:

• 0, 1

• IsEquiv(f ) for any A, B : Type and f : A → B.

• Is-n-type(A) for any type A : Type and truncation index n. Now, by definition, h-sets are types for which identity types are in HProp. The world of h-sets can thus be seen as the "usual mathematical" world, as it satisfies proof-irrelevance.

The n-truncated types are stable under a lot of operations, as:

Lemma 3.15
Let n -2 be a truncation index. Then • If A : Type n and x, y : A, then Is-n-type(x = y).

• If A : Type n and B : A → Type n , then Is-n-type ( x:A B a).

• If A : Type and B : A → Type n , then Is-n-type ( x:A B a). Note that the source type needs not to be truncated.

• If X : Type n , Y : Type and X ≃ Y , then Is-n-type(Y ).

• If X : Type n , then Is-(n + 1)-type(X).

• We have Is-(n + 1)-type Type n .

Nota Some types are not n-truncated for any n [HoTT, Example 8.8.6] ; it is highly suspected for example that the sphere S 2 is one of these ∞-truncated types (it is at least true in homotopy theory).

This stratification of types induces a stratification of functions. A function f : A → B is said to be n-truncated if all its homotopy fibers fib f (b) are n-truncated. If B : Type, a type A together with a n-truncated map f : A → B will be called a n-subobject of B.

As in [START_REF] Rijke | Sets in homotopy type theory[END_REF], we can define a sequence of subobject classifiers, namely, Type n classifies nsubobjects of a type B, in the sens that there is an equivalence Ξ :

A:Type f :A→B b:B Is-n-type fib f (b) ∼ -→ (B → Type n ) such that the diagram A t f G G f Type • n π 1 B χ f G G Type n
is a pullback for any f with n-truncated homotopy fibers where Type • n def = A:Type A is the universe of pointed n-truncated types and t f = λa, (fib f (f (a)), (a, idpath)).

We will use the equivalence Ξ to define n-subobjects of a type B either as a n-truncated map A → B, either as a characteristic map χ : B → Type n .

Truncations

We present here a way to change any type into a n-truncated type, using truncations. The interested reader can read Nicolai Kraus' PhD thesis [START_REF] Kraus | Truncation Levels in Homotopy Type Theory[END_REF] consecrated to truncation levels in HoTT.

Let n -1 be a truncation index. The n-truncation of a type A is the higher inductive type A n generated by tr n : A → A n α n tr : Is-n-type( A n ) If a : A, tr n (a) will be noted |a| n . The elimination principles are: Lemma 3.16 : Elimination principle of truncations Let A : Type and n -1 be a truncation index.

• If P : Type such that Is-n-type(P) and f : A → P, then there is a map

|f | n : A n → P such that for all a : A, |f | n (|a| n ) ≡ f (a).
• If P : A n → Type such that x: A n Is-n-type(P x) and f : a:A P(|a| n ), then there is a dependent map |f | n :

x: A n

P x

such that for all a :

A, |f | n (|a| n ) ≡ f (a).
Basically, this induction principle says that A n has contains as much data about A than A itself, but it can only be used to define a n-truncated type. It can be expressed as the following universal property: Lemma 3.17 : Universal property of truncations Let A : Type and P : Type n . Then the map precompose tr n :

A → P -→ A n → P f -→ f • tr n is an equivalence.
We will see in chapter 4 that all (Is-n-type, • n ) define modalities. In particular, every truncation index n yields a factorization system: Proposition 3.18 Let n -1 a truncation index. Then any map f : A → B can be factored as a n-connected map followed by a n-truncated map, where a map is n-connected if for all b : B, fib f (b) n is contractible.

In the rest of this thesis, we will only use this result with n = -1. In that case, (-1)-truncated functions are called embeddings, and (-1)-connected functions are called surjections. The factorization of a map f : A → B is given by

A f G G f 4 4 B Im(f ) π 1 Ìm(f ) def = b:B a:A f a = b -1 f def = λa : A, f a, (a, 1 b ) -1

Higher modalities

There is no one fundamental logical notion of necessity, not consequently of possibility. If this conclusion is valid, the subject of modality ought to be vanished from logic, since propositions are simply true or false.

Bertrand Russel

As said in the introduction, the main purpose of our work is to build, from a model M of homotopy type theory, another model M ′ satisfying new principles. Of course, M ′ should be describable inside M. In set theory, it corresponds to building inner models ( [Kun]). In type theory, it can be rephrased in terms of left-exact modalities: it consists of an operator on types such that for any type A, A satisfies a desired property. If the operator has a "good" behaviour, then it is a modality, and, with a few more properties, the universe of all types satisfying the chosen property forms a new model of homotopy type theory.

Modalities are actually a generalization of modal logics [START_REF] Goldblatt | Mathematical modal logic: a view of its evolution[END_REF] and modal type theories [START_REF] Moggi | Notions of Computation and Monads[END_REF]. At the time we write this thesis, the only references for modalities are [START_REF] Shulman | Higher Modalities[END_REF] and [HoTT,Section 7.7]. Most of the results presented here either are taken from the book, either are paper versions of results formalized in [HoTT/Coq, Folder Modalities].

Egbert Rijke, Mike Shulman and Bas Spitters are writing a paper [RSS] extending greatly what is said in the HoTT book, and probably in this thesis.

Modalities Definition 4.1

A left exact modality is the data of (i) A predicate P : Type → HProp (ii) For every type A, a type A such that P( A) (iii) For every type A, a map η A : A → A such that (iv) For every types A and B, if P(B) then

( A → B) → (A → B) f → f • η A
is an equivalence.

(v) for any A : Type and B : A → Type such that P(A) and x:A P(Bx), then P ( x:A B(x))

(vi) for any A : Type and x, y : A, if A is contractible, then (x = y) is contractible.

Conditions (i) to (iv) define a reflective subuniverse, (i) to (v) a modality.

Notation -The inverse of -• η A from point (iv) will be denoted rec :

(A → B) → ( A → B),
and its computation rule

β rec : f :A→B x:A rec (f )(η A x) = f x.
If is a modality, the type of modal types will be denoted Type . Let us fix a left-exact modality for the rest of this section. A modality acts functorialy on Type, in the sense that Lemma 4.2 : Functoriality of modalities Let A, B : Type and f : A → B. Then there is a map f : •(R) A is modal if and only if η A is an equivalence.

A → B such that • f • η A = η B • f • if g : B → C, (g • f ) = g • f • if IsEquiv f , then IsEquiv f .
•(R) 1 is modal.

•(R) Type is closed under dependent products, i.e. x:A B x is modal as soon as all B x are modal.

•(R) For any types A and B, the map

(A × B) → A × B
is an equivalence.

•(R) If A is modal, then for all x, y : A, (x = y) is modal.

1 Properties needing only a reflective subuniverse are annoted by (R), a modality by (M), a left-exact modality by (L)

•(M) For every type A and B : (A) → Type , then

-• η A : z: A B x -→ a:A B(η A a) f -→ f • η A is an equivalence. • (
fib f (b) → fib f (η B b)
is an equivalence, and the following diagram commutes

fib f (b) η G G γ fib f (b) x x fib f (η B b)
Notation -Again, the inverse of -• η A will be denoted ind : a:A B(η A a) → z: A B x, and its computation rule

β ind : f : a:A B(η A a) x:A ind (f )(η A x) = f x
Proof. We only prove the last point. It is straighforward to define a map φ :

x:X f x = y → x: X f x = η Y y, using η functions. We will use the following lemma to prove that the function induced by φ defines an equivalence: Hence we just need to check that every -fiber (fib φ (x; p)) is contractible. Technical transformations allow one to prove fib φ (x; p) ≃ fib s (y; p -1 ) for s :

fib η X (x) -→ fib η Y ( f x) (a, q) -→ (f a, -)
But left-exctness allows to characterize the contractibility of fibers: Thus, we just need to prove that (fib η X (a)) and (fib η Y (b)) are contractible. But one can check that η maps always satisfy this property. Finally, (fib s (y; p -1 )) is contractible, so (fib φ (x; p)) also, and the result is proved.

Let us finish these properties by the following proposition, giving an equivalent characterization of left-exactness.

Proposition 4.6 Let be a modality. Then is left-exact if and only if preserves path spaces, i.e.

A:Type x,y:A

IsEquiv( (ap η A ))

where (ap η A ) : (x = y) → η A x = η A y.

Proof. We will rather prove something slighlty more general, using an encode-decode proof [HoTT, Section 8.9] ; we will characterize, for a type A and a fixed inhabitant x : A the type Then one can show, using -induction and path-induction, that for any y : A, Encode(y, -) and Decode(y, -) are each other inverses. Then, taking y ′ = η A y, we have just shown that

η A x = η A y ≃ Cover(η A y), which is itself equivalent, by β rec , to (x = y). It is straightforward to check that the composition (x = y) → Cover(η A y) → η A x = η A y is exactly (ap η A ).
Now, let us prove the backward implication. Let A be a type such that A is contractible, and x, y : A. As η A x, η A y : A, we know that η A x = η A y is contractible. But as η A x = η A y ≃ (x = y) by assumption, (x = y) is also contractible.

As this whole thesis deals with truncation levels, it should be interesting to see how they are changed under a modality. We already know that if a type T is (-2)-truncated, i.e. contractible, then it is unchanged by the reflector:

T ≃ 1 ≃ 1 ≃ T .
Thus, Type -2 is closed by any reflective subuniverse. Now, let T : HProp. To check that T is an h-proposition, it suffices to check that x,y: T x = y For any x : T , the type y: T x = y is modal, as all x = y are ; by the same argument, x: T x = y is modal too for any y : T . Using twice the dependent eliminator of , it now suffices to check that

x,y:T η T x = η T y.

As T is supposed to be an h-proposition, this is true. It suffices to state Lemma 4.7 For any modality, Type -1 is closed under the reflector , i.e.

P:HProp

IsHProp( P).

A simple induction on the truncation level, together with the left-exactness property allows to state Lemma 4.8 For any left-exact modality, all Type p are closed under the reflector , i.e.

P:Type p

Is-p-type( P).

We note that this is not a equivalent characterization of left-exactness, as it is satisfied by truncations, and we will see they are not left-exact.

Examples of modalities 4.2.1 The identity modality

Let us begin with the most simple modality one can imagine: the one doing nothing. We can define it by letting A def = A for any type A, and η A def = idmap. Obviously, the desired computation rules are satisfied, so that the identity modality is indeed a left-exact modality.

It might sound useless to consider such a modality, but it can be precious when looking for properties of modalities: if it does not hold for the identity modality, it cannot hold for an abstract one.

Truncations

The first class of non-trivial examples might be the truncations modalities, seen in 3.4.1.

Double negation modality

Proposition 4.9

The double negation modality A def = ¬¬A is a modality.

Proof. We define the modality with (i) We will define the predicate P later.

It remains to check that for any x : ¬¬ x:A B x, B(κ x).

But the previous map can be easily extended to the dependent case, and thus it suffices to show that for all x : x:A B x, B(κ(η x). As κ • η = idmap, the goal is solved by π 2 x.

Unfortunately, it appears that the only type which can be modal are h-propositions, as they are equivalent to their double negation which is always an h-proposition. Thus, the type of modal types is consisted only of h-proposition, which is not satisfactory. The main purpose of this thesis, in particular chapter 6 is to extend this modality into a better one.

Truncated modalities

As for colimits, we define a truncated version of modalities, in order to use it in chapter 6. Basically, a truncated modality is the same as a modality, but restricted to Type n . Definition 4.10 : Truncated modality Let n ≥ -1 be a truncation index. A left exact modality at level n is the data of (i) A predicate P : Type n → HProp (ii) For every n-truncated type A, a n-truncated type A such that P ( A) (iii) For every n-truncated type A, a map η A : A → A such that (iv) For every n-truncated types A and B, if P(B) then

( A → B) → (A → B) f → f • η A
is an equivalence.

(v) for any A : Type n and B : A → Type n such that P(A) and x:A P(Bx), then P ( x:A B(x))

(vi) for any A : Type n and x, y : A, if A is contractible, then (x = y) is contractible.

Properties of truncated left-exact modalities described in 4.3 are still true when restricted to n-truncated types, except the one that does not make sense: Type n cannot be modal, as it is not even a n-truncated type.

Formalization

Let us discuss here about the formalization of the theory of modalities. General modalities are formalized in the Coq/HoTT library [HoTT/Coq], thanks to a huge work of Mike Shulman [START_REF] Shulman | Module for Modalities[END_REF]. The formalization might seem to be straightforward, but the universe levels (at least, their automatic handling by Coq) are here a great issue. Hence, we have to explicitely give the universe levels and their constraints in a large part of the library. For example, the reflector of a modality is defined, in [HoTT/Coq] as

: Type i → Type i ;
it maps any universe to itself.

In chapter 6, we will need a slighlty more general definition of modality. The actual definitions stay the same, but the universes constraints we consider change. The reflector will now have type : Type i → Type j , i j;

it maps any universe to a possibly higher one. Other components of the definition of a modality are changed in the same way. Fortunately, this change seems small enough for all properties of modalities to be kept. Of course, the examples of modalities mapping any universe to itself are still an example of generalized modality, it just does not use the possibility to inhabit a higher universe. This has been computer-checked, it can be found at https://github.com/KevinQuirin/HoTT/tree/ extended_modalities.

We would like to have the same generalization for truncated modalities. But there are a lot of new universe levels popping out, mostly because in Type n = T :Type Is-n-type T , Is-n-type come with its own universes. Hence, handling "by hand" so many universes together with their constraints quickly go out of control. One idea to fix this issue could be to use resizing rules [START_REF] Voevodsky | Resising Rules -their use and semantic justification[END_REF], allowing h-propositions to live in the smallest universe. We could then get rid of the universes generated by Is-n-type, and treat the truncated modality exactly as generalized modalities.

Translation

In this section, we will explain how left-exact modalities allows to perform model transformation, just as forcing does. Actually, we can to even better by exhibiting a translation of type theories, from CIC into itself, as it has been done for forcing [START_REF] Jaber | Extending type theory with forcing[END_REF][START_REF] Jaber | The Definitional Side of the Forcing[END_REF]. Let us explain here how this translation works.

Let be an accessible left-exact modality. We describe, for each term constructor, how to build its translation. We denote π (A) the proof that (A) is always modal.

• For types

[Type] def = (Type , π Type )
where π Type is a proof that Type is itself modal. To ease the reading in what follows, we introduce the notation

[A] def = π 1 [A]
• For dependent sums [ x: A B] def =

x: [A] [B], π

[A],[B] Σ [(x, y)] def = ([x], [y]) [π i t] def = π i [t]
where π A,B Σ is a proof that x:A B is modal when A and B are. • For dependent products [ x: A B] def =

x: [A] [B], π

[A],[B] Π [λ x : A, M] def = λ x : [A], [M] [t t ′ ] def = [t][t ′ ] where π A,B Π is a proof that x:A B is modal when B is. • For paths [x = A y] def = [x] = [A] [y], π [x],[y] = [1] def = 1 [J ] def = J
where π

x,y = is a proof that x = A y is modal when A is.

• For positive types (we only treat the case of the sum as an example)

[A + B] def = ( ([A] + [B]); π ([A] + [B])) [in ℓ t] def = η(in ℓ [t]) [in r t] def = η(in r [t]) [ f , g ] def = [A]+[B] rec [f ], [g]
• For truncations (i n)

[ A i ] def = ( [A] i ; π ( [A] i )) [|t| i ] def = η|[t]| i [|f | i ] def = [A] i rec |[f ]| i
Let us make it more explicit on inductive types. In Coq, inductive types are all of the fol-lowing form (we leave the mutual inductive types, behaving in the same way):

I (a 1 : A 1 ) • • • (a n : A n ) : Type def = |c 1 : x 1 :X 1 1 • • • x n 1 :X n 1 1 I(a 1 1 , . . . , a n 1 )
. . .

|c p : x 1 :X 1 p • • • x n 1 :X n 1 p I(a 1 p , . . . , a n p )
with technical conditions on the X j i to avoid ill-defined types. For every such inductive type, we build a new one I defined by

I (a 1 : [A 1 ]) • • • (a n : [A n ]) : Type def = | c 1 : x 1 :⌈X 1 1 ⌉ • • • x n 1 :⌈X n 1 1 ⌉ I([a 1 1 ], . . . , [a n 1 ]) . . . | c p : x 1 :⌈X 1 p ⌉ • • • x n 1 :⌈X n 1 p ⌉ I([a 1 p ], . . . , [a n p ])
where ⌈•⌉ is defined by

X = I([b 1 ], . . . , [b n ]) if X is I(b 1 , . . . , b n ) [X] else
Then, the translation of I(a 1 , . . . , a n ) is defined as ( I([a 1 ], . . . , [a n ])). Example Consider the following inductive q (A : Type) :

Type def = |α : q2 |β : A → q1 → qA
Then the inductive q is q (A : Type ) :

Type def = | α : q( 2) | β : π 1 A → q( 1) → qA
and the translation of qA is thus ( q[A]).

Then, we translate contexts pointwise:

[∅] def = ∅ [Γ, x : A] def = [Γ], x : [A]
As in the forcing translation [START_REF] Jaber | Extending type theory with forcing[END_REF], the main issue is that convertibility might not be preserved. For example, let f : A → X and g :

B → X. Then f , g (in ℓ t) is convertible to f t, but [ f , g (in ℓ t)] reduces to [A]+[B] rec [f ], [g] (η(in ℓ t)), which is only equal to [f t].
Two solutions to this problem can come to our mind:

• We could use the eliminator J of equality in the conversion rule, but this would require to use a type theory with explicit conversion in the syntax, like in [START_REF] Jaber | Extending type theory with forcing[END_REF]. Such type theories has been studied in [START_REF] Geuvers | A logical framework with explicit conversions[END_REF]DGW13]. We do not chose this solution, and thus do not give more details.

• We can ask the modality to be a strict modality, in the sense that retraction in the equivalence of (-• η) is conversion instead of equality, like for the closed modality. That way, we keep the conversion rule

, i.e. if Γ ⊢ u ≡ v, then [Γ] ⊢ [u] ≡ [v].
That is the solution we chose.

We first want to show that the translation respects substitution: The usual result we want about any translation is its soundness: Proposition 4.12 : Soundness of the translation Let Γ is a valid context, A a type and t a term. If Γ ⊢ t : A, then

[Γ] ⊢ [t] : [A].
Proof. We prove it by induction on the proof of Γ ⊢ t : A. We use the name of rules as in [HoTT, Appendix A]. We note M the predicate "is modal".

• Π-form:

This allows to state the following theorem Theorem 4.13 Let be a modality on Type such that

• is left-exact • Type is itself modal • For all A, B, f , x, β rec (A, B, f , x) is a strict equality.
Then induces a new type theory.

Nota

Note that, for any (accessible) modality , we can define an equivalent strict modality, by defining an inductive family S generated by

η S : A:Type A → S A
with an axiom asserting that all S A are -modal, and an induction principle restricted to -modals types As in [START_REF] Shulman | Localization as an Inductive Definition[END_REF], we can change the axiom by the equivalent

A:Type IsEquiv(η A : A → A),
and unfold the definition of IsEquiv to see that S is a valid HIT. We are actually building S as the localization [HTT, Definition 5.2.7.2] of -modal types. This idea is developed in [START_REF] Shulman | All Modalities are HITs[END_REF].

Then, it is straightforward to see that S is a strict modality, equivalent to .

According to the previous remark, the classical situation fulfilling the requirements is when the modality is left-exact and accessible. One example is the closed modality [HoTT/Coq, Modalities/Closed.v].

Note that univalence axiom remains true in the new theory:

Proposition 4.14 Let be as in theorem 4.13. Then the univalence axiom remains true in the new type theory.

Proof.

Lemma 4.15

We begin by showing that for any arrow f :

A → B, [IsEquiv(f )] = IsEquiv[f ].
Proof. Let A, B : Type and f :

A → B. Then IsEquiv(f ) def = g:B→A r: y:B f (g(y))=y s: x:A g(f (x))=x x:A ap f r(x) = s(f x).
As the translation go through dependent product and sums, and through path elimination, it is straightforward that

[IsEquiv(f )] = IsEquiv[f ]. Now, [idtoequiv A,B ] = [λ (p : A = B), transport p A≃• (id)] = λ (p : [A] = [B]), transport p [A]≃• (id) = idtoequiv [A],[B]
As univalence is true in the original type theory, we have A : Type, B : Type ⊢ IsEquiv(idtoequiv A,B ). By the soundness theorem, we have A : Type , B : Type ⊢ IsEquiv(idtoequiv A 1 ,B 1 ).

Nota

We note that if the modality is not left-exact (or not accessible), like truncations modalities, then Type is not itself modal. It is although still possible to write a translation, but we can only define it on a type theory with only one universe. Indeed, the judgement Γ ⊢ Type i : Type j cannot be expressed, and thus cannot be translated to

[Γ] ⊢ [Type i ] : [Type j ].
An implementation of this translation has been made, in the form of a Coq plugin, available at https://github.com/KevinQuirin/translation-mod/. We give here a brief description. For each module, there is a table T containing a list of pairs consisting of constants c (resp. inductive type i) together with its translation [c] (resp. another inductive type [i]). Each time we need the translation of a constant, the plugin read this table to find it. Then, we add two new commands in Coq: Modal Definition and Modal Translate.

I m (x 1 : [A 1 ]) • • • (x n : [A n ]) : Type with constructors C m i : [T i ],
and add (I, I m ) in the table T . Then, the translation of

I (t 1 , • • • , t n ) will be (I m ([t 1 ], • • • , [t n ])).
A comathematician is a device turning cotheorems into ffee.

Co-Alfréd Rényi

As seen in chapter 3, adding sigma-types to type theory results in adding limits over graphs in the underlying category, and adding higher inductives types results in adding colimits over graphs. If limits has been extensively studied in [START_REF] Avigad | Homotopy limits in type theory[END_REF], theory of colimits was not completely treated.

The following is conjoint work with Simon Boulier and Nicolas Tabareau, helped by precious discussions with Egbert Rijke. The sections 5.1 and 5.2 are extended version of the blog post [START_REF] Boulier | Colimits in HoTT[END_REF].

Colimits over graphs

As colimits are just dual to limits, it seems that it would be very easy to translate the work on limits to colimits. Although, even if it might be because we are more habituated to manipulate sigma-types than higher inductive types, it seems way harder.

Definitions

Let's recall the definitions of graphs and diagrams over graphs, introduced in [AKL15].

Definition 5.1 : Graph

A graph G is the data of • a type G 0 of vertices ; • for any i, j : G 0 , a type G 1 (i, j) of edges. Definition 5.2 : Diagram A diagram D over a graph G is the data of • for any i : G 0 , a type D 0 (i) ;
• for any i, j : G 0 and all φ : G 1 (i, j), a map D 1 (φ) : D 0 (i) → D 0 (j) 57 When the context is clear, G 0 will be simply denoted G, G 1 (i, j) will be noted G(i, j), D 0 (i) will be noted D(i) or D i , and D 1 (φ) will be noted D i,j (φ) or simply D(φ) (i and j can be inferred from φ).

Examples :

-One can consider the following graph, namely the graph of (co)equalizers

• G G G G • Here, G 0 = 2, G 1 (⊤, ⊥) = 2 and other G 1 (i, j) are empty.
A diagram over this graph consists of two types A and B, and two maps f , g :

A → B, producing the diagram A g G G f G G B
-The graph of the mapping telescope is

• G G • G G • • • In other words, G 0 = N and G 1 (i, i + 1) = 1.
A diagram over the mapping telescope is a sequence of types P : N → Type together with arrows f n : P n → P n+1 :

P 0 f 0 G G P 1 f 1 G G • • •
What we would like now would be to define the colimits of these diagrams over graphs, that would satisfy type theoretic versions of usual properties: it should make the diagram commute, and be universal with respect to this property. From now on, let G be a graph and D a diagram over this graph.

The commutation of the diagram is easy: the colimit should be the tip of a cocone.

Definition 5.3 : Cocone

Let Q be a type. A cocone over D into Q is the data of arrows q i : D i → Q, and for any i, j : G and g : G(i, j), an homotopy q j • D(g) = q i .

If Q and Q ′ are type with an arrow f : Q → Q ′ , and if C is a cocone over D into Q, one can easily build a cocone on D into Q ′ by postcomposing all maps of the cocone by f , giving a map

cocone post : cocone D (Q) → (Q ′ : Type) → (Q → Q ′ ) → cocone D (Q ′ )
The other way around (from a cocone into Q ′ , give a map Q → Q ′ ) is exactly the second condition we seek: Definition 5.4 : Universality of a cocone Let Q be a type, and C be a cocone over

D into Q. C is said universal if for any type Q ′ , cocone post (C, Q ′ ) is an equivalence.
We can finally define what it means for Q to be a colimit of D. Definition 5.5 : Colimit A type Q is said to be a colimit of D if there is a cocone C over D into Q, which is universal.

Example

Let A, B be types and f , g : A → B. Let Q be the HIT generated by

q : B → Q α : q • f ∼ q • g .
Then Q is a colimit of the coequalizer diagram associated to A, B, f , g. We say that Q is a coequalizer of f and g.

Note that for any diagram D, one can build a free colimit of D, namely the higher inductive type colim(D) generated by

colim : i:G D i → colim(D) α colim : ij:G g:G(i,j) x:D i colim j • D(g) ∼ colim i 5.1.

Properties of colimits

Diagrams can be thought as functors from type of graphs to Type, and hence one can define morphisms between diagrams as natural transformation.

i : G, a map m i : D i → D ′ i • for all g : G(i, j), a path D ′ (g) • m i = m j • D(g)
This definition leads to obvious definition of identity morphism of diagrams, and composition of morphisms of diagrams.

Then, two diagrams D and D ′ are said to be equivalent if there is a morphism of diagrams m between D and D ′ such that all D i are equivalences. It can easily be checked that the morphism m -1 given by inverting all m i 's satisfies m • m -1 = id and m -1 • m = id.

In the previous section, we defined the map cocone post changing a cocone into Q and a map Q → Q ′ into a cocone into Q ′ . We now define a map cocone pre taking a morphism of diagrams m between D and D ′ , and a cocone over D ′ into X, and giving a cocone over D into X: Definition 5.7 Let m be a morphism of diagrams between D and D ′ , and X a type. Any cocone over D ′ into X can be changed into a cocone over D into X, by precomposing all maps in the cocone by the m i 's:

cocone pre : Hom(D, D ′ ) → cocone D ′ (X) → cocone D (X).
Precomposition by a morphism of diagrams and postcomposition by a morphism are compatible with composition and identities, in the sense that cocone pre (m

• m ′ ) = (cocone pre (m)) • (cocone pre (m ′ )) cocone pre (idmap) = idmap cocone post (ϕ • ϕ ′ ) = (cocone post (ϕ)) • (cocone post (ϕ ′ )) cocone post (idmap) = idmap
These properties allows us to express functoriality properties of colimits. If m is a morphism between diagrams D and D ′ , then cocone

-1 post • cocone pre is a map Q → Q ′ , where Q (resp. Q ′ ) is a colimit of D (resp. D ′ ).
One can even check that if m is an equivalence of diagrams, then the produced map Q → Q ′ is an equivalence of types. This is the lemma: Lemma 5.8 Let D and D ′ be two equivalent diagrams, with respective colimits Q and

Q ′ . Then Q ≃ Q ′ .
In particular, identity of diagrams being an equivalence, it asserts that the colimit of a diagram is unique (up to equivalence). From now on, as we supposed since chapter 3 the univalence axiom, we will say the colimit of a diagram.

One more interesting property of colimits is that it is stable by dependent sums. More precisely, let X be a type, and D x a diagram over a graph G for all x : X. We want to link the colimits Q x of diagrams D x with the colimit of x:X D x . Definition 5.9 : Dependent diagram Let G be a graph, X a type and D x a diagram over G for all x : X. The diagram x:X D x is the diagram defined by

• ( x:X D x ) (i) = x:X D x (i) • ( x:X D x ) (φ) = (idmap, D x (φ))
Note that a family C x of cocones over D x can be extended to a cocone x:X C x on x:X D x . Then, the expected result is true Proposition 5.10 If, for all x : X, Q x is the colimit of D x , then x:X Q x is the colimit of x:X D x .

Truncated colimits

As said in the introduction, we now give a truncated version of colimits. Colimits actually behave well with respect to truncations. Indeed, if D is a diagram and P a colimit of D, then P n is the n-colimit of the n-truncated diagram D n . Let's make it more precise.

• ( D n ) 0 (i) def = D 0 (i) n : Type n • ( D n ) 1 (φ) def = |D 1 (φ)| n : D 0 (i) n → D 0 (j) n
Definition 5.12 Let D be a diagram over a graph G, P be a type, and C a cocone over

D into P. C is said n-universal if for any Q : Type n , cocone post (C, Q) is an equivalence.
Then, P is said to be a n-colimit of D if there is a cocone C over D into Q which is n-universal.

We can now give the fundamental proposition linking colimit and n-colimit.

Proposition 5.13

Let D be a diagram, and

P : Type. Then, if P is a colimit of D, P n is a n-colimit of D n .
The proof of this is really straightforward: a cocone over D into P can be changed equivalently into a cocone over D n into P n , using the elimination principle 3.16 of truncations, and then we can show that the following diagram commutes for any X : Type

n P n → X G G ∼ cocone( D n , X) P → X ∼ G G cocone(D, X) ∼ y y

Nota

This result does not hold for limits. If it were true, then applying it to the following equalizer diagram

A λ_, y G G f G G B
with A, B : Type, f : A → B and y : B would lead to an equivalence

a:A f a = y n ≃ a: A n |f | n a = |y| n ,
proving left-exactness of n-truncation.

Towards highly coherent colimits

In category theory, a diagram over a graph G in a category C is a functor G → C. Our definition of diagrams doesn't reflect this definition, as we don't take care of composition of morphisms in the category (actually, we only define a map G → C). Diagrams over a category are defined in [HoTT,Exercise 7.16]. We will here define these diagrams, and the associated colimits.

Nota

This new definition of diagrams is not sufficient to reflect what we would want to express. If we view homotopy type theory as ω-topos theory, what we want is rather a ω-functor from a graph into the ω-topos. That is an important open problem in homotopy type theory (even defining simplicial types is an open problem). It requires to handle an infinity of coherence levels, with finite data. However, we could define, for any fixed n, diagrams and colimits coherent up to coherence level n (but that would be a real nightmare).

The main goal of this section is to define the colimit of the coequalizer with degeneracy δ

A g G G f G G B δ Ø Ø
and compositions c f : f • δ = idmap and c g : g • δ = idmap. We will use this coequalizer to define the Boulier's construction in next section 5.2.

If we only take the previous definition of colimits, what we miss is the commutation of the following diagram

q • f • δ q•c f G G α•δ q q • g • δ q•c g
Òur idea to define the colimit of this diagram with degeneracy is to add it directly into the definition of the higher inductive type:

colim : B → Q colim α : x:A f x = g x colim • α : y:B colim α (δ y) = c f (y) • c g (y) -1

Nota

We indeed see here why this idea cannot be extended to a fully coherent notion of colimits: we cannot define a higher inductive type with an infinity of constructors. Hopefully, adding this first level of coherence will be sufficient for our applications.

The new constructor colim • α indeed asserts the commutation of the desired diagram. We can view this higher inductive type as the same type as the colimit over the coequalizer graph, but which does not add already existing paths.

One can easily (but very technically) check that properties in section 5.1.2 are still satisfied by this new notion of colimit.

Van Doorn's and Boulier's constructions

In topos theory, there is a result that we would want to use in chapter 6:

Lemma 5.14 : [MM92, p. IV.7.8] In a topos E, if f ∈ Hom E (A, B) is an epimorphism, then the colimit of A × B A π 2 G G π 1 G G A is B. The pullback A × B A is called the kernel pair of f .
Unfortunately, this result fails in higher topos ; the kernel pair should be replaced by the Čech nerve of f .

. . . G G G G G G G G A × B A × B A G G G G G G A × B A G G G G A f colim G G B
The issue we face in homotopy type theory is that the definition of the Čech nerve, and in general of simplicial objects is a hard open problem. It involves an infinite tower of coherences, and we do not know how to handle this. However, there is a way to define a diagram depending on a map f , which colimit is Im(f ).

The starting point of the construction is Floris Van Doorn's construction of proposition truncation [START_REF] Van Doorn | Constructing the Proposition Truncation using Non-recursive HITs[END_REF].

Proposition 5.15 : Van Doorn's construction Let A : Type. We define the higher inductive type T A as the coequalizer of

A × A π 2 G G π 1 G G A .

The colimit of the diagram

A q G G T A q G G T T A q G G T T T A q G G . . . is A -1 .
Let's compare the direct definitions of A -1 and T A A -1 tr : A → A -1 α tr :

x,y: A -1 x = y T A q : A → T A α :

x,y:A q x = q y

The definitions are almost the same, except that the path constructor of T A quantifies over A, while the one of A -1 quantifies over A -1 itself: such a higher inductive type is a recursive inductive type. Thus, proposition 5.15 allows us to build the truncation in a non-recursive way. The counterpart is that we have to iterate the construction. In [START_REF] Boulier | Colimits in HoTT[END_REF], we found a way to generalize a bit this result. The main idea is that iterating the kernel pair construction will result in a diagram of colimit Im(f ). Now, let A, B : Type and f : A → B. We define the kernel pair of f as the coequalizer of

A × B A π 2 G G π 1 G G A .
In other words, KP(f ) is the higher inductive type generated by kp : A → KP(f ) α :

x,y:A

f x = f y → kp x = kp y
Using the eliminator of coequalizers, one can build a map f : KP(f ) → B, such that the following commutes

A kp G G f 4 4 KP(f ) f B
Then we can build KP( f ) and build a map f : KP( f ) → B, etc. We have the following result Proposition 5.16 : Boulier's construction For any f :

A → B, Im(f ) is the colimit of the iterated kernel pair diagram of f A G G KP(f ) G G KP f G G KP f G G • • • In particular, if f is a surjection, the colimit of this diagram is B.
Proof. The main idea of the proof is the equivalence between the diagrams

A G G KP(f ) G G KP f G G • • • y:B fib f (y) G G y:B T (fib f (y)) G G y:B T T (fib f (y)) G G • • •
Let's begin by showing the first non-trivial equivalence:

s : KP(f ) ≃ y:B
T (fib f (y)).

(5.1)

KP(f ) is the colimit of A × B A π 2 G G π 1 G G A ,

and

y:B T (fib f (y)) is the colimit of

y:B fib f (y) × fib f (y) G G G G y:B fib f (y) .
As the two diagrams are equivalent, their colimits are equivalent. We will need the following fact, easily checked

π 1 • s = f .
Now, let's prove the other equivalences. We need the following lemma Lemma 5.17 Let X, Y : Type and ϕ : X → Y . Then fib ϕ (y) ≃ T (fib ϕ (y)).

π 1 (x) = y ≃ T (fib ϕ (y))
Then, using the sum-of-fibers property, we can change the iterated kernel pair of f into

y:B fib f (y) G G y:B fib f (y) G G y:B fib f (y) G G • • •
With the just proved lemma, and a bit of induction, we can prove the desired equivalence of diagrams.

As colimits are stable under dependent sum, we know that the colimit of the diagram is thus

y:B Q y, where Q is the colimit of fib f (y) G G T (fib f (y)) G G T T (fib f (y)) G G • • •
But proposition 5.15 asserts that Q ≃ fib f (y) -1 , and the result is proved.

The main issue with Van Doorn's construction is that is does not preserve truncations levels at all. For example, when computing 1 -1 , the first step is T 1 ≃ S 1 , which is a 1-type. Asking for preservation of all truncation levels along the diagram might be too much, but the least we could ask is that when starting with a P : HProp, the diagram should be the constant diagram P → P → P → • • • . The Boulier counterpart of this is, when starting with an embedding f , all f are embeddings.

This can be achieved by changing operators T and KP, by asking them to preserve identities:

T A q : A → T A α :
x,y:A q x = q y α 1 :

x:A α(x, x) = 1 KP(f ) kp : A → KP(f ) α :
x,y:A f x = f y → q x = q y α 1 :

x:A α(x, x, 1) = 1
This new KP can be thought of as the coequalizer preserving the "degeneracy" δ, as in section 5.1.4:

A × B A π 2 G G π 1 G G A δ Õ Õ
Then, the following is still true Proposition 5.18 : Boulier's construction For any f :

A → B, Im(f ) is the colimit of the iterated kernel pair diagram of f A G G KP(f ) G G KP f G G KP f G G • • • Moreover, if f is an embedding, f also is.
The proof is almost the same as for proposition 5.16, except that the new constructors in the higher inductives types introduce another level of coherence, which is very technical to handle.

Sheaves in homotopy type theory

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 T , a boolean topos (i.e. satisfying the excluded middle property) satisfying the axiom of choice and negating the continuum hypothesis [MM92, Theorem VI.2.1]. This is actually an adaptation of a slightly older method, in set theory, to change a model M of ZFC into a model M[G] of ZFC, satisfying other principles, called forcing. It's most famous application is the proof of consistency of ZFC with the negation of the continuum hypothesis, by Paul Cohen [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF], answering (neither negatively nor positively) the first Hilbert's problem. Indeed, Gödel proved in 1938 the consistency of ZFC with continuum hypothesis [Göd38] using the constructible model L. The global idea of this technique is to add to the theory ZFC partial information about the witness of ¬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 all approximations, i.e. with a witness of ¬HC.

Then, forcing has been adapted to the setting of topos theory by Myles Tierney [START_REF] Tierney | Sheaf theory and the continuum hypothesis[END_REF], 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 T , one can build another topos -the topos of sheaves Sh(T ) -together with geometric embedding from Sh(T ) to T called sheafification. Depending on the sheaves we chose to treat, the topos Sh(T ) satisfies new principles. The construction of the geometric embedding is done in [MM92, Section V.3], and briefly recalled in section 6.1.

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 [HTT], 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 sheafi-fication 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 λµ-calculus of Parigot [START_REF] Parigot | Classical proofs as programs[END_REF], 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-passingstyle (CPS) transformation to type theory, but they have been faced with the difficulty that the CPS transformation is incompatible with (full) dependent sums [START_REF] Barthe | CPS translating inductive and coinductive types[END_REF], 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 [BBC98], Krivine's realizability [START_REF] Krivine | Dependent choice,'quote'and the clock[END_REF] and even more recently with restriction on elimination of dependent sums and lazy evaluation [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. The work on forcing in type theory [JTS12; Jab+16] also gives a computational meaning to a type theory enriched with new logical or computational principle. Section 6.2 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.

Sheaves in topoi

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 E, with subobject classifier Ω. A Lawvere-Tierney topology on E is a way to modify slightly truth values of E. It allows to speak about locally true things instead of true things. Definition 6.1 : Lawvere-Tierney topology [MM92] A Lawvere-Tierney topology is an endomorphism j : Ω → Ω preserving ⊤ (j ⊤ = ⊤), idempotent (j • j = j) and commuting with products (j • ∧ = ∧ • (j, j)).

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: Theorem 6.2 : [MM92, Theorem V.1.2] Every Grothendieck topology J on a small category C determines a Lawvere-Tierney topology j on the presheaf topos Sets C op .

Any Lawvere-Tierney topology j on E induces a closure operator A → A on subobjects. If we see a subobject A of E as a characteristic function χ A , the closure A corresponds to the subobject of E whose characteristic function is

χ A = j • χ A .
A subobject A of E is said to be dense when A = E. Then, we are interested in objects of E for which it is impossible to make a distinction between objects and their dense subobjects, i.e. for which "true" and "locally true" coincide. Such objects are called sheaves, and are defined as Definition 6.3 : Sheaves[MM92, Section V.2] On object F of E is a sheaf (or j-sheaf) if for every dense monomorphism m : A ֒→ E in E, the canonical map Hom E (E, F) → Hom E (A, F) is an isomorphism.

One can show that Sh E , the full sub-category of E given by sheaves, is again a topos, with classifying object

Ω j = {P ∈ Ω | jP = P}.
Lawvere-Tierney sheafification is a way to build a left adjoint a j to the inclusion E ֒→ Sh ( E), exhibiting Sh(E) as a reflective subcategory of E. In particular, that implies that logical principles valid in E are still valid in Sh(E).

For any object E of E, a j (E) is defined as in the following diagram

E {•} E G G θ E Ω E j E E ′ G G closure 2 2 Ω E j a j (E) a a
The proof that a j defines a left adjoint to the inclusion can be found in [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF].

One classical example of use of sheafification is the construction, from any topos, of a boolean topos negating the continuum hypothesis. More precisely: Theorem 6.4 : Negation of CH [MM92, Theorem VI.

2.1]

There exists a Boolean topos satisfying the axiom of choice, in which the continuum hypothesis fails.

The proof actually follows almost exactly the famous proof of the construction by Paul Cohen of a model of ZFC negating the continuum hypothesis [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF]. Together with the model of constructible sets L by Kurt Gödel [START_REF] Gödel | The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory[END_REF], it proves that CH is independent of ZFC, solving first Hilbert's problem.

Sheaves in homotopy type theory

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 Ω of a topos are very close to those of a modality on Ω. We will extensively use this idea, applying it to every subobject classifier Type n we described in 3.4. The subobject classifier Ω of a topos is seen as the 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 [HoTT,Example 8.8.6]. Even worse, it seems that some types are not even the limit of its successive truncations, even in a hypercomplete setting [START_REF] Morel | A 1 -homotopy theory of schemes[END_REF]. 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 [MM92, Theorem IV.7.8], 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 -1 . The reader can think of the double negation ¬¬ defined in 4.2.3. We will define, by induction on the truncation level, left-exact modalities on all Type n , as in the following theorem.

Theorem 6.5

The sequence defined by induction by

: ∀ (n : nat), Type n → Type n -1 (T ) def = j T n+1 (T ) def = u:T →Type n -1 a:T u = (λt, n (a = t))
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 P is P seen as an inhabitant of Type n+1 .

P ∼ G G η n P η n+1 n P ∼ G G n+1 P

Sheaf theory

Let n be a truncation index greater that -1, and 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 n , one can build a closure operator.

Definition 6.6 : (cloture,closed,EnJ) Let E be a type.

• The closure of a subobject of E with n-truncated homotopy fibers (or n-subobject of E, for short), classified by χ : E → Type n , is the subobject of E classified by n • χ.

• An n-subobject of E classified by χ is said to be closed in E if it is equal to its closure, i.e. if χ = n • χ.

• An n-subobject of E classified by χ is said to be dense in E if its closure is E, i.e. if n • χ = λe, 1

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. Definition 6.7 : Restriction (E_to_χmono_map, E_to_χ_map) Let E, F : Type and χ : E → Type. We define the restriction map

Φ χ E as Φ χ E : E → F -→ e:E χe → F f -→ f • π 1 .
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. Definition 6.8 : Separated Type (separated) A type F in Type n+1 is separated if for any type E, and all dense n-subobject of E classified by χ, Φ χ E is an embedding.

With topos theory point of view, it means that given a map e:E χ e → F, if there is an extension f : E → F, then it is unique, as in

e:E χe f G G π 1 F E ! Y Y
Definition 6.9 : Sheaf (Snsheaf_struct) A type F of Type n+1 is a (n + 1)-sheaf if it is separated, and for any type E and all dense (-1)subobject of E classified by χ, Φ χ E is an equivalence.

In topos-theoretic words, it means that given a map f : e:E χ e → F, one can extend it uniquely to f :

E → F, as in e:E χe f G G π 1 F E ∃! Y Y
Note that these definitions are almost the same as the ones in [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF]. 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. Proposition 6.10 : (nj_paths_separated) A type F is Type n+1 is separated if, and only if all its path types are n-modal, ie

x,y:F ( n (x = y)) = (x = y).

A (n + 1)-sheaf is hence just a type satisying the usual property of sheaves (i.e. 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 IsSeparated (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 leftexactness).

Proposition 6.11 : (nType_j_Type_is_SnType_j_Type) Type n is a (n + 1)-sheaf.

Proof. We have two things to prove here : separation, and sheafness.

• Let E : Type and χ :

E → Type, dense in E. Let φ 1 , φ 2 : E → Type n , such that φ 1 • π 1 = φ 2
• π 1 and let x : E. We show φ 1 (x) = φ 2 (x) using univalence.

As χ is dense, we have a term m x : n (χ x). But as φ 2 (x) is modal, we can obtain a term h x : χ x. As φ 1 and φ 2 are equal on e:E χ e, we have an arrow φ 1 (x) → φ 2 (x). The same method leads to an arrow φ 2 (x) → φ 1 (x), and one can prove that they are each other inverse.

• Now, we prove that Type n is a sheaf. Let E : Type and χ : E → HProp, dense in E. Let f : e:E χ e → Type n . We want to extend f into a map E → Type n .

We define g as g(e) = n fib φ (e) , where

c:C n (fib g•f (c)) ≃ n          w:fib g (c) n (fib f (w 1 ))          .
Proof. This is just a modal counterpart of the property characterizing fibers of composition of function.

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. Proposition 6.13 : (dep_prod_SnType_j_Type) If A : Type n+1 and B : A → Type n+1 such that for any a : A, (B a) is a sheaf, then a:A B a is a sheaf.

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.

• Separation: Let E : Type and χ : E → Type n dense in E. Let φ 1 , φ 2 : E → a:A B a equal on e:E χ e i.e. such that φ 1 • π 1 = φ 2 • π 1 . Then for any a : A, (λx : E, φ 1 (x, a)) and (λx : E, φ 2 (x, a)) coincide on e:E (χ e), and as B a is separated, they coincide also on all E.

• Sheaf: Let E : Type, χ : E → HProp dense in E and f : e:E χ e → a:A B a. Let a : A ; the map (λ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.

Sheafification

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

Let n be a fixed truncation index, and n a left-exact modality on Type n , compatible with -1 as in Condition 6.14 For any mere proposition P (where P is P seen as a Type n ), n P = -1 P and the following coherence diagram commutes

P ∼ G G η -1 P η n -1 P ∼ G G n P
From types to separated types Let T : Type n+1 . We define n+1 T as the image of T n • {•} T , as in

T {•} T G G µ T (Type n ) T T n n+1 T G G Type n T ,
where {•} T is the singleton map λ(t : T ), λ(t ′ : T ), t = t ′ . n+1 T can be given explicitly by

n+1 T def = Im(λ t : T , λ t ′ , n (t = t ′ )) def = u:T →Type n a:A (λt, n (a = t)) = u .
This corresponds to the free separated object used in the topos-theoretic construction, but using Type n instead of the j-subobject classifier Ω j .

Proposition 6.15 : (separated_Type_is_separated) For any T : Type n+1 , n+1 T is separated.

Proof. We use the following lemma: Lemma 6.16 : (separated_mono_is_separated) A (n + 1)-truncated type T with an embedding f : T → U into a separated (n + 1)-truncated type U is itself separated.

Proof. Let E : Type and χ :

E → Type n dense in E. Let φ 1 , φ 2 : e:E χ e → T such that φ 1 • π 1 ∼ φ 2 • π 1 . Postcomposing by f yields an homotopy f • φ 1 • π 1 ∼ f • φ 2 • π 1 . As f • φ 1 , f • φ 2 :
e:E χ e → U , and U is separated, we can deduce f

• φ 1 ∼ f • φ 2 . As f is an embedding, φ 1 ∼ φ 2 .
As n+1 T embeds in Type n T , we only have to show that the latter is separated. But it is the case because Type n is a sheaf (by Proposition 6.11) and a function type is a sheaf as soon as its codomain is a sheaf (by Proposition 6.13).

We will now show that n+1 defines a modality, with unit map µ. The left-exactness of n+1 will come from the second part of the process. The first thing to show that n+1 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 5.18. Here is a sketch of the proof: as µ T is a surjection (it is defined by the surjection-embedding factorization), n+1 T is the colimit of its iterated kernel pair. Hence, for any type Q defining a cocone on KP(µ T ), there is a unique arrow n+1 T → Q. What remains to show is any separated type Q defines a cocone on KP(µ T ) ; we will actually show that any separated type Q defines a cocone on KP(µ T ) n+1 , which is enough. We do it by defining another diagram T , equivalent to KP(µ 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 n+1 T to the colimit of the iterated kernel pair of µ T . This lemmas allows to prove that, in the iterated kernel pair

diagram of f X G G f A A KP(f ) G G f 1 7 7 KP(f 1 ) G G f 2 KP(f 2 ) G G f 3 y y • • • S if f satisties 6.
(a) = f (b) ≃ (a = b), then Coeq 1           a,b:A f a = f b π 2 G G π 1 G G A           ≃ Coeq 1           a,b:B (a = b) π 2 G G π 1 G G B           Proof of lemma 6.18. As said, it suffices to show that C(µ T ) n+1 = T . KP 0 (µ T ) n+1 G G ∼ KP 1 (µ T ) n+1 G G ∼ KP 2 (µ T ) n+1 G G ∼ • • • T0 G G T1 G G T2 G G • • •
The first equivalence is trivial. Let's then start with the second. What we need to show is

KP(µ T ) n+1 ≃ TT n+1 , i.e. Coeq 1           a,b:T µ T a = µ T b π 2 G G π 1 G G T           ≃ Coeq 1           a,b:T (a = b) π 2 G G π 1 G G T           .
By the previous remark, it suffices to show that µ T satisfies condition (6.1), i.e. ∀a, b : T , n (a = b) = (µ T a = µ T b). By univalence, we want arrows in both ways, forming an equivalence.

• Suppose p : (µ T a = µ T b). Then projecting p along first components yields q : t:T n (a = t) = n (b = t). Taking for example t = b, we deduce n (a = b) = n (b = b), and the latter is inhabited by η b=b 1.

• Suppose now p : n (a = b). Let ι be the first projection from n+1 T → (T → Type n ). ι is an embedding, thus it suffices to prove ι(µ

T a) = ι(µ T b), i.e. t:T n (a = t) = n (b = t).
The latter remains true by univalence.

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 (µ T ) n+1 ≃ Ti . We want to prove KP i+1 (µ T ) n+1 ≃ Ti+1 , i.e.

Coeq 1            a,b:KP i (µ T ) f i a = f i b π 2 G G π 1 G G KP i (µ T )            n+1 ≃ Coeq 1            a,b: Ti n+1 (a = b) π 2 G G π 1 G G Ti n+1            n+1
where f i is the map KP i (µ T ) → n+1 T . But lemma 6.19 just asserted that f i satisfies 6.1, 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. Now, let Q be any separated Type n+1 , and f : X → Q. Then the following diagram commutes

X n+1 G G 7 7 TX n+1 G G T TX n+1 y y G G • • • Q
But we know (lemma 6.18) that n+1 T is the (n + 1)-colimit of the diagram T , thus there is an universal arrow n+1 T → Q. This is enough to state the following proposition. Proposition 6.20 : (separation_reflective_subuniverse) ( n+1 , µ) defines a reflective subuniverse on Type n+1 .

To show that n+1 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 → Type n+1 be a family of separated types. We want to show that x:A B x is separated. Let E be a type, and χ : E → Type n a dense subobject of E.

Let f , g be two maps from e:E χ e to x:A B x, equal when precomposed with π 1 .

e:E χ e

g•π 1 G G f •π 1 G G dense x:A B x E g X X f X X
We can restrict the previous diagram to e:E χ e

π 1 •g•π 1 G G π 1 •f •π 1 G G dense A E π 1 •g X X π 1 •f X X
and as A is separated, π 1 •f = π 1 •g. For the second components, let x : E. Notice that y:E x = y has a dense n-subobject, y: e:E χ e x = y 1 :

y: e:E χ e x = y 1

π 2 •f •π 1 •π 1 G G π 2 •g•π 1 •π 1 G G dense B x y:E x = y π 2 •f •π 1 T T π 2 •g•π 1 T T
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 Proposition 6.21 : (separated_modality) ( n+1 , µ) defines a modality on Type n+1 .

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.

From Separated Type to Sheaf

For any T in Type n+1 , n+1 T is defined as the closure of n+1 T , seen as a subobject of T → Type n . n+1 T can be given explicitly by To prove that n+1 T is a sheaf for any T : Type n+1 , we use the following lemma.

Lemma 6.22 : (closed_to_sheaf) Any closed (-1)-subobject of a sheaf is a sheaf.

Proof. Let U be a sheaf, and κ : U → HProp be a closed (-1)-subobject. Let e : E. As χ is dense, we have a term w : n (χ e), and by n -induction, a term w : χ e. Then, by retraction property, ψ(e) = φ(e, w), and by π 2 • φ, we have hence our term of type κ(ψ e).

As T → Type n is a sheaf, and n+1 T is closed in T → Type n , n+1 T is a sheaf. We now prove that it forms a reflective subuniverse. Proposition 6.23 : (sheafification_subu) ( n+1 , ν) defines a reflective subuniverse.

Proof. Let T , Q : Type n+1 such that Q is a sheaf. Let f : T → Q. Because Q is a sheaf, it is in particular separated; thus we can extend f to n+1 f : n+1 T → Q.

But as n+1 T is the closure of n+1 T , n+1 T is dense into n+1 T , so the sheaf property of Q allows to extend n+1 f to n+1 f : n+1 T → Q.

As all these steps are universal, the composition is.

The next step is the closure under dependent sums, to state: Proposition 6.24 : (sheafification_modality) ( n+1 , ν) defines a modality.

Proof. The proof uses the same ideas as in subsection 6.2.2. Let A : Type n+1 a sheaf and B : A → Type n+1 a sheaf family. By proposition 6.21, we already know that a:A B a is separated. Let E be a type, and χ : E → HProp a dense subobject. Let f : e:E χ e → x:A B x ; we want to extend it into a map E → x:A B x.

e:E χ e f G G

x:A B x E V V
As A is a sheaf, and π 1 •f : e:E χ e → A, wa can recover an map g 1 : E → A. We then want to show e:E B(g 1 e). Let e : E. As χ is dense, we have a term w : n (χ e), and as B(g 1 e) is a sheaf, we can recover a term w : χ e. Then g 1 (e) = f (e, w), and π 2 • f gives the result.

It remains to show that n+1 is left exact and is compatible with -1 . To do that, we need to extend the notion of compatibility and show that actually every modality n+1 is compatible with n on lower homotopy types. Proposition 6.25 If T : Type n , then n+1 T = n T , where T is T seen as a Type n+1 .

Proof. We prove it by induction on n:

• For n = -1: Let T : HProp. Then where κ is defined by -1 -induction on t. Indeed, as T is an HProp, (a = t) ≃ 1. Let ψ : 0 T → -1 T by obtaining the witness a : T (which is possible because we are trying to inhabit a modal proposition), and letting ψ(u; x) = η T a. These two maps form an equivalence (the section and retraction are trivial because the equivalence is between mere propositions).

• Suppose now that n+1 is compatible with all k on lower homotopy types. Let n+2 be as above, and let T : Type n+1 . Then, as n+1 is compatible with n , and (a = t) is in Type n , .

It remains to prove that for every (u, x) inhabiting the Σ-type above, u is in T → Type n , i.e. that for every t : T , Is-n-type(u t). But for any truncation index p, the type Is-p-type X : HProp is a sheaf as soon as X is, so we can get rid of -1 and of the truncation, which tells us that for every t : T , u t = n (a = t) : Type n .

This proves in particular that n+1 is compatible with -1 in the sense of condition 6.14. The last step is the left-exactness of n+1 . Let T be in Type n+1 such that n+1 T is contractible. Thanks to the just shown compatibility between n+1 and n for Type n , left exactness means that for any x, y : T , n (x = y) is contractible.

Using a proof by univalence as we have done for proving n (a = b) ≃ (µ T (a) = µ T (b)) in Proposition 6.18, we can show that: As n+1 T is contractible, path spaces of n+1 T are contractible, in particular (ν T a = ν T b), which proves left exactness.

• The definition of the dense topology as a left exact modality on HProp is given in sheaf_base_case.v.

• Section 6.2.1 is formalized in sheaf_def_and_thm.v.

• Section 6.2.2 is formalized in sheaf_induction.v.

Overall, 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 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ï.

Limitations of the formalization

In the formalization, we had to use the 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 [START_REF] Sozeau | Universe Polymorphism in Coq[END_REF] 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 Σ-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.

One issue with universe polymorphism lies in the management of recursive definitions. Indeed, the following recursive definition of sheafification 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 n+1 should be at least one level higher as the one of Type n occurring in n because of the use of Σ-type over T → Type n and equality on the return type of n . 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 [START_REF] Ahrens | Univalent Categories and the Rezk completion[END_REF]. In the definition of the completion, they use the Yoneda embedding and representable functors, which is similar to our use of characteristic functions.

Conclusion and future works

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 [HTT] and this theory. More precisely, homotopy type theory is expected to be the internal language of (∞, 1)-toposes.

In homotopy type theory, types are classified by their 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 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 [HTT, Section 6.2.2]. In homotopy type theory, a modality is an operator on Type, together with unit maps η : X:Type X → X satisfying properties. They can be seen just as idempotent monads. Relying on the equivalence between type theory and (∞, 1)-toposes, one can conjecture that modalities -actually, accessible leftexact modalities -induces reflective sub-type theories. In this thesis, we want to describe a classical type theory (i.e. 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 T , and the double-negation Lawvere-Tierney topology, and build the topos of sheaves Sh ¬¬ (T ). Then the latter is a boolean topos (i.e. 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, 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) 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:

Id( A :

 A Type)(a : A) : A → Type généré par un seul constructeur idpath : Id A (a, a), et le type Id(A, a, b) sera noté a = A b ou a = b. Ce type identité n'est en fait pas satisfaisant.

Figure 1 . 1 :

 11 Figure 1.1 : Traduction de Gödel-Gentzen

  soit une équivalence. On note que si A = B, alors il existe une équivalence canonique entre A et B, et on note idtoequiv : A = B → A ≃ B. On peut alors énoncer l'axiome d'univalence : Axiome 1.2 Pour tous types A et B, la fonction idtoequiv : A = B → A ≃ B est une équivalence.

  Le premier exemple est le cercle S 1 . Il est généré par les constructeurs base : S 1 loop : base = base On peut le représenter par • loop ' ' base Comme pour les types inductifs, on donne aussi des éliminateurs pour les HIT. Exemple Donnons l'éliminateur non-dépendant de S 1 . Si P est un type, b : P et p : b = b, alors il existe une fonction S 1 rec : S 1 → P tel que S 1 rec (base) ≡ b et ap S 1 rec (loop) = p. L'éliminateur dépendant est un peu plus compliqué. Si P : S 1 → Type est une famille de type sur S 1 , b : (Pbase) et p : transport loop P (b) = b, alors il existe un terme ) ≡ b et ap S 1 ind (loop) = p.

  autre sens correspond à notre définition de colimite : Définition 1.6 : Colimite Un type Q est une colimite de D s'il existe un cocone C sur D dans Q, qui est universel, i.e. tel que postcompose cocone (C, Q ′ ) soit une équivalence.

Définition 1. 10

 10 Une modalité exacte à gauche est la donnée de (i) Un prédicat P : Type → HProp (ii) Pour tout type A, un type A tel que P( A) (iii) Pour tout type A, une fonction η A : A → A tels que (iv) Pour tous types A et B, si P(B) alors

  pour tous A : Type et B : A → Type tels que P(A) et x:A P(Bx), alors P ( x:A B(x)) 1.4. MODALITÉS (vi) pour tous A : Type et x, y : A, si A est contractible, alors (x = y) est contractible.

  If A and B are two types, we would like to define the type of pairs (a, b), where a : A and b : B. The resulting type is called the product of A and B, noted A × B.

  A and B are types, f : A → B and b : B, the particular dependent sum a:A f a = b is called the fiber of f over b, noted fib f (b). It describes the inverse image of b by f .

  called the adjunction of the equivalence We say that A and B are equivalent, noted A ≃ B, if there is a function f : A → B which is an equivalence.

  we give the elimination principle of the circle. We start by the non-dependent eliminator. Lemma 3.7 : Non-dependent elimination of S 1 Let P be a type. If b : P and p : b = b, then there is a map S 1 rec : S 1 → P such that S 1 rec (base) ≡ b (judgementally) and ap S 1 rec (loop) = p (propositionally).

Lemma 3. 8 :

 8 Dependent elimination of S 1 Let P : S 1 → Type be a type family over S 1 . If b : P(base) and p : transport loop P (b) = b, then there is ind (base) ≡ b and ap S 1 ind (loop) = p.

  then there is a dependent map Coeq f ,g ind : x:Coeq f ,g P x such that for all b : B, Coeq f ,g ind (q b) ≡ q ′ b and ap Coeq f ,g ind (α b) = α ′ b.

  S) ≡ s and for all a : A, ap Σ A rec (merid(a)) = m(a) • Let P : ΣA → Type. If there are n : P(N ), s : P(S) and m : a:A transport merid(a) P n = s, then there is a dependent map Σ A ind : that Σ A ind (S) ≡ s, Σ A ind (N ) ≡ n and ap Σ A ind (merid(a)) = m(a).

2 Figure 3 . 1 :

 231 Figure 3.1: Paths: a and b are points, p 1 and p 2 paths, H 1 and H 2 homotopies.

Proposition 4. 3

 3 Any left-exact modality satisfies the following properties 1 .

  M) If A, B : Type are modal, then so are Is-n-type A, A ≃ B and IsEquiv f for all f : A → B. •(L) If A : Type n , then A : Type n . •(L) If A, B : Type and f : A → B, then the map

Lemma 4. 4

 4 Let A : Type, B : Type and f : A → B. If for all b : Y , (fib f (b)) is contractible, then A ≃ B.

Lemma 4. 5

 5 Let A, B : Type. Let f : A → B. If A and B are contractible, then so is fib f (b) for any b : B.

  η A x = y for any y : A. Let Cover : A → Type be defined by induction by Cover(y) def = rec (λy, (x = y)). Note that for any y : A, Cover(y) is always modal. We will show that η A x = y ≃ Cover(y). Now, let Encode : y: A η A x = y → Cover(y) be defined by Encode(y, p) def = transport p Cover transport β rec ((λz, (x=z)),x) idmap (η x=x 1) and Decode : y: A Cover(y) → η A x = y by Decode def = ind λy p, (ap η A ) transport β rec ((λz, (x=y)),y) idmap p

  We want a term η A of type A → ¬¬A. Taking η A def = λ x : A, λ y : ¬A, y a do the job. Now, we can define P to be exactly A:Type IsEquiv η A . (iv) Let A, B : Type, and ϕ : A → ¬¬B. We want to extend it into ψ : ¬¬A → ¬¬B. Let a : ¬¬A and b : ¬B. Then a(λ x : A, ϕ x b) : 0, as wanted. One can check that it forms an equivalence. (v) Let A : Type and B : A → Type such that P(A) and a:A P(B a). There is a map x:A B x → A thus by the preivous point, we can extend it into κ : ¬¬ x:A B x → A.

  Proposition 4.11 If Γ ⊢ A : Type, Γ, x : A ⊢ B : Type and Γ, x : A ⊢ b : B, then [b[a/x]] ≡ [b][[a]/x]. Proof. It can be shown directly by induction on the term b.

A:

  Type B: S A→Type a:A B(η S A a) → a: S A B a.

Modal

  Definition allows to give a definition in the reflective subuniverse; Modal Definition foo : bar using open a new goal of type [bar], waits for the user to give a proof, and define a new term foo m : [bar] and a new constant foo : bar at the Defined command. Then, it adds in T a new pair (foo, foo m ). Modal Translate allows to translate automatically a previously existing constant or inductive type. If foo def = qux : bar is a constant, Modal Translate foo using computes the value of [foo], and add in T the pair (foo, [foo]). If I (x 1 : A 1 ) • • • (x n : A n ) : Type is an inductive type with p constructors C i : T i , then the plugin builds a new inductive type

Definition 5. 6 :

 6 Morphism of diagram Let D and D ′ be two diagrams over the same graph G. A morphism of diagram m between D and D ′ is the data of • for all

  Definition 5.11 : Truncation of a diagram Let D be a diagram over a graph G, and n a truncation index. Then the diagram D n is the diagram over G defined by

Proof.

  We have the following sequence of equivalences: fib ϕ (y) def = x:KP(ϕ) ϕ x = y ≃ x: y:B T (fib ϕ (y)) ϕ • s -1 (x) = y by 5.1 ≃ x: y:B T (fib ϕ (y))

  :E χ e (f b) → E defined by φ(x) = (x 1 ) 1 . Using the following lemma, one can prove that the map f → g defines an inverse of Φ χ E . Lemma 6.12 : (nj_fibers_compose) Let A, B, C : Type n , f : A → B and g : B → C. Then if all fibers of f and g are n-truncated, then

  n (a = t)) = u .

  Let E : Type and χ : E → HProp dense in E. Let φ : e:E χ e → u:U κ u. As π 1 • φ is a map e:E χ e → U and U is a sheaf, it can be extended into ψ : E → U . As κ is closed, it suffices now to prove e:E n (κ (ψ e)) to obtain a map E → u:U κ u.

  -1 (a = t)) = u       because the type inside the truncation is already in HProp. Now, let define φ : -1 T → 0 T by φt = (λt ′ , 1; κ)

  n (a = t)) = u -1

  Proposition 6.26 : (good_sheafification_unit_paths_are_nj_paths) For all a, b : T , n (a = b) ≃ (ν T a = ν T b).

:

  ∀ (n : nat), Type n → Type n -1 (T ) λt, n (a = t))

  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 ∈ E et x ∈ F en théorie des ensembles (c'est la définition de x ∈ E ∩ 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 :

			Propositions comme
	Nom	Notation	des types
	Zéro

x ∈ 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".

  Soient A, B : Type et f : A → B. On dit que f est une équivalence, noté IsEquiv(f ) s'il existe • une fonction g : B → A, appelée inverse de f • un terme retr f :

	compatible avec la structure d'ω-groupoïde.
	Avant de lier les type identités avec les types d'équivalence, définissons d'abord les équiva-
	lences.
	Définition 1.1

  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 . 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 -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 :

	Le classifiant Ω d'un topos est vu
	comme l'ensemble des 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 fais-
	ceautisation 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 [HoTT, Example
	8.8.6]. Théoreme 1.1
	La suite définie par induction par

  • 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 χ, Φ En terme de diagrammes, un faisceau est donc un objet F tel que pour tous E : Type, χ n : E → Type n , χ -1 : E → HProp, f n : e:E χ n e → F et f -1 : e:E χ -1 e → F, les diagrammes suivants commutent Type n+1 et B : A → Type n+1 tels que pour tout a : A, (B a) est un faisceau, alors

		χ E est un plongement.
	• 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 χ, Φ χ E est une équivalence.
		e:E χ n e	f n G G F Y Y	e:E χ -1 e	f -1 G G F X X
		π 1	!	π 1	∃!
		E		E
	On a alors
	Proposition 1.15	• Type n est un (n + 1)-faisceau.
	• Si A :

a:A B a est un faisceau.

  T est bien un faisceau, car objet clos dans un faisceau, et 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 n+1 est exacte à gauche, et on a donc bien étendu notre modalité sur Type n à une modalité sur Type n+1 .

			équivalents, et on a donc
	Lemme 1.17
	Soit T : Type n+1 . Alors n+1 T est la (n + 1)-colimite du diagramme T .
	Cela suffit pour affirmer que ( n+1 , µ) est une modalité.
	Passons maintenant à la deuxième étape. Pour T : Type n+1 , on définit n+1 T comme la clôture de n+1 T vu comme sous-objet de T → Type n . n+1 T peut être donné explicitement par
	n+1 T	def =	-1	(λt, n (a = t)) = u .
		u:T →Type n	a:T

n+1

  y, p]The elimination principle should be looked closer. Lets simplify to understand how it works: suppose that the type family P depends only on two objects x, y : A. Then if C is reflexive, i.e. if C(x, x) is always inhabited, then whenever x = y, C(x, y) is inhabited too.Path-induction, also known as "J principle", allow us to state the following:

Lemma 3.1 : [HoTT, Lemma 2.3.1] Let A : Type and P : A → Type a type family over A. Then if p : x = A y, there is a function transport p P : P x → P y.

Proof. Let's do this proof to use path-induction for the first time. Let Q be the type family indexed by x, y : A Q(x, y) := P x → P y.

  1, then each |f i | n+1 does. Nota It is clear that if A and B are equivalent types, and ∀a, b : A, f

Note that, to ease the reading, some references are shortcutted by their usual names:[HoTT] is the Homotopy Type Theory book,[HoTT/Coq] is the Coq/HoTT library,[HTT] is Lurie's monograph Higher topos theory, etc.

In type theory, the argument is harder to prove, and is called Girard's paradox.

We will see in chapters 4 and 6 that we sometimes need to "help" Coq

The type of dependent functions with source type A and target type B x is called "dependent product over B" (or "pi-type over B"), and will be denoted x:A B x or (x : A) → (B a). When B does not depend on A, we just say "arrow type" and note it A → B.The introduction and elimination rules of dependent products are:Γ, x : A ⊢ b : B -intro Γ ⊢ λ (x : A), b : x:A B

Acknowlegdments

First of all, I would like to thank Nicolas Tabareau for the time he spent helping me. All this thesis is also his work, and I would never have finished it withour his help. Without him, I would never have discovered homotopy type theory and computer-checked proofs ; even worse, I would have become a set theorist. Thank you again for avoiding this. I am also grateful to Matthieu and Tom for accepting to review my wiork during three years ; these discussions were 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.

Formalization

All this chapter has been formalized with Coq, defining a library for colimits on top of the Coq/HoTT library [HoTT/Coq], based on the formalization of limits in [START_REF] Avigad | Homotopy limits in type theory[END_REF] for the basic definitions of graph, diagram, etc.

The root folder of the library formalizes results about general colimits over graphs, with the following key results:

• Colimit_prod.is_colimit_prod shows that if D is a diagram, and A × D the diagram where each node X of D is changed into X × D, then A × colimD is a colimit of A × D.

• Colimit_Sigma.is_colimit_sigma shows the commutation of colimits with dependent sums, as in proposition 5.10.

• Colimit_trunc.tr_colimit shows the proposition 5.13 about truncated colimits.

The second part of the library, in folder IteratedKernelPair, formalizes the section 5.2. We note that the formalization for the kernel pair preserving degeneracy involves a lot of manipulation of paths between paths. Definition 6.17 : (OTid) Let X : Type. Let TX be the higher inductive type generated by

We consider the diagram T :

The main result we want about T is the following:

The key point of the proof is that diagrams T and KP(µ T ) n+1 are equivalent. We will need the following lemma: Lemma 6.19 : (OT_Omono_sep) Let A, S : Type n+1 , S separated, and f :

Sketch of proof. By induction on truncation, we need to show that

We use the encode-decode [HoTT, Section 8.9] method to characterize f (|a| n+1 ) = x, and the result follows. We refer to the formalization for details.

Summary

Starting from any left-exact modality -1 on HProp, we have defined for any truncation level n, a new left-exact modality n on Type n , which corresponds to -1 when restricted to HProp. When -1 is consistent (in the sense of proposition 4.13), n 0 = -1 0 is also not inhabited, hence 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: Proposition 6.27 Taking ( ¬¬ ) n , the modality obtained by sheafification of the double negation modality, the following holds P:HProp ¬¬ (P + ¬P).

Proof. Let P : HProp, and pose Q def = P + ¬P. Then, as P and ¬P are disjoint h-propositions, P + ¬P is itself a h-proposition [HoTT/Coq, ishprop_sum]. Thus, ¬¬ Q ≃ ¬¬Q, and the latter is inhabited by the usual λ (x : ¬Q), x(inr(λ y : P, x(inl y))).

Extension to Type

In the previous section, we have defined a (countably) infinite family of modalities Type i → Type i . One can extend them to whole Type by composing with truncation: Lemma 6.28 Let i : Type i → Type i be a modality. Then

If -1 is the double negation modality on HProp and i = -1, is exactly the double negation modality on Type described in 4.2.3. Chosing i 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 [HoTT, Exercise 7.11], isn't either. But in the following sense, when restricted to i-truncated types, it is:

Proof. For i-truncated types, = i , and i is left-exact.

The compatibility between the modalities n and between the modalities • 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 (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.

Furthermore, the univalence remains true in this new type theory in the following sense: Proposition 6.30

Let n be a given truncation index, and the modality associated to n as defined in lemma 6.28. Then, for any type A, B : Type n , if ϕ is the canonical arrow

then IsEquiv(ϕ) is modal.

Proof. The first thing to notice is that, if X and Y are modal, and f : X → Y , then the mere proposition IsEquiv f is also modal. Therefore, it suffices to show that both A = B and A ≃ B are modal. By proposition 4.3, A = B is modal. Moreover, (A ≃ B) ≃ f :A→B IsEquiv f . Therefore, as A and B are modal, A ≃ B is too. Hence, IsEquiv ϕ is modal.

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 M be a model of homotopy type theory with one universe. Using the modality ¬¬ (for any level n) associated to the sheafification, there is a model ¬¬ M of type theory with one universe (using results in Section 4.5), where excluded middle is true, and which is univalent (as shown in Proposition 6.30). After reviewing the content and some statistics about the formalization in Section 6.3.1, we present the limitations of our formalization in Section 6.3.2, in particular the issues relative to universe polymorphism.

Formalization

Content of the formalization

We provide a more detailed insight of the structure of our formalization:

• Colimits and iterated kernel pairs are formalized in Limit, T.v, OT.vv OT_Tf.v, T_telescope.v, Tf_Omono_sep.v.

• Reflective subuniverses and modalities are formalized in reflective_subuniverse.v, modalities.v.

CHAPTER 7. CONCLUSION AND FUTURE WORKS

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 [START_REF] Morel | A 1 -homotopy theory of schemes[END_REF]. 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 [HoTT,Section 8.8] or Postnikov principle [HTT, Section 5.5.6], and use it to build a real modality on Type.

Lawvere-Tierney sheaves in higher topos theory. If we rely on the leitmotiv Homotopy type theory is the internal language of (∞, 1)-topos, we could transpose our work to higher topos theory. As there are more tools in topos theory (e.g. 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 [Rez], inspired by the homotopy-type-theoretic proof by Peter LeFanu Lumsdaine, Eric Finster and Dan Licata.

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 Grothendieck topologies [MM92, Chapter III], and one can show that Lawvere-Tierney topologies on a presheaf topos Sets C op correspond exactly to Grothendieck topologies on C. Then, we have the following: Theorem 7.1 : [MM92, Section V.4, theorem 2] Let C is a small category and j a Lawvere-Tierney topology on Sets C op , while J is the corresponding Grothendieck topology on C. Then a presheaf P is a sheaf for j iff P is a J-sheaf.

The concept of Grothendieck sheaf and Grothendieck sheafification already exists in (∞, 1)topos [HTT, Section 6.2.2]. It would be nice to check if theorem 7.1 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.

Nomenclature

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 [HoTT/Coq].