QUIRIN, K.; TABAREAU, N. Lawvere-Tierney sheafification in Homotopy Type Theory. Journal of Formalized Reasoning, [S. l.], v. 9, n. 2, p. 131–161, 2016. DOI: 10.6092/issn.1972-5787/6232. Disponível em: https://jfr.unibo.it/article/view/6232. Acesso em: 8 feb. 2023.