(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
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
type of h-sets
Created on September 11, 2012 at 23:09:57. See the history of this page for a list of all contributions to it.