Lawvere-Tierney sheafification in Homotopy Type Theory. - Kevin Quirin; Nicolas Tabareau (J. Formaliz. Reason., 2016)

Lawvere-Tierney sheafification in Homotopy Type Theory. (Faisceautisation de Lawvere-Tierney en théorie des types homotopiques). - Kevin Quirin (2016)