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 (7)

• Two-Level Type Theory and Applications
• Internal Universes in Models of Homotopy Type Theory
• Modal Dependent Type Theory and Dependent Right Adjoints
• The homotopy theory of type theories
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• A construction of certain weak colimits and an exactness property of the 2-category of categories
• 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