[007E] 参考文献

[Church--1940-0000] 文献

Alonzo Church. A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, 5(2):56--68, 1940. https://doi.org/10.2307/2266170

[Hedberg--1998-0000] 文献

Michael Hedberg. A coherence theorem for Martin-Löf's type theory. Journal of Functional Programming, 8(4):413--436, 1998-07. https://doi.org/10.1017/S0956796898003153

[HoTT-Book] 文献

The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. http://homotopytypetheory.org/book/

[Hovey--1999-0000] 文献

Mark Hovey. Model categories. American Mathematical Society, 1999.

[Kapulkin--Lumsdaine--2021-0000] 文献

Krzysztof Kapulkin & Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). Journal of the European Mathematical Society (JEMS), 23(6):2071--2126, 2021. https://doi.org/10.4171/JEMS/1050 https://arxiv.org/abs/1211.2851v5

[Lambek--Scott--1986-0000] 文献

J. Lambek & P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, 1986.

[Lumsdaine--2010-0000] 文献

Peter LeFanu Lumsdaine. Weak ω-categories from intensional type theory. Logical Methods in Computer Science, 6(3), 2010-09-17. https://doi.org/10.2168/lmcs-6(3:24)2010 https://arxiv.org/abs/0812.0409v4

[Lurie--2009-0000] 文献

Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009. https://www.math.ias.edu/~lurie/papers/HTT.pdf

[Martin-Loef--1975-0000] 文献

Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. Studies in Logic and the Foundations of Mathematics, 80:73--118, 1975. https://doi.org/10.1016/S0049-237X(08)71945-1

[Pierce--2002-0000] 文献

Benjamin C. Pierce. Types and programming languages. MIT Press, 2002.

[Quillen--1967-0000] 文献

Daniel G. Quillen. Homotopical algebra. Springer, 1967. https://doi.org/doi:10.1007/BFb0097438

[Russell--1908-0000] 文献

Bertrand Russell. Mathematical Logic as Based on the Theory of Types. American Journal of Mathematics, 30(3):222--262, 1908. https://doi.org/10.2307/2369948

[Streicher--1993-0000] 文献

Thomas Streicher. Investigations into Intensional Type Theory. Habilitation Thesis, Ludwig-Maximilians-Universität München, 1993. https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf

[van-den-Berg--Garner--2011-0000] 文献

Benno van den Berg & Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370--394, 2011. https://doi.org/10.1112/plms/pdq026 https://arxiv.org/abs/0812.0298v2