同伦型优雅模型的单值宇宙
代数拓扑
2014-06-03 v1 范畴论
逻辑
摘要
我们在某些适用于同伦型的模型范畴(源自 Grothendieck 的测试范畴理论)中,构建了 Voevodsky 意义上的单值宇宙。实际上,这意味着除了单纯集的同伦论之外,带有单值公理的内涵类型论也可以在立方集(无论是否带有连接)的同伦论或 Joyal 的细胞集的同伦论中进行解释。
引用
@article{arxiv.1406.0058,
title = {Univalent universes for elegant models of homotopy types},
author = {Denis-Charles Cisinski},
journal= {arXiv preprint arXiv:1406.0058},
year = {2014}
}