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 PDF BibTeX XML Cite \textit{M. Bezem} et al., J. Pure Appl. Algebra 225, No. 10, Article ID 106687, 21 p. (2021; Zbl 07357172) Full Text: DOI arXiv OpenURL
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 PDF BibTeX XML Cite \textit{D. R. Grayson}, Bull. Am. Math. Soc., New Ser. 55, No. 4, 427--450 (2018; Zbl 1461.03012) Full Text: DOI arXiv OpenURL
The Univalent Foundations Program [Aczel, Peter; Ahrens, Benedikt; Altenkirch, Thorsten; Awodey, Steve; Barras, Bruno; Bauer, Andrej; Bertot, Yves; Bezem, Marc; Coquand, Thierry; Finster, Eric; Grayson, Daniel; Herbelin, Hugo; Joyal, Andre; Licata, Dan; Lumsdaine, Peter; Mahboubi, Assia; Martin-Lof, Per; Melikhov, Sergey; Pelayo, Alvaro; Polonsky, Andrew; Shulman, Michael; Sozeau, Matthieu; Spitters, Bas; van den Berg, Benno; Voevodsky, Vladimir; Warren, Michael; Zeilberger, Noam; Angiuli, Carlo; Bordg, Anthony; Brunerie, Guillaume; Kapulkin, Chris; Rijke, Egbert; Sojakova, Kristina; Avigad, Jeremy; Cohen, Cyril; Constable, Robert; Curien, Pierre-Louis; Dybjer, Peter; Escardo, Martín; Hou, Kuen-Bang; Gambino, Nicola; Garner, Richard; Gonthier, Georges; Hales, Thomas; Harper, Robert; Hofmann, Martin; Hofstra, Pieter; Kock, Joachim; Kraus, Nicolai; Li, Nuo; Luo, Zhaohui; Nahas, Michael; Palmgren, Erik; Riehl, Emily; Scott, Dana; Scott, Philip; Soloviev, Sergei] Homotopy type theory. Univalent foundations of mathematics. (English) Zbl 1298.03002 Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press. ix, 468 p. (2013). Reviewer: Marco Benini (Buccinasco) MSC: 03-02 55-02 03B15 03G30 18A15 18B05 55U40 PDF BibTeX XML Cite \textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002) Full Text: arXiv Link OpenURL
Jones, Kevin Charles; Kim, Youngsoo; Mhoon, Andrea H.; Santhanam, Rekha; Walker, Barry J.; Grayson, Daniel R. The additivity theorem in \(K\)-theory. (English) Zbl 1077.19001 \(K\)-Theory 32, No. 2, 181-191 (2004). Reviewer: Antonio R. Garzón (Granada) MSC: 19D06 55U10 PDF BibTeX XML Cite \textit{K. C. Jones} et al., \(K\)-Theory 32, No. 2, 181--191 (2004; Zbl 1077.19001) Full Text: DOI OpenURL
Gillet, Henri; Grayson, Daniel R. The loop space of the Q-construction. (English) Zbl 0628.55011 Ill. J. Math. 31, 574-597 (1987); erratum ibid. 47, No. 3, 745-748 (2003). Reviewer: M.Stein MSC: 55U35 55U10 18F25 55P35 PDF BibTeX XML Cite \textit{H. Gillet} and \textit{D. R. Grayson}, Ill. J. Math. 31, 574--597 (1987; Zbl 0628.55011) OpenURL