Riehl, Emily On the \(\infty\)-topos semantics of homotopy type theory. (English) Zbl 07813470 Bull. Lond. Math. Soc. 56, No. 2, 461-517 (2024). MSC: 18N40 18N45 18N60 03B38 55U10 55U40 PDFBibTeX XMLCite \textit{E. Riehl}, Bull. Lond. Math. Soc. 56, No. 2, 461--517 (2024; Zbl 07813470) Full Text: DOI arXiv
Weinberger, Jonathan Generalized Chevalley criteria in simplicial homotopy type theory. arXiv:2403.08190 Preprint, arXiv:2403.08190 [math.CT] (2024). MSC: 03B38 18N50 18N60 18N45 55U35 18D30 BibTeX Cite \textit{J. Weinberger}, ``Generalized Chevalley criteria in simplicial homotopy type theory'', Preprint, arXiv:2403.08190 [math.CT] (2024) Full Text: arXiv OA License
Cagne, Pierre; Buchholtz, Ulrik; Kraus, Nicolai; Bezem, Marc On symmetries of spheres in univalent foundations. arXiv:2401.15037 Preprint, arXiv:2401.15037 [cs.LO] (2024). MSC: 55P10 55U40 03B38 BibTeX Cite \textit{P. Cagne} et al., ``On symmetries of spheres in univalent foundations'', Preprint, arXiv:2401.15037 [cs.LO] (2024) Full Text: arXiv OA License
Corson, Samuel M. The Griffiths double cone group is isomorphic to the triple. (English) Zbl 07818424 Pac. J. Math. 327, No. 2, 297-336 (2023). MSC: 03E75 20A15 55Q52 20F10 20F34 PDFBibTeX XMLCite \textit{S. M. Corson}, Pac. J. Math. 327, No. 2, 297--336 (2023; Zbl 07818424) Full Text: DOI arXiv
Martínez-Rivillas, Daniel O.; de Queiroz, Ruy J. G. B. The theory of an arbitrary higher \(\lambda\)-model. (English) Zbl 07811407 Bull. Sect. Log., Univ. Łódź, Dep. Log. 52, No. 1, 39-58 (2023). MSC: 03B70 PDFBibTeX XMLCite \textit{D. O. Martínez-Rivillas} and \textit{R. J. G. B. de Queiroz}, Bull. Sect. Log., Univ. Łódź, Dep. Log. 52, No. 1, 39--58 (2023; Zbl 07811407) Full Text: DOI arXiv
Buchholtz, Ulrik; Weinberger, Jonathan Synthetic fibered \((\infty,1)\)-category theory. (English) Zbl 07806740 High. Struct. 7, No. 1, 74-165 (2023). MSC: 18N60 18N45 18D30 18N55 55U35 18N50 18D40 18D70 03B38 PDFBibTeX XMLCite \textit{U. Buchholtz} and \textit{J. Weinberger}, High. Struct. 7, No. 1, 74--165 (2023; Zbl 07806740) Full Text: arXiv Link
Casacuberta, Carles Cohomological localizations and set-theoretical reflection. (English) Zbl 07773756 Morel, Jean-Michel (ed.) et al., Mathematics going forward. Collected mathematical brushstrokes. Cham: Springer. Lect. Notes Math. 2313, 167-181 (2023). MSC: 55P60 03E55 55N20 18A40 57Q05 PDFBibTeX XMLCite \textit{C. Casacuberta}, Lect. Notes Math. 2313, 167--181 (2023; Zbl 07773756) Full Text: DOI
Wärn, David Eilenberg-MacLane spaces and stabilisation in homotopy type theory. (English) Zbl 07752396 J. Homotopy Relat. Struct. 18, No. 2-3, 357-368 (2023). MSC: 03Bxx 55P35 PDFBibTeX XMLCite \textit{D. Wärn}, J. Homotopy Relat. Struct. 18, No. 2--3, 357--368 (2023; Zbl 07752396) Full Text: DOI arXiv OA License
Manin, Fedor Rational homotopy type and computability. (English) Zbl 07749826 Found. Comput. Math. 23, No. 5, 1817-1849 (2023). Reviewer: Samuel Smith (Philadelphia) MSC: 55Q05 55-08 03D35 55P62 PDFBibTeX XMLCite \textit{F. Manin}, Found. Comput. Math. 23, No. 5, 1817--1849 (2023; Zbl 07749826) Full Text: DOI arXiv
de Jong, Tom; Hötzel Escardó, Martín On small types in univalent foundations. (English) Zbl 07731919 Log. Methods Comput. Sci. 19, No. 2, Paper No. 8, 33 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{T. de Jong} and \textit{M. Hötzel Escardó}, Log. Methods Comput. Sci. 19, No. 2, Paper No. 8, 33 p. (2023; Zbl 07731919) Full Text: DOI arXiv
Christensen, J. Daniel; Scoccola, Luis The Hurewicz theorem in homotopy type theory. (English) Zbl 07723339 Algebr. Geom. Topol. 23, No. 5, 2107-2140 (2023). MSC: 18-XX 55Q99 03B38 18N60 55N99 PDFBibTeX XMLCite \textit{J. D. Christensen} and \textit{L. Scoccola}, Algebr. Geom. Topol. 23, No. 5, 2107--2140 (2023; Zbl 07723339) Full Text: DOI arXiv
Bannister, Nathaniel; Bergfalk, Jeffrey; Moore, Justin Tatch On the additivity of strong homology for locally compact separable metric spaces. (English) Zbl 07720424 Isr. J. Math. 255, No. 1, 349-381 (2023). MSC: 03Exx 55Nxx 55Pxx PDFBibTeX XMLCite \textit{N. Bannister} et al., Isr. J. Math. 255, No. 1, 349--381 (2023; Zbl 07720424) Full Text: DOI arXiv
Lieberman, Michael; Rosický, Jiří; Vasey, Sebastien Cellular categories and stable independence. (English) Zbl 1514.18006 J. Symb. Log. 88, No. 2, 811-834 (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18C35 03C45 03C48 03C52 03C55 16B50 55U35 PDFBibTeX XMLCite \textit{M. Lieberman} et al., J. Symb. Log. 88, No. 2, 811--834 (2023; Zbl 1514.18006) Full Text: DOI arXiv
Frey, Jonas; Rasekh, Nima Constructing coproducts in locally Cartesian closed \(\infty\)-categories. (English) Zbl 1510.18002 Homology Homotopy Appl. 25, No. 1, 71-86 (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18B25 03G30 PDFBibTeX XMLCite \textit{J. Frey} and \textit{N. Rasekh}, Homology Homotopy Appl. 25, No. 1, 71--86 (2023; Zbl 1510.18002) Full Text: DOI arXiv
Kraus, Nicolai; Nordvall Forsberg, Fredrik; Xu, Chuangjie Type-theoretic approaches to ordinals. (English) Zbl 07679991 Theor. Comput. Sci. 957, Article ID 113843, 34 p. (2023). MSC: 03-XX PDFBibTeX XMLCite \textit{N. Kraus} et al., Theor. Comput. Sci. 957, Article ID 113843, 34 p. (2023; Zbl 07679991) Full Text: DOI arXiv
Frey, Jonas Categories of partial equivalence relations as localizations. (English) Zbl 1514.18004 J. Pure Appl. Algebra 227, No. 8, Article ID 107115, 25 p. (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18B25 55P99 03G30 PDFBibTeX XMLCite \textit{J. Frey}, J. Pure Appl. Algebra 227, No. 8, Article ID 107115, 25 p. (2023; Zbl 1514.18004) Full Text: DOI arXiv
Farah, Ilijas; Vignati, Alessandro Obstructions to countable saturation in corona algebras. (English) Zbl 07640186 Proc. Am. Math. Soc. 151, No. 3, 1285-1300 (2023). MSC: 03C66 03C50 46L05 PDFBibTeX XMLCite \textit{I. Farah} and \textit{A. Vignati}, Proc. Am. Math. Soc. 151, No. 3, 1285--1300 (2023; Zbl 07640186) Full Text: DOI arXiv
Kraus, Nicolai; von Raumer, Jakob A rewriting coherence theorem with applications in homotopy type theory. (English) Zbl 1509.03052 Math. Struct. Comput. Sci. 32, No. 7, 982-1014 (2022). MSC: 03B38 55U35 68Q42 PDFBibTeX XMLCite \textit{N. Kraus} and \textit{J. von Raumer}, Math. Struct. Comput. Sci. 32, No. 7, 982--1014 (2022; Zbl 1509.03052) Full Text: DOI arXiv
Myers, David Jaz Good fibrations through the modal prism. (English) Zbl 1502.18047 High. Struct. 6, No. 1, 212-255 (2022). Reviewer: Daniel Graves (Leeds) MSC: 18N45 03B38 55U35 PDFBibTeX XMLCite \textit{D. J. Myers}, High. Struct. 6, No. 1, 212--255 (2022; Zbl 1502.18047) Full Text: arXiv Link
Martínez-Rivillas, Daniel O.; de Queiroz, Ruy J. G. B. \(\infty\)-groupoid generated by an arbitrary topological \(\lambda\)-model. (English) Zbl 1494.03033 Log. J. IGPL 30, No. 3, 465-488 (2022). MSC: 03B40 06B35 55P99 PDFBibTeX XMLCite \textit{D. O. Martínez-Rivillas} and \textit{R. J. G. B. de Queiroz}, Log. J. IGPL 30, No. 3, 465--488 (2022; Zbl 1494.03033) Full Text: DOI arXiv
Barbieri-Viale, Luca On topological motives. (English) Zbl 1498.14048 Topology Appl. 314, Article ID 108141, 23 p. (2022). MSC: 14F42 03C60 55N35 18G80 PDFBibTeX XMLCite \textit{L. Barbieri-Viale}, Topology Appl. 314, Article ID 108141, 23 p. (2022; Zbl 1498.14048) Full Text: DOI arXiv
Coquand, Thierry; Huber, Simon; Sattler, Christian Canonicity and homotopy canonicity for cubical type theory. (English) Zbl 1486.03027 Log. Methods Comput. Sci. 18, No. 1, Paper No. 28, 35 p. (2022). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 03B38 03G30 55U35 PDFBibTeX XMLCite \textit{T. Coquand} et al., Log. Methods Comput. Sci. 18, No. 1, Paper No. 28, 35 p. (2022; Zbl 1486.03027) Full Text: arXiv Link
Swan, Andrew W. On the Nielsen-Schreier theorem in homotopy type theory. (English) Zbl 07471707 Log. Methods Comput. Sci. 18, No. 1, Paper No. 18, 15 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{A. W. Swan}, Log. Methods Comput. Sci. 18, No. 1, Paper No. 18, 15 p. (2022; Zbl 07471707) Full Text: arXiv Link
Christensen, J. Daniel; Rijke, Egbert Characterizations of modalities and lex modalities. (English) Zbl 1482.18015 J. Pure Appl. Algebra 226, No. 3, Article ID 106848, 21 p. (2022). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N55 03B38 03B45 03G30 18N60 55P60 PDFBibTeX XMLCite \textit{J. D. Christensen} and \textit{E. Rijke}, J. Pure Appl. Algebra 226, No. 3, Article ID 106848, 21 p. (2022; Zbl 1482.18015) Full Text: DOI arXiv
Bergfalk, Jeffrey; Lupini, Martino; Panagiotopoulos, Aristotelis The definable content of homological invariants II: Čech cohomology and homotopy classification. arXiv:2210.11098 Preprint, arXiv:2210.11098 [math.LO] (2022). MSC: 55P15 03E15 18G99 55N99 54D45 55P99 BibTeX Cite \textit{J. Bergfalk} et al., ``The definable content of homological invariants II: \v{C}ech cohomology and homotopy classification'', Preprint, arXiv:2210.11098 [math.LO] (2022) Full Text: arXiv OA License
Hazratpour, Sina; Riehl, Emily A 2-categorical proof of Frobenius for fibrations defined from a generic point. arXiv:2210.00078 Preprint, arXiv:2210.00078 [math.CT] (2022). MSC: 18N45 18N40 03B38 55U35 BibTeX Cite \textit{S. Hazratpour} and \textit{E. Riehl}, ``A 2-categorical proof of Frobenius for fibrations defined from a generic point'', Preprint, arXiv:2210.00078 [math.CT] (2022) Full Text: arXiv OA License
Corson, Samuel M. The nonabelian product modulo sum. arXiv:2206.02682 Preprint, arXiv:2206.02682 [math.GR] (2022). MSC: 03E75 20A15 55Q52 BibTeX Cite \textit{S. M. Corson}, ``The nonabelian product modulo sum'', Preprint, arXiv:2206.02682 [math.GR] (2022) Full Text: arXiv OA License
Weinberger, Jonathan Internal sums for synthetic fibered \((\infty,1)\)-categories. arXiv:2205.00386 Preprint, arXiv:2205.00386 [math.CT] (2022). MSC: 03B38 18N60 18D30 18B50 18N45 55U35 18N50 BibTeX Cite \textit{J. Weinberger}, ``Internal sums for synthetic fibered $(\infty,1)$-categories'', Preprint, arXiv:2205.00386 [math.CT] (2022) Full Text: arXiv OA License
Weinberger, Jonathan Two-sided cartesian fibrations of synthetic \((\infty,1)\)-categories. arXiv:2204.00938 Preprint, arXiv:2204.00938 [math.CT] (2022). MSC: 18N60 03B38 18D30 18N45 55U35 18N50 BibTeX Cite \textit{J. Weinberger}, ``Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories'', Preprint, arXiv:2204.00938 [math.CT] (2022) Full Text: arXiv OA License
Weinberger, Jonathan Strict stability of extension types. arXiv:2203.07194 Preprint, arXiv:2203.07194 [math.CT] (2022). MSC: 03B38 03G30 18N45 18N50 18N60 55U35 BibTeX Cite \textit{J. Weinberger}, ``Strict stability of extension types'', Preprint, arXiv:2203.07194 [math.CT] (2022) Full Text: arXiv OA License
Angere, Staffan Identity and intensionality in univalent foundations and philosophy. (English) Zbl 1507.03008 Synthese 198, Suppl. 5, S1177-S1217 (2021). MSC: 03A05 03B38 55U35 00A30 PDFBibTeX XMLCite \textit{S. Angere}, Synthese 198, S1177--S1217 (2021; Zbl 1507.03008) Full Text: DOI
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
Bentzen, Bruno Naive cubical type theory. (English) Zbl 07630474 Math. Struct. Comput. Sci. 31, No. 10, 1205-1231 (2021). MSC: 03B38 PDFBibTeX XMLCite \textit{B. Bentzen}, Math. Struct. Comput. Sci. 31, No. 10, 1205--1231 (2021; Zbl 07630474) Full Text: DOI arXiv
Swan, Andrew W.; Uemura, Taichi On Church’s thesis in cubical assemblies. (English) Zbl 07630473 Math. Struct. Comput. Sci. 31, No. 10, 1185-1204 (2021). MSC: 03B38 PDFBibTeX XMLCite \textit{A. W. Swan} and \textit{T. Uemura}, Math. Struct. Comput. Sci. 31, No. 10, 1185--1204 (2021; Zbl 07630473) Full Text: DOI arXiv
Mörtberg, Anders Cubical methods in homotopy type theory and univalent foundations. (English) Zbl 07630472 Math. Struct. Comput. Sci. 31, No. 10, 1147-1184 (2021). MSC: 03B38 PDFBibTeX XMLCite \textit{A. Mörtberg}, Math. Struct. Comput. Sci. 31, No. 10, 1147--1184 (2021; Zbl 07630472) Full Text: DOI
Licata, Dan (ed.); LeFanu Lumsdaine, Peter (ed.) Special issue on homotopy type theory 2019. (English) Zbl 1514.03007 Math. Struct. Comput. Sci. 31, No. 10, 1145-1146 (2021). MSC: 03-06 18-06 55-06 03B38 03G30 18N45 55U35 00B15 PDFBibTeX XMLCite \textit{D. Licata} (ed.) and \textit{P. LeFanu Lumsdaine} (ed.), Math. Struct. Comput. Sci. 31, No. 10, 1145--1146 (2021; Zbl 1514.03007) Full Text: DOI
Streicher, Thomas The genesis of the groupoid model. (English) Zbl 07547340 Math. Struct. Comput. Sci. 31, No. 9, 1003-1005 (2021). MSC: 03B38 PDFBibTeX XMLCite \textit{T. Streicher}, Math. Struct. Comput. Sci. 31, No. 9, 1003--1005 (2021; Zbl 07547340) Full Text: DOI
Coquand, Thierry; Ruch, Fabian; Sattler, Christian Constructive sheaf models of type theory. (English) Zbl 07547339 Math. Struct. Comput. Sci. 31, No. 9, 979-1002 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18F20 03B38 18N45 PDFBibTeX XMLCite \textit{T. Coquand} et al., Math. Struct. Comput. Sci. 31, No. 9, 979--1002 (2021; Zbl 07547339) Full Text: DOI arXiv
Angiuli, Carlo; Brunerie, Guillaume; Coquand, Thierry; Harper, Robert; Hou (Favonia), Kuen-Bang; Licata, Daniel R. Syntax and models of Cartesian cubical type theory. (English) Zbl 07460116 Math. Struct. Comput. Sci. 31, No. 4, 424-468 (2021). MSC: 03B38 55U35 18N45 PDFBibTeX XMLCite \textit{C. Angiuli} et al., Math. Struct. Comput. Sci. 31, No. 4, 424--468 (2021; Zbl 07460116) Full Text: DOI
Boulier, Simon; Tabareau, Nicolas Model structure on the universe of all types in interval type theory. (English) Zbl 07460115 Math. Struct. Comput. Sci. 31, No. 4, 392-423 (2021). MSC: 03B38 55U35 18N45 PDFBibTeX XMLCite \textit{S. Boulier} and \textit{N. Tabareau}, Math. Struct. Comput. Sci. 31, No. 4, 392--423 (2021; Zbl 07460115) Full Text: DOI
Cherubini, Felix; Rijke, Egbert Modal descent. (English) Zbl 1481.18029 Math. Struct. Comput. Sci. 31, No. 4, 363-391 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 03B10 PDFBibTeX XMLCite \textit{F. Cherubini} and \textit{E. Rijke}, Math. Struct. Comput. Sci. 31, No. 4, 363--391 (2021; Zbl 1481.18029) Full Text: DOI arXiv
Campion, Tim; Cousins, Greg; Ye, Jinhe Classifying spaces and the Lascar group. (English) Zbl 07457784 J. Symb. Log. 86, No. 4, 1396-1431 (2021). MSC: 03C48 03C52 18N50 55U10 PDFBibTeX XMLCite \textit{T. Campion} et al., J. Symb. Log. 86, No. 4, 1396--1431 (2021; Zbl 07457784) Full Text: DOI arXiv Backlinks: MO MO
Shulman, Michael Homotopy type theory: the logic of space. (English) Zbl 1479.18002 Anel, Mathieu (ed.) et al., New spaces in mathematics. Formal and conceptual reflections. Cambridge: Cambridge University Press. 322-403 (2021). Reviewer: Matteo Capucci (Glasgow) MSC: 18-03 03B70 18N45 PDFBibTeX XMLCite \textit{M. Shulman}, in: New spaces in mathematics. Formal and conceptual reflections. Cambridge: Cambridge University Press. 322--403 (2021; Zbl 1479.18002) Full Text: DOI arXiv Link
Gallozzi, Cesare Homotopy type-theoretic interpretations of constructive set theories. (English) Zbl 07408498 Math. Struct. Comput. Sci. 31, No. 1, 112-143 (2021). MSC: 03B38 03E70 18N45 PDFBibTeX XMLCite \textit{C. Gallozzi}, Math. Struct. Comput. Sci. 31, No. 1, 112--143 (2021; Zbl 07408498) Full Text: DOI
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
Isaev, Valery Indexed type theories. (English) Zbl 1494.18018 Math. Struct. Comput. Sci. 31, No. 1, 3-63 (2021). Reviewer: Marco Benini (Como) MSC: 18N45 03B38 55U35 PDFBibTeX XMLCite \textit{V. Isaev}, Math. Struct. Comput. Sci. 31, No. 1, 3--63 (2021; Zbl 1494.18018) Full Text: DOI arXiv
Hötzel Escardó, Martín The Cantor-Schröder-Bernstein theorem for \(\infty\)-groupoids. (English) Zbl 07402358 J. Homotopy Relat. Struct. 16, No. 3, 363-366 (2021). MSC: 03-XX 55U40 03B15 03F55 03B38 PDFBibTeX XMLCite \textit{M. Hötzel Escardó}, J. Homotopy Relat. Struct. 16, No. 3, 363--366 (2021; Zbl 07402358) Full Text: DOI arXiv
Dinis, Bruno; Edmundo, Mário J.; Mamino, Marcello Fundamental group in o-minimal structures with definable Skolem functions. (English) Zbl 07358543 Ann. Pure Appl. Logic 172, No. 8, Article ID 102975, 28 p. (2021). MSC: 03C64 55N30 58K10 55P65 PDFBibTeX XMLCite \textit{B. Dinis} et al., Ann. Pure Appl. Logic 172, No. 8, Article ID 102975, 28 p. (2021; Zbl 07358543) Full Text: DOI arXiv
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
Goubault, Éric; Ledent, Jérémy; Rajsbaum, Sergio A simplicial complex model for dynamic epistemic logic to study distributed task computability. (English) Zbl 1497.03032 Inf. Comput. 278, Article ID 104597, 22 p. (2021). Reviewer: Philippe Gaucher (Paris) MSC: 03B42 55U35 18N40 68M14 68Q85 PDFBibTeX XMLCite \textit{É. Goubault} et al., Inf. Comput. 278, Article ID 104597, 22 p. (2021; Zbl 1497.03032) Full Text: DOI arXiv Link
Veltri, Niccolò; van der Weide, Niels Constructing higher inductive types as groupoid quotients. (English) Zbl 1498.03037 Log. Methods Comput. Sci. 17, No. 2, Paper No. 8, 42 p. (2021). MSC: 03B38 18N10 55U35 PDFBibTeX XMLCite \textit{N. Veltri} and \textit{N. van der Weide}, Log. Methods Comput. Sci. 17, No. 2, Paper No. 8, 42 p. (2021; Zbl 1498.03037) Full Text: arXiv Link
Rasekh, Nima Every elementary higher topos has a natural number object. (English) Zbl 1464.18006 Theory Appl. Categ. 37, 337-377 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18B25 03G30 18N60 55U35 PDFBibTeX XMLCite \textit{N. Rasekh}, Theory Appl. Categ. 37, 337--377 (2021; Zbl 1464.18006) Full Text: arXiv Link
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
Droz, Jean-Marie; Zakharevich, Inna Extending to a model structure is not a first-order property. (English) Zbl 07319060 New York J. Math. 27, 319-348 (2021). MSC: 55U35 03B10 18B35 06A07 03C07 PDFBibTeX XMLCite \textit{J.-M. Droz} and \textit{I. Zakharevich}, New York J. Math. 27, 319--348 (2021; Zbl 07319060) Full Text: arXiv Link
Campion, Tim; Ye, Jinhe Homotopy types of abstract elementary classes. (English) Zbl 1498.03079 J. Pure Appl. Algebra 225, No. 5, Article ID 106461, 10 p. (2021). MSC: 03C48 03C52 03C75 18N40 55U35 PDFBibTeX XMLCite \textit{T. Campion} and \textit{J. Ye}, J. Pure Appl. Algebra 225, No. 5, Article ID 106461, 10 p. (2021; Zbl 1498.03079) Full Text: DOI arXiv
Ahrens, Benedikt; North, Paige Randall; Shulman, Michael; Tsementzis, Dimitris The Univalence Principle. arXiv:2102.06275 Preprint, arXiv:2102.06275 [math.CT] (2021). MSC: 18N99 03B38 03G30 55U35 BibTeX Cite \textit{B. Ahrens} et al., ``The Univalence Principle'', Preprint, arXiv:2102.06275 [math.CT] (2021) Full Text: arXiv OA License
Christensen, J. Daniel Non-accessible localizations. arXiv:2109.06670 Preprint, arXiv:2109.06670 [math.AT] (2021). MSC: 18N55 03B38 03B45 03G30 18E35 18N60 55P60 55U35 BibTeX Cite \textit{J. D. Christensen}, ``Non-accessible localizations'', Preprint, arXiv:2109.06670 [math.AT] (2021) Full Text: arXiv OA License
Barton, Reid; Commelin, Johan Model categories for o-minimal geometry. arXiv:2108.11952 Preprint, arXiv:2108.11952 [math.AT] (2021). MSC: 55U40 03C64 18F10 55U35 BibTeX Cite \textit{R. Barton} and \textit{J. Commelin}, ``Model categories for o-minimal geometry'', Preprint, arXiv:2108.11952 [math.AT] (2021) Full Text: arXiv OA License
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
Pinyo, Gun; Kraus, Nicolai From cubes to twisted cubes via graph morphisms in type theory. (English) Zbl 07756110 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 5, 18 p. (2020). MSC: 03B70 68N30 PDFBibTeX XMLCite \textit{G. Pinyo} and \textit{N. Kraus}, LIPIcs -- Leibniz Int. Proc. Inform. 175, Article 5, 18 p. (2020; Zbl 07756110) Full Text: DOI arXiv
Cavallo, Evan; Mörtberg, Anders; Swan, Andrew W. Unifying cubical models of univalent type theory. (English) Zbl 07650827 Fernández, Maribel (ed.) et al., 28th EACSL annual conference on computer science logic, CSL 2020, Barcelona, Spain, January 13–16, 2020. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 152, Article 14, 17 p. (2020). MSC: 68-XX 03B70 PDFBibTeX XMLCite \textit{E. Cavallo} et al., LIPIcs -- Leibniz Int. Proc. Inform. 152, Article 14, 17 p. (2020; Zbl 07650827) Full Text: DOI
Corfield, David Expressing ‘the structure of’ in homotopy type theory. (English) Zbl 1475.03022 Synthese 197, No. 2, 681-700 (2020). MSC: 03A05 03B38 55U35 PDFBibTeX XMLCite \textit{D. Corfield}, Synthese 197, No. 2, 681--700 (2020; Zbl 1475.03022) Full Text: DOI Backlinks: MO
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
van der Weide, Niels Constructing higher inductive types as groupoid quotients. (English) Zbl 1498.03036 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 929-943 (2020). MSC: 03B38 18N10 55U35 PDFBibTeX XMLCite \textit{N. van der Weide}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 929--943 (2020; Zbl 1498.03036) Full Text: DOI
Weaver, Matthew Z.; Licata, Daniel R. A constructive model of directed univalence in bicubical sets. (English) Zbl 1498.03038 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 915-928 (2020). MSC: 03B38 55U35 18N45 03F65 PDFBibTeX XMLCite \textit{M. Z. Weaver} and \textit{D. R. Licata}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 915--928 (2020; Zbl 1498.03038) Full Text: DOI
Sojakova, Kristina; Doorn, Floris van; Rijke, Egbert Sequential colimits in homotopy type theory. (English) Zbl 1498.03035 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 845-858 (2020). MSC: 03B38 55U35 18N45 PDFBibTeX XMLCite \textit{K. Sojakova} et al., in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 845--858 (2020; Zbl 1498.03035) Full Text: DOI
Sattler, Christian; Vezzosi, Andrea Partial univalence in \(n\)-truncated type theory. (English) Zbl 1498.03034 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 807-819 (2020). MSC: 03B38 55U35 18N45 PDFBibTeX XMLCite \textit{C. Sattler} and \textit{A. Vezzosi}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 807--819 (2020; Zbl 1498.03034) Full Text: DOI arXiv
Kraus, Nicolai; von Raumer, Jakob Coherence via well-foundedness. Taming set-quotients in homotopy type theory. (English) Zbl 1498.03033 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 662-675 (2020). MSC: 03B38 55U35 20E05 PDFBibTeX XMLCite \textit{N. Kraus} and \textit{J. von Raumer}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 662--675 (2020; Zbl 1498.03033) Full Text: DOI arXiv
Altenkirch, Thorsten; Scoccola, Luis The integers as a higher inductive type. (English) Zbl 1498.03028 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 67-73 (2020). MSC: 03B38 55U35 18N45 PDFBibTeX XMLCite \textit{T. Altenkirch} and \textit{L. Scoccola}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 67--73 (2020; Zbl 1498.03028) Full Text: DOI arXiv
Ahrens, Benedikt; North, Paige Randall; Shulman, Michael; Tsementzis, Dimitris A higher structure identity principle. (English) Zbl 1498.03027 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 53-66 (2020). MSC: 03B38 55U35 03F50 18N45 68Q60 PDFBibTeX XMLCite \textit{B. Ahrens} et al., in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 53--66 (2020; Zbl 1498.03027) Full Text: DOI arXiv
Scoccola, Luis Nilpotent types and fracture squares in homotopy type theory. (English) Zbl 1498.18038 Math. Struct. Comput. Sci. 30, No. 5, 511-544 (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B70 55P60 18E35 PDFBibTeX XMLCite \textit{L. Scoccola}, Math. Struct. Comput. Sci. 30, No. 5, 511--544 (2020; Zbl 1498.18038) Full Text: DOI arXiv
Anel, Mathieu; Biedermann, Georg; Finster, Eric; Joyal, André A generalized Blakers-Massey theorem. (English) Zbl 1456.18017 J. Topol. 13, No. 4, 1521-1553 (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N20 18B25 18N45 55U35 03B38 PDFBibTeX XMLCite \textit{M. Anel} et al., J. Topol. 13, No. 4, 1521--1553 (2020; Zbl 1456.18017) Full Text: DOI arXiv
Bentzen, Bruno What types should not be. (English) Zbl 1451.03009 Philos. Math. (3) 28, No. 1, 60-76 (2020). MSC: 03A05 03B38 55U35 PDFBibTeX XMLCite \textit{B. Bentzen}, Philos. Math. (3) 28, No. 1, 60--76 (2020; Zbl 1451.03009) Full Text: DOI Link
Kapulkin, Chris; Lefanu Lumsdaine, Peter The law of excluded middle in the simplicial model of type theory. (English) Zbl 1452.03038 Theory Appl. Categ. 35, 1546-1548 (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 03B38 55U10 18C50 55U35 PDFBibTeX XMLCite \textit{C. Kapulkin} and \textit{P. Lefanu Lumsdaine}, Theory Appl. Categ. 35, 1546--1548 (2020; Zbl 1452.03038) Full Text: arXiv Link
Henry, Simon Weak model categories in classical and constructive mathematics. (English) Zbl 1445.55013 Theory Appl. Categ. 35, 875-958 (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 55U35 55U40 18N40 18N50 18N65 03F65 PDFBibTeX XMLCite \textit{S. Henry}, Theory Appl. Categ. 35, 875--958 (2020; Zbl 1445.55013) Full Text: arXiv Link
Buchholtz, Ulrik; Hou, Kuen-Bang Cellular cohomology in homotopy type theory. (English) Zbl 1528.55013 Log. Methods Comput. Sci. 16, No. 2, Paper No. 7, 21 p. (2020). MSC: 55U35 03B38 55N20 PDFBibTeX XMLCite \textit{U. Buchholtz} and \textit{K.-B. Hou}, Log. Methods Comput. Sci. 16, No. 2, Paper No. 7, 21 p. (2020; Zbl 1528.55013) Full Text: arXiv Link
Barthel, Tobias; Schlank, Tomer M.; Stapleton, Nathaniel Chromatic homotopy theory is asymptotically algebraic. (English) Zbl 1442.55002 Invent. Math. 220, No. 3, 737-845 (2020). Reviewer: Jordan Williamson (Praha) MSC: 55N22 55P42 03C20 PDFBibTeX XMLCite \textit{T. Barthel} et al., Invent. Math. 220, No. 3, 737--845 (2020; Zbl 1442.55002) Full Text: DOI arXiv
Forssell, Henrik; Robbestad Gylterud, Håkon; Spivak, David I. Type theoretical databases. (English) Zbl 1474.68100 J. Log. Comput. 30, No. 1, 217-238 (2020). MSC: 68P15 03B38 18N50 55U35 PDFBibTeX XMLCite \textit{H. Forssell} et al., J. Log. Comput. 30, No. 1, 217--238 (2020; Zbl 1474.68100) Full Text: DOI
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
Dougherty, John The hole argument, take \(n\). (English) Zbl 1435.03034 Found. Phys. 50, No. 4, 330-347 (2020). MSC: 03B38 55U40 03A10 PDFBibTeX XMLCite \textit{J. Dougherty}, Found. Phys. 50, No. 4, 330--347 (2020; Zbl 1435.03034) Full Text: DOI
Gadgil, Siddhartha Homogeneous length functions on groups: intertwined computer and human proofs. (English) Zbl 1468.20081 J. Autom. Reasoning 64, No. 4, 677-688 (2020). MSC: 20F65 20F12 03B35 03B38 68V15 68V20 PDFBibTeX XMLCite \textit{S. Gadgil}, J. Autom. Reasoning 64, No. 4, 677--688 (2020; Zbl 1468.20081) Full Text: DOI arXiv
Gavrilovich, Misha Standard conjectures in model theory, and categoricity of comparison isomorphisms: a model theory perspective. (English) Zbl 1442.14072 Commun. Algebra 48, No. 4, 1548-1566 (2020). MSC: 14F20 11J89 11U09 03C45 14F35 PDFBibTeX XMLCite \textit{M. Gavrilovich}, Commun. Algebra 48, No. 4, 1548--1566 (2020; Zbl 1442.14072) Full Text: DOI arXiv
Barbieri-Viale, Luca; Prest, Mike Tensor product of motives via Künneth formula. (English) Zbl 1439.14077 J. Pure Appl. Algebra 224, No. 6, Article ID 106267, 13 p. (2020). MSC: 14F42 03C60 18C10 18E10 PDFBibTeX XMLCite \textit{L. Barbieri-Viale} and \textit{M. Prest}, J. Pure Appl. Algebra 224, No. 6, Article ID 106267, 13 p. (2020; Zbl 1439.14077) Full Text: DOI arXiv
Christensen, J. Daniel; Peck Opie, Morgan; Rijke, Egbert; Scoccola, Luis Nerio Localization in homotopy type theory. (English) Zbl 1439.18023 High. Struct. 4, No. 1, 1-32 (2020). MSC: 18N45 18E35 03B38 55P60 PDFBibTeX XMLCite \textit{J. D. Christensen} et al., High. Struct. 4, No. 1, 1--32 (2020; Zbl 1439.18023) Full Text: arXiv
Kaposi, Ambrus; Kovács, András Signatures and induction principles for higher inductive-inductive types. (English) Zbl 1528.03108 Log. Methods Comput. Sci. 16, No. 1, Paper No. 10, 30 p. (2020). MSC: 03B38 03G30 PDFBibTeX XMLCite \textit{A. Kaposi} and \textit{A. Kovács}, Log. Methods Comput. Sci. 16, No. 1, Paper No. 10, 30 p. (2020; Zbl 1528.03108) Full Text: arXiv
Rijke, Egbert; Shulman, Michael; Spitters, Bas Modalities in homotopy type theory. (English) Zbl 1489.03005 Log. Methods Comput. Sci. 16, No. 1, Paper No. 2, 79 p. (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 03B38 03B45 03G30 18N45 55U35 PDFBibTeX XMLCite \textit{E. Rijke} et al., Log. Methods Comput. Sci. 16, No. 1, Paper No. 2, 79 p. (2020; Zbl 1489.03005) Full Text: arXiv
Rodin, Andrei Models of HoTT and the constructive view of theories. (English) Zbl 1528.03112 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, 191-219 (2019). MSC: 03B38 03A05 18N45 55U35 PDFBibTeX XMLCite \textit{A. Rodin}, Synth. Libr. 407, 191--219 (2019; Zbl 1528.03112) Full Text: DOI
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
Ahrens, Benedikt; North, Paige Randall Univalent foundations and the equivalence principle. (English) Zbl 1528.03101 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, 137-150 (2019). MSC: 03B38 03G30 18N45 55U35 PDFBibTeX XMLCite \textit{B. Ahrens} and \textit{P. R. North}, Synth. Libr. 407, 137--150 (2019; Zbl 1528.03101) Full Text: DOI arXiv
Uemura, Taichi Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing. (English) Zbl 1528.03114 Dybjer, Peter (ed.) et al., 24th international conference on types for proofs and programs, TYPES 2018, Braga, Portugal, June 18–21, 2018. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 130, Article 7, 20 p. (2019). MSC: 03B38 03G30 18N40 55U35 PDFBibTeX XMLCite \textit{T. Uemura}, LIPIcs -- Leibniz Int. Proc. Inform. 130, Article 7, 20 p. (2019; Zbl 1528.03114) Full Text: DOI arXiv
Coquand, Thierry; Huber, Simon; Sattler, Christian Homotopy canonicity for cubical type theory. (English) Zbl 1528.03106 Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 11, 23 p. (2019). MSC: 03B38 03G30 55U35 PDFBibTeX XMLCite \textit{T. Coquand} et al., LIPIcs -- Leibniz Int. Proc. Inform. 131, Article 11, 23 p. (2019; Zbl 1528.03106) Full Text: DOI
Mainzer, Klaus From mathesis universalis to provability, computability, and constructivity. (English) Zbl 1469.03113 Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 203-234 (2019). MSC: 03D10 03D35 03F35 03F60 03B30 03F25 68V15 03B38 55U40 PDFBibTeX XMLCite \textit{K. Mainzer}, Synth. Libr. 412, 203--234 (2019; Zbl 1469.03113) Full Text: DOI
Awodey, Steve Mathesis universalis and homotopy type theory. (English) Zbl 1469.03035 Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 13-36 (2019). MSC: 03B38 55U40 PDFBibTeX XMLCite \textit{S. Awodey}, Synth. Libr. 412, 13--36 (2019; Zbl 1469.03035) 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
Zhan, Bohua Formalization of the fundamental group in untyped set theory using auto2. (English) Zbl 1468.68332 J. Autom. Reasoning 63, No. 2, 517-538 (2019). MSC: 68V20 03B35 03E30 55Q05 PDFBibTeX XMLCite \textit{B. Zhan}, J. Autom. Reasoning 63, No. 2, 517--538 (2019; Zbl 1468.68332) Full Text: DOI arXiv
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
Brunerie, Guillaume The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory. (English) Zbl 1477.03035 J. Autom. Reasoning 63, No. 2, 255-284 (2019). MSC: 03B38 03B35 55U35 PDFBibTeX XMLCite \textit{G. Brunerie}, J. Autom. Reasoning 63, No. 2, 255--284 (2019; Zbl 1477.03035) Full Text: DOI arXiv
Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea Guarded cubical type theory. (English) Zbl 1477.03034 J. Autom. Reasoning 63, No. 2, 211-253 (2019). MSC: 03B38 55U35 18F20 PDFBibTeX XMLCite \textit{L. Birkedal} et al., J. Autom. Reasoning 63, No. 2, 211--253 (2019; Zbl 1477.03034) Full Text: DOI arXiv Link
Bezem, Marc; Coquand, Thierry; Huber, Simon The univalence axiom in cubical sets. (English) Zbl 1506.03064 J. Autom. Reasoning 63, No. 2, 159-171 (2019). MSC: 03B38 55U35 18N45 03F65 PDFBibTeX XMLCite \textit{M. Bezem} et al., J. Autom. Reasoning 63, No. 2, 159--171 (2019; Zbl 1506.03064) Full Text: DOI arXiv