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
basic constructions:
strong axioms
further
As a category has internal logic, so a (∞,1)-category has internal -logic
See
(∞,1)-type theory, (∞,1)-logic
Created on May 7, 2011 at 10:29:08. See the history of this page for a list of all contributions to it.