Navarro Garmendia, Alberto Vladimir Voevodsky, Fields Medal 2002. (Vladimir Voevodsky, Medalla Fields 2002.) (Spanish) Zbl 1485.01060 Gac. R. Soc. Mat. Esp. 24, No. 3, 623-643 (2021). MSC: 01A70 14C15 14F42 PDFBibTeX XMLCite \textit{A. Navarro Garmendia}, Gac. R. Soc. Mat. Esp. 24, No. 3, 623--643 (2021; Zbl 1485.01060) Full Text: Link Backlinks: MO
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael Construction of the circle in UniMath. (English) Zbl 07357172 J. Pure Appl. Algebra 225, No. 10, Article ID 106687, 21 p. (2021). MSC: 03B38 03B70 55U35 03G30 PDFBibTeX XMLCite \textit{M. Bezem} et al., J. Pure Appl. Algebra 225, No. 10, Article ID 106687, 21 p. (2021; Zbl 07357172) Full Text: DOI arXiv
Tsementzis, Dimitris A meaning explanation for HoTT. (English) Zbl 1475.03055 Synthese 197, No. 2, 651-680 (2020). MSC: 03A05 03B38 55U35 PDFBibTeX XMLCite \textit{D. Tsementzis}, Synthese 197, No. 2, 651--680 (2020; Zbl 1475.03055) Full Text: DOI Link
Bordg, Anthony Univalent foundations and the unimath library. (English) Zbl 1528.03104 Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 173-189 (2019). MSC: 03B38 03G30 18N45 55U35 68V35 PDFBibTeX XMLCite \textit{A. Bordg}, Synth. Libr. 407, 173--189 (2019; Zbl 1528.03104) Full Text: DOI arXiv
Buchholtz, Ulrik Higher structures in homotopy type theory. (English) Zbl 1528.03105 Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 151-172 (2019). MSC: 03B38 03G30 18N45 55U35 PDFBibTeX XMLCite \textit{U. Buchholtz}, Synth. Libr. 407, 151--172 (2019; Zbl 1528.03105) Full Text: DOI arXiv
van der Weide, Niels; Geuvers, Herman The construction of set-truncated higher inductive types. (English) Zbl 07515964 König, Barbara (ed.), Proceedings of the 35th conference on the mathematical foundations of programming semantics, MFPS XXXV, London, UK, June 4–7, 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 347, 261-280 (2019). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{N. van der Weide} and \textit{H. Geuvers}, Electron. Notes Theor. Comput. Sci. 347, 261--280 (2019; Zbl 07515964) Full Text: DOI
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders From signatures to monads in UniMath. (English) Zbl 1468.03007 J. Autom. Reasoning 63, No. 2, 285-318 (2019). MSC: 03B35 03B38 18C10 18C15 55U35 68V20 PDFBibTeX XMLCite \textit{B. Ahrens} et al., J. Autom. Reasoning 63, No. 2, 285--318 (2019; Zbl 1468.03007) Full Text: DOI arXiv
Kapulkin, Krzysztof; Szumiło, Karol Internal languages of finitely complete \((\infty , 1)\)-categories. (English) Zbl 1462.18007 Sel. Math., New Ser. 25, No. 2, Paper No. 33, 46 p. (2019). Reviewer: Julie Bergner (Riverside) MSC: 18N60 55U35 03B38 PDFBibTeX XMLCite \textit{K. Kapulkin} and \textit{K. Szumiło}, Sel. Math., New Ser. 25, No. 2, Paper No. 33, 46 p. (2019; Zbl 1462.18007) Full Text: DOI arXiv
Grayson, Daniel R. An introduction to univalent foundations for mathematicians. (English) Zbl 1461.03012 Bull. Am. Math. Soc., New Ser. 55, No. 4, 427-450 (2018). MSC: 03B38 03B35 03G30 18A15 55U35 PDFBibTeX XMLCite \textit{D. R. Grayson}, Bull. Am. Math. Soc., New Ser. 55, No. 4, 427--450 (2018; Zbl 1461.03012) Full Text: DOI arXiv
Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir Categorical structures for type theory in univalent foundations. (English) Zbl 1496.03053 Log. Methods Comput. Sci. 14, No. 3, Paper No. 18, 18 p. (2018). MSC: 03B38 03F50 18C50 03B70 55U40 68V15 PDFBibTeX XMLCite \textit{B. Ahrens} et al., Log. Methods Comput. Sci. 14, No. 3, Paper No. 18, 18 p. (2018; Zbl 1496.03053) Full Text: DOI arXiv
Angiuli, Carlo; Harper, Robert Meaning explanations at higher dimension. (English) Zbl 1436.03102 Indag. Math., New Ser. 29, No. 1, 135-149 (2018). MSC: 03B38 55U35 PDFBibTeX XMLCite \textit{C. Angiuli} and \textit{R. Harper}, Indag. Math., New Ser. 29, No. 1, 135--149 (2018; Zbl 1436.03102) Full Text: DOI
van Doorn, Floris; von Raumer, Jakob; Buchholtz, Ulrik Homotopy type theory in Lean. (English) Zbl 1484.68319 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 479-495 (2017). MSC: 68V20 03B35 03B38 03G30 55U40 PDFBibTeX XMLCite \textit{F. van Doorn} et al., Lect. Notes Comput. Sci. 10499, 479--495 (2017; Zbl 1484.68319) Full Text: DOI arXiv