命题即其证明的（同伦）类型
逻辑
2023-03-31 v1 范畴论
摘要
为致敬 W.W. Tait 而对同伦类型理论所作的介绍与综述。
引用
@article{arxiv.1701.02024,
title = {A proposition is the (homotopy) type of its proofs},
author = {Steve Awodey},
journal= {arXiv preprint arXiv:1701.02024},
year = {2023}
}