恒等类型的同伦论模型
逻辑
2009-11-13 v1 代数拓扑
范畴论
摘要
本文提出了同伦代数与数理逻辑之间的一种新颖联系。研究表明,一种形式的内涵类型论在任何 Quillen 模型范畴中均有效,从而推广了 Martin-Löf 类型论的 Hofmann-Streicher 群胚模型。
引用
@article{arxiv.0709.0248,
title = {Homotopy theoretic models of identity types},
author = {Steve Awodey and Michael A. Warren},
journal= {arXiv preprint arXiv:0709.0248},
year = {2009}
}
评论
11 pages