- Thierry Coquand, Fabian Ruch, Christian Sattler, “Constructive sheaf models of type theory”, Math. Struct. Comp. Sci., 31, № 9, 2021, 979
- Thierry Coquand, 10304, Computer Science – Theory and Applications, 2017, 1
- M. A. Guzev, Yu. N. Zhuravlev, “To the Justification of the Effectiveness of Future Mathematics in the New Biology”, Russ. J. Math. Phys., 29, № 4, 2022, 500
- Daniel Grayson, “An introduction to univalent foundations for mathematicians”, Bull. Amer. Math. Soc., 55, № 4, 2018, 427
- Simona Paoli, 26, Simplicial Methods for Higher Categories, 2019, 3
- Thierry Coquand, “A survey of constructive presheaf models of univalence”, ACM SIGLOG News, 5, № 3, 2018, 54
- Thierry Coquand, “Combinatorial topology and constructive mathematics”, Indagationes Mathematicae, 29, № 6, 2018, 1637
- ANDREA VEZZOSI, ANDERS MÖRTBERG, ANDREAS ABEL, “Cubical Agda: A dependently typed programming language with univalence and higher inductive types”, J. Funct. Prog., 31, 2021, e8
- Nicola Gambino, Simon Henry, “Towards a constructive simplicial model of Univalent Foundations”, Journal of London Math Soc, 105, № 2, 2022, 1073
- Nicola Gambino, Christian Sattler, Karol Szumiło, “The Constructive Kan–Quillen Model Structure: Two New Proofs”, The Quarterly Journal of Mathematics, 73, № 4, 2022, 1307