Lawvere-Tierney sheafification in Homotopy Type Theory
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 negatio...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2016-12-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | https://jfr.unibo.it/article/view/6232 |