On the interpretation of type theory in locally cartesian closed categories
| Author(s) : | Martin Hofmann, |
| Publisher : | N/A |
| Publication Date : | 1994 |
| ISSN : | N/A |
| Abstract : | Abstract. We show how to construct a model of dependent type theory (category with attributes) from a locally cartesian closed category (lccc). This allows to define a semantic function interpreting the syntax of type theory in an lccc. We sketch an application which gives rise to an interpretation of extensional type theory in intensional type theory. 1, |