A General Framework for the Semantics of Type Theory
Category Theory
2023-08-10 v3 Logic in Computer Science
Logic
Abstract
We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-L\"{o}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.
Keywords
Cite
@article{arxiv.1904.04097,
title = {A General Framework for the Semantics of Type Theory},
author = {Taichi Uemura},
journal= {arXiv preprint arXiv:1904.04097},
year = {2023}
}