Modeling Martin-Löf type theory in categories

Journal of Applied Logic 12 (1):28-44 (2014)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/j.jal.2013.08.003

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,592

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Higher type categories.Martin Dowd - 1993 - Mathematical Logic Quarterly 39 (1):251-254.
Homotopy theoretic models of identity types.Steve Awodey & Michael A. Warren - unknown
Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
An interpretation of Martin-löf's type theory in a type-free theory of propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.
An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):446-448.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Propositions as [Types].Steve Awodey & Andrej Bauer - unknown
Martin-Löf complexes.S. Awodey & M. A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):928-956.
A note on Russell's paradox in locally cartesian closed categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.
Adding Sentence Types to a Model of Syntactic Category Acquisition.Stella Frank, Sharon Goldwater & Frank Keller - 2013 - Topics in Cognitive Science 5 (3):495-521.
The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
The strength of Martin-Löf type theory with a superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
Induction–recursion and initial algebras.Peter Dybjer & Anton Setzer - 2003 - Annals of Pure and Applied Logic 124 (1-3):1-47.

Analytics

Added to PP
2016-06-30

Downloads
9 (#1,246,467)

6 months
6 (#509,139)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Categorical Logic and Type Theory.R. A. G. Seely - 2000 - Bulletin of Symbolic Logic 6 (2):225-229.

Add more references