nLab
reflective productpreserving sub(∞,1)category  internal formulation
Context
Notions of subcategory
$(\infty,1)$topos theory
(∞,1)topos theory
Background
Definitions

elementary (∞,1)topos

(∞,1)site

reflective sub(∞,1)category

(∞,1)category of (∞,1)sheaves

(∞,1)topos

(n,1)topos, ntopos

(∞,1)quasitopos

(∞,2)topos

(∞,n)topos
Characterization
Morphisms
Extra stuff, structure and property

hypercomplete (∞,1)topos

over(∞,1)topos

nlocalic (∞,1)topos

locally nconnected (n,1)topos

structured (∞,1)topos

locally ∞connected (∞,1)topos, ∞connected (∞,1)topos

local (∞,1)topos

cohesive (∞,1)topos
Models
Constructions
structures in a cohesive (∞,1)topos
Contents
Idea
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 productpreserving sub(∞,1)category.
References
HoTTCoq code for internal reflective subcategories is at
The fact that in the internal formulation reflective subcategories are automatically productpreserving is mentioned on p. 5 of
Revised on November 21, 2011 16:40:57
by
Urs Schreiber
(82.113.99.46)