Contents

Idea

As type theory has categorical semantics in 1-categories, 2-type theory has semantics in 2-categories.

References

2-categorical type theory is discussed in chapter 7 of

• Daniel Licata, Dependently Typed Programming with Domain-Specific Logics PhD Thesis (2011) (pdf)

A more encompassing discussion of 2-categorical logic is being developed at

Created on May 7, 2011 10:25:39 by Urs Schreiber (89.204.137.104)