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