Lawvere-Tierney sheafification in Homotopy Type Theory / Kevin Quirin ; sous la direction de Nicolas Tabareau

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : anglais / English

Coq -- logiciel

Théorie des types

Homotopie

Tabareau, Nicolas (1982-....) (Directeur de thèse / thesis advisor)

Cointe, Pierre (1954-....) (Président du jury de soutenance / praeses)

Sozeau, Matthieu (1982-....) (Rapporteur de la thèse / thesis reporter)

Escardó, Martín Hötzel (19..-....) (Rapporteur de la thèse / thesis reporter)

Spitters, Bas (Membre du jury / opponent)

École nationale supérieure des mines (Nantes ; 1990-2016) (Organisme de soutenance / degree-grantor)

École doctorale Sciences et technologies de l'information et mathématiques (Nantes) (Ecole doctorale associée à la thèse / doctoral school)

ASCOLA. ASpect and COmposition LAnguages (Laboratoire associé à la thèse / thesis associated laboratory)

Laboratoire d’Informatique de Nantes Atlantique (UMR 6241) (Nantes) (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Le but principal de cette thèse est de définir une extension de la traduction de double-négation de Gödel à tous les types tronqués, dans le contexte de la théorie des types homotopique. Ce but utilisera des théories déjà existantes, comme la théorie des faisceaux de Lawvere-Tierney, quenous 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]

Résumé / 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]