pith. sign in

arxiv: 1205.5527 · v1 · pith:RW5UPZ52new · submitted 2012-05-24 · 🧮 math.LO · math.CT

Combinatorial realizability models of type theory

classification 🧮 math.LO math.CT
keywords modeltheorytypegroupoidgeneratedrealizabilitysyntacticanalyse
0
0 comments X
read the original abstract

We introduce a new model construction for Martin-L\"{o}f intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines the syntactic model with a notion of realizability; it also encompasses the well-known Hofmann- Streicher groupoid semantics. 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.