nLab
reflective product-preserving sub-(∞,1)-category - internal formulation

Context

Notions of subcategory

(,1)(\infty,1)-topos theory

(∞,1)-topos theory

Background

Definitions

Characterization

Morphisms

Extra stuff, structure and property

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 product-preserving sub-(∞,1)-category.

References

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

Revised on November 21, 2011 16:40:57 by Urs Schreiber (82.113.99.46)