Bidlingmaier, Martin E.; Faissole, Florian; Spitters, Bas Synthetic topology in homotopy type theory for probabilistic programming. (English) Zbl 1517.68072 Math. Struct. Comput. Sci. 31, No. 10, 1301-1329 (2021). MSC: 68N19 03B38 03F60 06D22 18B25 18C20 18C50 18N45 28E15 55U35 68N30 68V20 PDFBibTeX XMLCite \textit{M. E. Bidlingmaier} et al., Math. Struct. Comput. Sci. 31, No. 10, 1301--1329 (2021; Zbl 1517.68072) Full Text: DOI arXiv
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
Booij, Auke B. Extensional constructive real analysis via locators. (English) Zbl 07408496 Math. Struct. Comput. Sci. 31, No. 1, 64-88 (2021). MSC: 03B38 03F60 PDFBibTeX XMLCite \textit{A. B. Booij}, Math. Struct. Comput. Sci. 31, No. 1, 64--88 (2021; Zbl 07408496) Full Text: DOI arXiv
Piceghello, Stefano Coherence for monoidal groupoids in HoTT. (English) Zbl 07756113 Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 8, 20 p. (2020). MSC: 03B70 68N30 PDFBibTeX XMLCite \textit{S. Piceghello}, LIPIcs -- Leibniz Int. Proc. Inform. 175, Article 8, 20 p. (2020; Zbl 07756113) Full Text: DOI
Ladyman, James; Presnell, Stuart Universes and univalence in homotopy type theory. (English) Zbl 07124569 Rev. Symb. Log. 12, No. 3, 426-455 (2019). MSC: 03A05 03B38 18N40 55U35 00A30 PDFBibTeX XMLCite \textit{J. Ladyman} and \textit{S. Presnell}, Rev. Symb. Log. 12, No. 3, 426--455 (2019; Zbl 07124569) Full Text: DOI
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
Angiuli, Carlo; Hou, (Favonia) Kuen-Bang; Harper, Robert Cartesian cubical computational type theory: constructive reasoning with paths and equalities. (English) Zbl 07533331 Ghica, Dan R. (ed.) et al., 27th EACSL annual conference on computer science logic, CSL 2018, Birmingham, United Kingdom, September 4–8, 2018. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 119, Article 6, 17 p. (2018). MSC: 03B70 PDFBibTeX XMLCite \textit{C. Angiuli} et al., LIPIcs -- Leibniz Int. Proc. Inform. 119, Article 6, 17 p. (2018; Zbl 07533331) Full Text: DOI
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
Shulman, Michael Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. (English) Zbl 1390.03014 Math. Struct. Comput. Sci. 28, No. 6, 856-941 (2018). Reviewer: Ittay Weiss (Portsmouth) MSC: 03B15 03G30 55U40 55M20 03B60 PDFBibTeX XMLCite \textit{M. Shulman}, Math. Struct. Comput. Sci. 28, No. 6, 856--941 (2018; Zbl 1390.03014) Full Text: DOI arXiv Backlinks: MO
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
Timany, Amin; Jacobs, Bart Category theory in Coq 8.5. (English) Zbl 1387.68208 Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 30, 18 p. (2016). MSC: 68T15 03B15 03G30 18A99 55U40 PDFBibTeX XMLCite \textit{A. Timany} and \textit{B. Jacobs}, LIPIcs -- Leibniz Int. Proc. Inform. 52, Article 30, 18 p. (2016; Zbl 1387.68208) Full Text: DOI arXiv
Shulman, Michael Idempotents in intensional type theory. (English) Zbl 1445.03011 Log. Methods Comput. Sci. 12, No. 3, Paper No. 9, 24 p. (2016). MSC: 03B38 03G30 18N60 55U40 PDFBibTeX XMLCite \textit{M. Shulman}, Log. Methods Comput. Sci. 12, No. 3, Paper No. 9, 24 p. (2016; Zbl 1445.03011) Full Text: DOI arXiv Backlinks: MO