Quirin, Kevin, and Nicolas Tabareau. “Lawvere-Tierney Sheafification in Homotopy Type Theory”. Journal of Formalized Reasoning 9, no. 2 (January 1, 2016): 131–161. Accessed February 8, 2023. https://jfr.unibo.it/article/view/6232.