Two-dimensional models of type theory

Richard Garner

arXiv:0808.2122·math.LO·October 17, 2011·Math. Struct. Comput. Sci.

Two-dimensional models of type theory

Richard Garner

PDF

TL;DR

This paper introduces a non-extensional two-dimensional variant of Martin-L"of type theory and provides a sound and complete semantics for it using 2-categories.

Contribution

It presents a novel two-dimensional type theory and develops a semantics framework based on 2-categories, expanding the theoretical foundations of type theory.

Findings

01

Established soundness and completeness of the semantics

02

Defined a non-extensional variant of Martin-L"of type theory

03

Provided a categorical semantics in 2-categories

Abstract

We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.