# 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 at 10:25:39. See the history of this page for a list of all contributions to it.