natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
= + +
/ | -/ | |
, | ||
of / of | ||
for | for hom-tensor adjunction | |
introduction rule for | for hom-tensor adjunction | |
( of) | ( of) | |
into | into | |
( of) | ( of) | |
, , | ||
higher | ||
/ | -// | |
/ | ||
, () | , | |
(, ) | / | |
(absence of) | (absence of) | |
Semantics is the interpretation of the syntax of a theory in a model.
See a separate page for semantics of a programming language.
Notably the semantics of type theories is given by categories. For instance
dependent type theory is precisely the formal language for which locally cartesian closed categories are the semantics,
intensional type theory is the formal language for which locally cartesian closed (infinity,1)-categories are the semantics;
homotopy type theory is the formal language for which elementary (infinity,1)-toposes are the semantics.
For more on this see at categorical semantics and at relation between type theory and category theory.
Last revised on November 27, 2018 at 22:46:10. See the history of this page for a list of all contributions to it.