(2,1)-quasitopos?
structures in a cohesive (∞,1)-topos
rational homotopy?
The external definition of reflective sub-(∞,1)-category via the universal property of the reflector has an immediate formulation in the internal language of an (∞,1)-topos. This internal formulation, however, automatically gives a reflective product-preserving sub-(∞,1)-category.
HoTT-Coq code for internal reflective subcategories is at
The fact that in the internal formulation reflective subcategories are automatically product-preserving is mentioned on p. 5 of
Last revised on November 21, 2011 at 16:40:57. See the history of this page for a list of all contributions to it.