Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas Cubical Agda: a dependently typed programming language with univalence and higher inductive types. (English) Zbl 1512.68058 J. Funct. Program. 31, Paper No. e8, 47 p. (2021). MSC: 68N18 55U35 PDFBibTeX XMLCite \textit{A. Vezzosi} et al., J. Funct. Program. 31, Paper No. e8, 47 p. (2021; Zbl 1512.68058) Full Text: DOI
Carranza, Daniel; Chang, Jonathan; Kapulkin, Chris; Sandford, Ryan 2-adjoint equivalences in homotopy type theory. (English) Zbl 1509.03051 Log. Methods Comput. Sci. 17, No. 1, Paper No. 3, 9 p. (2021). MSC: 03B38 55U35 03B35 68V20 PDFBibTeX XMLCite \textit{D. Carranza} et al., Log. Methods Comput. Sci. 17, No. 1, Paper No. 3, 9 p. (2021; Zbl 1509.03051) Full Text: arXiv Link
van den Berg, Benno Univalent polymorphism. (English) Zbl 1440.18048 Ann. Pure Appl. Logic 171, No. 6, Article ID 102793, 29 p. (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 03F50 03G30 18C50 55U35 68Q55 PDFBibTeX XMLCite \textit{B. van den Berg}, Ann. Pure Appl. Logic 171, No. 6, Article ID 102793, 29 p. (2020; Zbl 1440.18048) Full Text: DOI arXiv
Buchholtz, Ulrik; van Doorn, Floris; Rijke, Egbert Higher groups in homotopy type theory. (English) Zbl 1452.03034 Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 205-214 (2018). MSC: 03B38 55U35 PDFBibTeX XMLCite \textit{U. Buchholtz} et al., in: Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9--12, 2018. New York, NY: Association for Computing Machinery (ACM). 205--214 (2018; Zbl 1452.03034) Full Text: DOI arXiv
Buchholtz, Ulrik; Rijke, Egbert The Cayley-Dickson construction in homotopy type theory. (English) Zbl 1522.03039 High. Struct. 2, No. 1, 30-41 (2018). MSC: 03B38 18N40 18N45 55U35 PDFBibTeX XMLCite \textit{U. Buchholtz} and \textit{E. Rijke}, High. Struct. 2, No. 1, 30--41 (2018; Zbl 1522.03039) Full Text: arXiv Backlinks: MO
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
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
Cockx, Jesper; Devriese, Dominique; Piessens, Frank Eliminating dependent pattern matching without K. (English) Zbl 1419.68037 J. Funct. Program. 26, Paper No. e16, 40 p. (2016). MSC: 68N18 03B15 03G30 55U40 PDFBibTeX XMLCite \textit{J. Cockx} et al., J. Funct. Program. 26, Paper No. e16, 40 p. (2016; Zbl 1419.68037) Full Text: DOI