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 mismatched 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.
@article{6232,
title = {Lawvere-Tierney sheafification in Homotopy Type Theory},
journal = {Journal of Formalized Reasoning},
volume = {9},
year = {2016},
doi = {10.6092/issn.1972-5787/6232},
language = {EN},
url = {http://dml.mathdoc.fr/item/6232}
}
Quirin, Kevin; Tabareau, Nicolas. Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, Tome 9 (2016) . doi : 10.6092/issn.1972-5787/6232. http://gdmltest.u-ga.fr/item/6232/