No CrossRef data available.
Article contents
Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
Published online by Cambridge University Press: 04 March 2009
Abstract
We establish functional completeness of Locally Cartesian Closed Categories by axiomatising the theory of LCCC's in a constructive style. As a consequence we show that there is essentially only one interpretation of Martin-Löf's theory of types with extensional equality in the theory of LCCC's.
- Type
- Research Article
- Information
- Copyright
- Copyright © Cambridge University Press 1996