Quirin, Kevin, and Nicolas Tabareau. 2016. “Lawvere-Tierney Sheafification in Homotopy Type Theory”. Journal of Formalized Reasoning 9 (2):131-61. https://doi.org/10.6092/issn.1972-5787/6232.