Combinatorial realizability models of type theory

Annals of Pure and Applied Logic 164 (10):957-988 (2013)
  Copy   BIBTEX

Abstract

We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type as the free groupoid generated by G

Links

PhilArchive



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

External links

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

Through your library

Similar books and articles

A liberal conception of multiple realizability.Eric Funkhouser - 2007 - Philosophical Studies 132 (3):467-494.
A general notion of realizability.Lars Birkedal - 2002 - Bulletin of Symbolic Logic 8 (2):266-282.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
A brief introduction to algebraic set theory.Steve Awodey - 2008 - Bulletin of Symbolic Logic 14 (3):281-298.
Sheaf toposes for realizability.Steven Awodey & Andrej Bauer - 2008 - Archive for Mathematical Logic 47 (5):465-478.
European Functionalism.Sven Rosenkranz - 2011 - Australasian Journal of Philosophy 89 (2):229 - 249.
Intensional models for the theory of types.Reinhard Muskens - 2007 - Journal of Symbolic Logic 72 (1):98-118.
Transplendent Models: Expansions Omitting a Type.Fredrik Engström & Richard W. Kaye - 2012 - Notre Dame Journal of Formal Logic 53 (3):413-428.
The Theory of $\kappa$ -like Models of Arithmetic.Richard Kaye - 1995 - Notre Dame Journal of Formal Logic 36 (4):547-559.
Multiple realizability.Eric Funkhouser - 2007 - Philosophy Compass 2 (2):303–315.

Analytics

Added to PP
2013-12-12

Downloads
45 (#339,015)

6 months
3 (#928,914)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Maddy On The Multiverse.Claudio Ternullo - 2019 - In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Berlin: Springer Verlag. pp. 43-78.
Martin-Löf complexes.S. Awodey & M. A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):928-956.
Models of HoTT and the Constructive View of Theories.Andrei Rodin - 2019 - In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Springer Verlag.

Add more citations

References found in this work

Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Martin-Löf complexes.S. Awodey & M. A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):928-956.

Add more references