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
As a category has an internal logic so a 2-category has internal 2-logic
2-type theory, 2-logic
Last revised on May 7, 2011 at 23:10:51. See the history of this page for a list of all contributions to it.