Quirin, K., & Tabareau, N. (2016). Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, 9(2), 131–161. https://doi.org/10.6092/issn.1972-5787/6232