# nLab reflective sub-(infinity,1)-category - internal formulation

under construction

# Contents

## Idea

The following gives a characterization of reflective sub-(∞,1)-categories of an (∞,1)-topos entirely in terms of its internal logic/homotopy type theory.

(…)

(…)

## References

Coq-code for lex reflective subcategories in homotopy type theory is at

Revised on November 21, 2011 16:50:41 by Urs Schreiber (82.113.99.46)