Quirin, K.; Tabareau, N. Lawvere-Tierney Sheafification in Homotopy Type Theory. JFR 2016, 9, 131-161.