K. Quirin and N. Tabareau, “Lawvere-Tierney sheafification in Homotopy Type Theory”, JFR, vol. 9, no. 2, pp. 131–161, Jan. 2016.