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

under construction

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

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

(…)

(…)

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

- Mike Shulman,
*ReflectiveSubcategory.v*)_

Last revised on November 21, 2011 at 16:50:41. See the history of this page for a list of all contributions to it.