Combinatorial realizability models of type theory

被引：6

作者：

Hofstra, Pieter ^{[1
]}

Warren, Michael A. ^{[2
]}

机构：

[1] Univ Ottawa, Dept Math & Stat, Ottawa, ON K1N 6N5, Canada

[2] Inst Adv Study, Sch Math, Princeton, NJ 08540 USA

来源：

ANNALS OF PURE AND APPLIED LOGIC | 2013年 / 164卷 / 10期

基金：

加拿大自然科学与工程研究理事会;

关键词：

Realizability; Gluing; Logical relations; Homotopy type theory; Martin-Lof type theory; Groupoid semantics;

D O I：

10.1016/j.apal.2013.05.002

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

We introduce a new model construction for Martin-Lof 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. (c) 2013 Elsevier B.V. All rights reserved.

引用

页码：957 / 988

页数：32

共 8 条

[1] Awodey S., 2012, EPISTEMOLOGY VERSUS, P183, DOI [10.1007/978-94-007-4435-6_9., DOI 10.1007/978-94-007-4435-6_9, 10.1007/978-94-007-4435-69, DOI 10.1007/978-94-007-4435-69]
[2] Martin-Lof complexes
Awodey, Steve
Hofstra, Pieter
Warren, Michael A.
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2013, 164 (10) : 928 - 956
[3] Dybjer P., 1996, LECT NOTES COMPUT SC, V1158
[4] The identity type weak factorisation system
Gambino, Nicola
Garner, Richard
[J]. THEORETICAL COMPUTER SCIENCE, 2008, 409 (01) : 94 - 109
[5] Hofmann M., 1998, Twenty-five years of constructive type theory, Oxf. Logic Guides, V36, P83
[6] Hofmann Martin, 1997, Extensional Constructs in Intensional Type Theory, P13, DOI DOI 10.1007/978-1-4471-0963-1_2
[7] INTENSIONAL INTERPRETATIONS OF FUNCTIONALS OF FINITE TYPE I
TAIT, WW
[J]. JOURNAL OF SYMBOLIC LOGIC, 1967, 32 (02) : 198 - &
[8] Voevodsky V., 2010, Univalent Foundations Project, grant proposal application

← 1 →