A General Framework for the Semantics of Type Theory

Abstract

We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-Löf type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

References in corpus (1)

• The Universal Exponentiable Arrow

Cited by in corpus (4)

• Decalf: A Directed, Effectful Cost-Aware Logical Framework
• Internal parametricity, without an interval
• Comparing semantic frameworks for dependently-sorted algebraic theories
• Controlling unfolding in type theory