nLab semantics

Semantics

Context

Type theory

= + +

/-/
,
of / of
introduction rule for for hom-tensor adjunction
( of) ( of)
into into
( of) ( of)
, ,
higher
/-//
/
, () ,
(, ) /
(absence of) (absence of)

homotopy levels

semantics

Semantics

Idea

Semantics is the interpretation of the syntax of a theory in a model.

See a separate page for semantics of a programming language.

Examples

Categorical semantics of dependent type theory

Notably the semantics of type theories is given by categories. For instance

For more on this see at categorical semantics and at relation between type theory and category theory.

category: logic

Last revised on November 27, 2018 at 22:46:10. See the history of this page for a list of all contributions to it.