David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 48 (3):299 - 317 (1989)
In the paper there are introduced and discussed the concepts of an indexed category with quantifications and a higher level indexed category to present an algebraic characterization of some version of Martin-Löf Type Theory. This characterization is given by specifying an additional equational structure of those indexed categories which are models of Martin-Löf Type Theory. One can consider the presented characterization as an essentially algebraic theory of categorical models of Martin-Löf Type Theory. The paper contains a construction of an indexed category with quantifications from terms and types of the language of Martin-Löf Type Theory given in the manner of Troelstra . The paper contains also an inductive definition of a valuation of these terms and types in an indexed category with quantifications.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
M. Beeson (1982). Recursive Models for Constructive Set Theories. Annals of Mathematical Logic 23 (2-3):127-178.
John Cartmell (1986). Generalised Algebraic Theories and Contextual Categories. Annals of Pure and Applied Logic 32 (3):209-243.
Citations of this work BETA
No citations found.
Similar books and articles
S. Awodey & M. A. Warren (2013). Martin-Löf Complexes. Annals of Pure and Applied Logic 164 (10):928-956.
Jan Smith (1984). An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions. Journal of Symbolic Logic 49 (3):730-753.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Ingrid Lindström (1989). A Construction of Non-Well-Founded Sets Within Martin-Löf's Type Theory. Journal of Symbolic Logic 54 (1):57-64.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
Erik Palmgren (1991). A Construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe. Journal of Symbolic Logic 56 (3):1012-1015.
Andrew M. Pitts & Paul Taylor (1989). A Note on Russell's Paradox in Locally Cartesian Closed Categories. Studia Logica 48 (3):377 - 387.
Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65 (2):525-549.
Added to index2009-01-28
Total downloads13 ( #136,707 of 1,410,151 )
Recent downloads (6 months)1 ( #177,743 of 1,410,151 )
How can I increase my downloads?