Lawvere-Tierney sheafification in Homotopy Type Theory

Kevin Quirin 1 Nicolas Tabareau 1
1 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : Sheafification is a popular tool in topos theory which allows to extend the internal logic of a topos with new principles. One of its most famous applications is the possibility to transform a topos into a boolean topos using the dense topology, which corresponds in essence to Gödel's double negation translation. The same construction has not been developed in Martin-Löf type theory because of a mismatch between topos theory and type theory. This mismatch has been fixed recently by considering homotopy type theory, an extension of Martin-Löf type theory with new principles inspired by category theory and homotopy theory, and which corresponds closely to higher toposes. In this paper, we give a computer-checked construction of Lawvere-Tierney sheafification in homotopy type theory.
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), 〈10.6092/issn.1972-5787/6232〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger
Contributeur : Nicolas Tabareau <>
Soumis le : mercredi 1 février 2017 - 13:30:17
Dernière modification le : vendredi 22 juin 2018 - 09:34:25


Fichiers produits par l'(les) auteur(s)



Kevin Quirin, Nicolas Tabareau. Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), 〈10.6092/issn.1972-5787/6232〉. 〈hal-01451710〉



Consultations de la notice


Téléchargements de fichiers