类型论的组合可实现性模型
逻辑
2012-05-25 v1 范畴论
摘要
我们引入了一种新的 Martin-Löf 内涵类型论的模型构造，该模型对于该理论的 1-截断版本是可靠且完备的。该模型在形式上将语法模型与可实现性概念相结合；它也涵盖了著名的 Hofmann-Streicher 群胚语义。作为我们的主要应用，我们使用该模型来分析由图 G 生成的类型论所关联的语法群胚，表明其与由 G 生成的自由群胚具有相同的同伦类型。
关键词
引用
@article{arxiv.1205.5527,
title = {Combinatorial realizability models of type theory},
author = {Pieter Hofstra and Michael A. Warren},
journal= {arXiv preprint arXiv:1205.5527},
year = {2012}
}
备注
38 pages