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
)_
Last revised on November 21, 2011 at 16:50:41. See the history of this page for a list of all contributions to it.