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
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