Petrakis, Iosif; Zeuner, Max Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory. (English) Zbl 07941273 Log. Methods Comput. Sci. 20, No. 4, Paper No. 2, 33 p. (2024). MSC: 03F60 28-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Kotiuga, P. Robert; Lahtinen, Valtteri An electrical engineering perspective on naturality in computational physics. (English) Zbl 07932068 Adv. Comput. Math. 50, No. 5, Paper No. 103, 41 p. (2024). MSC: 65N22 65N30 58J10 55U15 55U10 53Z30 78M10 78M35 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Prieto-Cubides, Jonathan; Robbestad Gylterud, Håkon On planarity of graphs in homotopy type theory. (English) Zbl 07927454 Math. Struct. Comput. Sci. 34, No. 4, 281-321 (2024). MSC: 03-XX 05-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Myers, David Jaz Modal fracture of higher groups. (English) Zbl 07922727 Differ. Geom. Appl. 96, Article ID 102176, 54 p. (2024). MSC: 18-XX 55-XX 57-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Schroeder-Heister, Peter Proof-theoretic semantics: an autobiographical survey. (English) Zbl 07920750 Piecha, Thomas (ed.) et al., Peter Schroeder-Heister on proof-theoretic semantics. Cham: Springer. Outst. Contrib. Log. 29, 1-51 (2024). MSC: 03Fxx × Cite Format Result Cite Review PDF Full Text: DOI
Weinberger, Jonathan Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories. (English) Zbl 07919890 J. Homotopy Relat. Struct. 19, No. 3, 297-378 (2024). MSC: 18N60 03B38 18D30 18N45 55U35 18N50 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Chen, Lu Univalence and ontic structuralism. (English) Zbl 07896336 Found. Phys. 54, No. 3, Paper No. 38, 27 p. (2024). MSC: 03Bxx 55Uxx 03Axx × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Awodey, Steve; Gambino, Nicola; Hazratpour, Sina Kripke-Joyal forcing for type theory and uniform fibrations. (English) Zbl 07896247 Sel. Math., New Ser. 30, No. 4, Paper No. 74, 70 p. (2024). MSC: 03C25 03G30 18B25 18C50 55P05 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Myers, David Jaz; Sati, Hisham; Schreiber, Urs Topological quantum gates in homotopy type theory. (English) Zbl 07893326 Commun. Math. Phys. 405, No. 7, Paper No. 172, 114 p. (2024). MSC: 81Txx 81Pxx 03B38 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Arsiwalla, Xerxes D.; Gorard, Jonathan Pregeometric spaces from Wolfram model rewriting systems as homotopy types. (English) Zbl 07879176 Int. J. Theor. Phys. 63, No. 4, Paper No. 83, 44 p. (2024). MSC: 68Qxx 81Txx 83Cxx × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Christensen, J. Daniel Non-accessible localizations. (English) Zbl 07873630 J. Topol. 17, No. 2, Article ID e12336, 19 p. (2024). Reviewer: Raffael Stenzel (Bonn) MSC: 18N55 03B38 03G30 18N60 18E35 55P60 55U35 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Nuyts, Andreas; Devriese, Dominique Transpension: the right adjoint to the Pi-type. (English) Zbl 07872363 Log. Methods Comput. Sci. 20, No. 2, Paper No. 16, 54 p. (2024). MSC: 03B70 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv Backlinks: MO
Dean, Christopher J.; Finster, Eric; Markakis, Ioannis; Reutter, David; Vicary, Jamie Computads for weak \(\omega \)-categories as an inductive type. (English) Zbl 1541.18030 Adv. Math. 450, Article ID 109739, 70 p. (2024). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N20 18N30 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Ochigame, Rodrigo Automated mathematics and the reconfiguration of proof and labor. (English) Zbl 1541.00040 Bull. Am. Math. Soc., New Ser. 61, No. 3, 423-437 (2024). MSC: 00A30 01A80 68V15 68T01 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Weinberger, Jonathan Internal sums for synthetic fibered \((\infty,1)\)-categories. (English) Zbl 07842164 J. Pure Appl. Algebra 228, No. 9, Article ID 107659, 52 p. (2024). MSC: 03B38 18N60 18D30 18B50 18N45 55U35 18N50 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Shulman, Michael Strange new universes: proof assistants and synthetic foundations. (English) Zbl 1540.68274 Bull. Am. Math. Soc., New Ser. 61, No. 2, 257-270 (2024). MSC: 68V15 68V20 × Cite Format Result Cite Review PDF Full Text: DOI Backlinks: MO MO
Riehl, Emily On the \(\infty\)-topos semantics of homotopy type theory. (English) Zbl 1533.18019 Bull. Lond. Math. Soc. 56, No. 2, 461-517 (2024). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N40 18N45 18N60 03B38 55U10 55U40 × Cite Format Result Cite Review PDF Full Text: DOI arXiv Backlinks: MO
Contente, Michele; Maietti, Maria Emilia The compatibility of the minimalist foundation with homotopy type theory. (English) Zbl 07811876 Theor. Comput. Sci. 991, Article ID 114421, 30 p. (2024). MSC: 03-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
East, James; Azeef Muhammed, P. A. A groupoid approach to regular \(\ast \)-semigroups. (English) Zbl 1531.20071 Adv. Math. 437, Article ID 109447, 104 p. (2024). MSC: 20M10 20M50 18B40 20M17 20M20 20M05 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Maruyama, Yoshihiro Duality, intensionality, and contextuality: philosophy of category theory and the categorical unity of science in Samson Abramsky. (English) Zbl 07920675 Palmigiano, Alessandra (ed.) et al., Samson Abramsky on logic and structure in computer science and beyond. Cham: Springer. Outst. Contrib. Log. 25, 41-88 (2023). MSC: 03B70 68Qxx 81P68 × Cite Format Result Cite Review PDF Full Text: DOI
Benjamin, Thibaut Monoidal weak \(\omega\)-categories as models of a type theory. (English) Zbl 07813367 Math. Struct. Comput. Sci. 33, No. 8, 744-780 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Annenkov, Danil; Capriotti, Paolo; Kraus, Nicolai; Sattler, Christian Two-level type theory and applications. (English) Zbl 07813366 Math. Struct. Comput. Sci. 33, No. 8, 688-743 (2023); erratum ibid. 34, No. 1, 80 (2024). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Buchholtz, Ulrik; Rijke, Egbert The long exact sequence of homotopy \(n\)-groups. (English) Zbl 07813365 Math. Struct. Comput. Sci. 33, No. 8, 679-687 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Stenzel, Raffael On notions of compactness, object classifiers, and weak Tarski universes. (English) Zbl 07813364 Math. Struct. Comput. Sci. 33, No. 8, 661-678 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv Backlinks: MO
Yamada, Norihiro Game semantics of Martin-Löf type theory. (English) Zbl 07813361 Math. Struct. Comput. Sci. 33, No. 7, 605-646 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Uemura, Taichi A general framework for the semantics of type theory. (English) Zbl 07813328 Math. Struct. Comput. Sci. 33, No. 3, 134-179 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Taxerås Flaten, Jarl G. Univalent categories of modules. (English) Zbl 07813327 Math. Struct. Comput. Sci. 33, No. 2, 106-133 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Rasekh, Nima Cartesian fibrations of complete Segal spaces. (English) Zbl 1536.18017 High. Struct. 7, No. 1, 40-73 (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N60 18N40 18N50 18N55 18F20 × Cite Format Result Cite Review PDF Full Text: arXiv Link
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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Escardó, Martín; Oliva, Paulo Higher-order games with dependent types. (English) Zbl 07739131 Theor. Comput. Sci. 974, Article ID 114111, 11 p. (2023). MSC: 68Qxx × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Christensen, J. Daniel; Scoccola, Luis The Hurewicz theorem in homotopy type theory. (English) Zbl 1544.55014 Algebr. Geom. Topol. 23, No. 5, 2107-2140 (2023). Reviewer: Ödül Tetik (Vienna) MSC: 55Q99 03B38 18N60 55N99 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Popescu, Andrei Rensets and renaming-based recursion for syntax with bindings extended version. (English) Zbl 07722430 J. Autom. Reasoning 67, No. 3, Paper No. 23, 27 p. (2023). MSC: 68V15 × Cite Format Result Cite Review PDF Full Text: DOI
Rasekh, Nima Yoneda lemma for simplicial spaces. (English) Zbl 1516.18018 Appl. Categ. Struct. 31, No. 4, Paper No. 27, 92 p. (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N60 18N40 18N50 18F20 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Sterling, Jonathan What should a generic object be? (English) Zbl 07712490 Math. Struct. Comput. Sci. 33, No. 1, 46-67 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Sato, Masahiro; Garrigue, Jacques An intuitionistic set-theoretical model of fully dependent CC\(^{\boldsymbol{\omega}}\). (English) Zbl 07712488 Math. Struct. Comput. Sci. 33, No. 1, 1-32 (2023). MSC: 68-XX × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Martínez-Rivillas, Daniel O.; de Queiroz, Ruy J. G. B. Towards a homotopy domain theory. (English) Zbl 07680036 Arch. Math. Logic 62, No. 3-4, 559-579 (2023). MSC: 03B70 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Veltri, Niccolò; Vezzosi, Andrea Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda. (English) Zbl 1512.68176 J. Log. Algebr. Methods Program. 131, Article ID 100846, 23 p. (2023). MSC: 68Q85 68N18 68Q55 × Cite Format Result Cite Review PDF Full Text: DOI
Stenzel, Raffael Univalence and completeness of Segal objects. (English) Zbl 1502.18048 J. Pure Appl. Algebra 227, No. 4, Article ID 107254, 47 p. (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 18N50 18N60 18C50 55U35 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Pitts, Andrew M.; Steenkamp, S. C. Constructing initial algebras using inflationary iteration. (English) Zbl 1530.18006 Kishida, Kohei (ed.), Proceedings of the fourth international conference on applied category theory 2021, ACT 2021, Cambridge, UK, July 12–16, 2021. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 372, 88-102 (2022). MSC: 18A40 03F65 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Swan, Andrew W. A class of higher inductive types in Zermelo-Fraenkel set theory. (English) Zbl 1521.03025 Math. Log. Q. 68, No. 1, 118-127 (2022). MSC: 03B38 03E55 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Gambino, Nicola; Henry, Simon Towards a constructive simplicial model of univalent foundations. (English) Zbl 1527.18022 J. Lond. Math. Soc., II. Ser. 105, No. 2, 1073-1109 (2022). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03G30 03F50 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Yaghmaie, Aboutorab; Ahmadi Kakavandi, Bijan; Masoumi, Saeed; Moniri, Morteza Representation and spacetime: the hole argument revisited. (English) Zbl 1522.83013 Int. Stud. Philos. Sci. 35, No. 2, 171-188 (2022). MSC: 83C05 83E05 00A30 03B38 × Cite Format Result Cite Review PDF Full Text: DOI
Hinze, Ralf; Swierstra, Wouter Calculating datastructures. (English) Zbl 07705358 Komendantskaya, Ekaterina (ed.), Mathematics of program construction. 14th international conference, MPC 2022, Tbilisi, Georgia, September 26–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13544, 62-101 (2022). MSC: 68N30 × Cite Format Result Cite Review PDF Full Text: DOI
Hewer, Brandon; Hutton, Graham Subtyping without reduction. (English) Zbl 07705357 Komendantskaya, Ekaterina (ed.), Mathematics of program construction. 14th international conference, MPC 2022, Tbilisi, Georgia, September 26–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13544, 34-61 (2022). MSC: 68N30 × Cite Format Result Cite Review PDF Full Text: DOI
Fuenmayor, David; Serrano Suárez, Fabián Fernando Formalising basic topology for computational logic in simple type theory. (English) Zbl 07691290 Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 56-74 (2022). MSC: 68V20 03G05 06E25 54A05 × Cite Format Result Cite Review PDF Full Text: DOI
Palmgren, Erik From type theory to setoids and back. (English) Zbl 07676407 Math. Struct. Comput. Sci. 32, No. 10, 1283-1312 (2022). MSC: 03-XX × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Cottrell, Thomas; Fujii, Soichiro Hom weak \(\omega\)-categories of a weak \(\omega\)-category. (English) Zbl 1520.18025 Math. Struct. Comput. Sci. 32, No. 4, 420-441 (2022). Reviewer: Alexander Prähauser (Wien) MSC: 18N65 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Schroeder-Heister, Peter Axiomatic thinking, identity of proofs and the quest for an intensional proof-theoretic semantics. (English) Zbl 07633000 Ferreira, Fernando (ed.) et al., Axiomatic thinking I. Cham: Springer. 145-163 (2022). MSC: 03-03 03A05 00A30 01A80 01A60 × Cite Format Result Cite Review PDF Full Text: DOI
Petrakis, Iosif Proof-relevance in Bishop-style constructive mathematics. (English) Zbl 1531.03098 Math. Struct. Comput. Sci. 32, No. 1, 1-43 (2022). Reviewer: Daniel A. Romano (Banja Luka) MSC: 03F65 03B38 × Cite Format Result Cite Review PDF Full Text: DOI
Popescu, Andrei Rensets and renaming-based recursion for syntax with bindings. (English) Zbl 07628212 Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 618-639 (2022). MSC: 68V15 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Shulman, Michael Affine logic for constructive mathematics. (English) Zbl 07606771 Bull. Symb. Log. 28, No. 3, 327-386 (2022). MSC: 03F52 03F65 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Crosilla, Laura Predicativity and constructive mathematics. (English) Zbl 07598443 Oliveri, Gianluigi (ed.) et al., Objects, structures, and logics. FilMat studies in the philosophy of mathematics. Cham: Springer. Boston Stud. Philos. Hist. Sci. 339, 287-309 (2022). MSC: 03-XX 00A30 × Cite Format Result Cite Review PDF Full Text: DOI Link
Marquis, Jean-Pierre The structuralist mathematical style: Bourbaki as a case study. (English) Zbl 07598440 Oliveri, Gianluigi (ed.) et al., Objects, structures, and logics. FilMat studies in the philosophy of mathematics. Cham: Springer. Boston Stud. Philos. Hist. Sci. 339, 199-231 (2022). MSC: 03-XX 00A30 × Cite Format Result Cite Review PDF Full Text: DOI Link
Tohmé, Fernando; Caterina, Gianluca; Gangle, Rocco Observability in the univalent universe. (English) Zbl 07592507 Mediterr. J. Math. 19, No. 5, Paper No. 216, 19 p. (2022). MSC: 03-XX 68-XX × Cite Format Result Cite Review PDF Full Text: DOI
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 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Sterling, Jonathan; Angiuli, Carlo; Gratzer, Daniel A cubical language for Bishop sets. (English) Zbl 07566056 Log. Methods Comput. Sci. 18, No. 1, Paper No. 43, 80 p. (2022). MSC: 03B70 68-XX × Cite Format Result Cite Review PDF Full Text: arXiv Link
Emmenegger, Jacopo; Pasquali, Fabio; Rosolini, Giuseppe A characterisation of elementary fibrations. (English) Zbl 1492.18008 Ann. Pure Appl. Logic 173, No. 6, Article ID 103103, 29 p. (2022). Reviewer: Robert Rosebrugh (Sackville) MSC: 18C40 18C50 03G30 18D30 18D40 18N45 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Anel, Mathieu; Biedermann, Georg; Finster, Eric; Joyal, André Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves. (English) Zbl 1498.18009 Adv. Math. 400, Article ID 108268, 64 p. (2022). Reviewer: Markus Szymik (Sheffield) MSC: 18F20 18N60 18N55 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Barton, Neil; Müller, Moritz; Prunescu, Mihai On representations of intended structures in foundational theories. (English) Zbl 07502595 J. Philos. Log. 51, No. 2, 283-296 (2022). MSC: 03-XX × Cite Format Result Cite Review PDF Full Text: DOI
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 × Cite Format Result Cite Review PDF 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: 20J15 03B38 55U35 18B25 18N45 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Bordg, Anthony The interpretation lifting theorem for C-systems. (English) Zbl 1483.18003 Theory Appl. Categ. 38, 214-231 (2022). Reviewer: Sergejs Solovjovs (Praha) MSC: 18C10 18C50 18F20 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
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 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
de Jong, Tom The Scott model of PCF in univalent type theory. (English) Zbl 1517.68069 Math. Struct. Comput. Sci. 31, No. 10, 1270-1300 (2021). MSC: 68N18 03B38 06B35 18B25 18C50 18N45 68N30 68Q55 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; Veltri, Niccolò; van der Weide, Niels Bicategories in univalent foundations. (English) Zbl 1514.18019 Math. Struct. Comput. Sci. 31, No. 10, 1232-1269 (2021). MSC: 18N10 03B38 18N45 68V20 × Cite Format Result Cite Review PDF Full Text: DOI
Bentzen, Bruno Naive cubical type theory. (English) Zbl 07630474 Math. Struct. Comput. Sci. 31, No. 10, 1205-1231 (2021). MSC: 03B38 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI
Coquand, Thierry; Ruch, Fabian; Sattler, Christian Constructive sheaf models of type theory. (English) Zbl 1529.18006 Math. Struct. Comput. Sci. 31, No. 9, 979-1002 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18F20 03B38 18N45 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Emmenegger, Jacopo; Pasquali, Fabio; Rosolini, Giuseppe Elementary fibrations of enriched groupoids. (English) Zbl 07547338 Math. Struct. Comput. Sci. 31, No. 9, 958-978 (2021). MSC: 03B38 03G30 18B40 18D20 × Cite Format Result Cite Review PDF Full Text: DOI
Altenkirch, Thorsten Martin Hofmann’s contributions to type theory: groupoids and univalence. (English) Zbl 1496.03003 Math. Struct. Comput. Sci. 31, No. 9, 953-957 (2021). MSC: 03-03 01A70 03B38 × Cite Format Result Cite Review PDF Full Text: DOI
Turner, D. A. Constructive mathematics, Church’s thesis, and free choice sequences. (English) Zbl 07495191 De Mol, Liesbeth (ed.) et al., Connecting with computability. 17th conference on computability in Europe, CiE 2021, virtual event, Ghent, Belgium, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12813, 446-456 (2021). MSC: 68Qxx × Cite Format Result Cite Review PDF Full Text: DOI Link
Cavallo, Evan; Harper, Robert Internal parametricity for cubical type theory. (English) Zbl 1508.03047 Log. Methods Comput. Sci. 17, No. 4, Paper No. 5, 60 p. (2021). Reviewer: Jonathan Weinberger (Baltimore) MSC: 03B38 × Cite Format Result Cite Review PDF Full Text: arXiv Link
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 1529.03123 Math. Struct. Comput. Sci. 31, No. 4, 424-468 (2021). MSC: 03B38 55U35 18N45 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Botta, Nicola; Brede, Nuria; Jansson, Patrik; Richter, Tim Extensional equality preservation and verified generic programming. (English) Zbl 1522.68119 J. Funct. Program. 31, Paper No. e24, 24 p. (2021). MSC: 68N18 03B38 03B70 18C20 68Q65 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
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 × Cite Format Result Cite Review PDF Full Text: DOI
Ellerman, David On abstraction in mathematics and indefiniteness in quantum mechanics. (English) Zbl 07413738 J. Philos. Log. 50, No. 4, 813-835 (2021). MSC: 03A05 00A30 81P05 × Cite Format Result Cite Review PDF Full Text: DOI Link
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Sattler, Christian; Sestini, Filippo Constructing a universe for the setoid model. (English) Zbl 07410416 Kiefer, Stefan (ed.) et al., Foundations of software science and computation structures. 24th international conference, FOSSACS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12650, 1-21 (2021). MSC: 68Nxx 68Qxx × Cite Format Result Cite Review PDF Full Text: DOI
Gallozzi, Cesare Homotopy type-theoretic interpretations of constructive set theories. (English) Zbl 07408498 Math. Struct. Comput. Sci. 31, No. 1, 112-143 (2021). MSC: 03E70 03B38 03F50 × Cite Format Result Cite Review PDF Full Text: DOI
Hötzel Escardó, Martín Injective types in univalent mathematics. (English) Zbl 1478.18025 Math. Struct. Comput. Sci. 31, No. 1, 89-111 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
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 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Emmenegger, Jacopo W-types in setoids. (English) Zbl 1505.03029 Log. Methods Comput. Sci. 17, No. 3, Paper No. 28, 33 p. (2021). Reviewer: Jonathan Sterling (Aarhus) MSC: 03B38 03B35 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Hyvernat, Pierre Representing continuous functions between greatest fixed points of indexed containers. (English) Zbl 07407785 Log. Methods Comput. Sci. 17, No. 3, Paper No. 13, 30 p. (2021). MSC: 68N30 03B38 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Gratzer, Daniel; Kavvos, G. A.; Nuyts, Andreas; Birkedal, Lars Multimodal dependent type theory. (English) Zbl 1498.03030 Log. Methods Comput. Sci. 17, No. 3, Paper No. 11, 67 p. (2021). MSC: 03B38 03B45 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Hötzel Escardó, Martín The Cantor-Schröder-Bernstein theorem for \(\infty\)-groupoids. (English) Zbl 1534.03022 J. Homotopy Relat. Struct. 16, No. 3, 363-366 (2021). MSC: 03B38 55U35 18N45 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Rasekh, Nima Filter quotients and non-presentable \((\infty,1)\)-toposes. (English) Zbl 1467.18045 J. Pure Appl. Algebra 225, No. 12, Article ID 106770, 36 p. (2021). Reviewer: Philippe Gaucher (Paris) MSC: 18N60 18B25 18N45 55U35 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Posur, Sebastian A constructive approach to Freyd categories. (English) Zbl 1478.18008 Appl. Categ. Struct. 29, No. 1, 171-211 (2021). MSC: 18E10 18E05 18A25 16S99 18C35 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Kapulkin, Krzysztof; Lumsdaine, Peter Lefanu The simplicial model of univalent foundations (after Voevodsky). (English) Zbl 1471.18025 J. Eur. Math. Soc. (JEMS) 23, No. 6, 2071-2126 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 18C50 55U10 55U35 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael Construction of the circle in UniMath. (English) Zbl 1542.03038 J. Pure Appl. Algebra 225, No. 10, Article ID 106687, 21 p. (2021). MSC: 03B38 03B70 55U35 03G30 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
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 × Cite Format Result Cite Review PDF Full Text: arXiv Link
Petrakis, Iosif Direct spectra of Bishop spaces and their limits. (English) Zbl 1473.03038 Log. Methods Comput. Sci. 17, No. 2, Paper No. 4, 50 p. (2021). Reviewer: Daniel Romano (Banja Luka) MSC: 03F65 03F60 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: arXiv Link