Observability in the univalent universe. (English) Zbl 07592507
Summary: In this paper, we present a summary of Homotopy Type Theory with Voevodsky’s Univalent Axiom and discuss the existence of a universe of types satisfying the latter. We take up the idea of the observability of the behavior of computations, as defined in the grossone framework, in which for every finite natural number \(n\), \(n\leq\) \textcircled{1}. In this context, the number of complete computable sequences that can be enumerated by imaginary Turing machines is equal to \textcircled{1}. We replace the notion of \(\infty\)-topos of \(\infty\)-groupoids by a \textcircled{1}-topos of \textcircled{1}-groupoids as a model of Type Theory. We find that in this setting there exists a universe of types satisfying univalence, ensuring the completeness of the sequences generated by type-theoretic computations.
References:
| [1] | Awodey, S.: From Sets to Types, to Categories, to Sets. In: Sommaruga G. (ed.) Foundational Theories of Classical and Constructive Mathematics. The Western Ontario Series in Philosophy of Science, vol 76. Springer, Dordrecht (2011) · Zbl 1317.03016 |
| [2] | Baez, J.: The Homotopy Hypothesis, https://math.ucr.edu/home/baez/homotopy/homotopy.pdf (2007) |
| [3] | Bauer, A., Coquand, T., Gambino, N.: Homotopy Type Theory: Unified Foundations of Mathematics and Computation (MURI Proposal) (2014) |
| [4] | Caldarola, F., The sierpinski curve viewed by numerical computations with infinities and infinitesimals, Appl. Math. Comput., 318, 321-328 (2018) · Zbl 1426.28016 · doi:10.1016/j.amc.2017.06.024 |
| [5] | Cococcioni, M.; Pappalardo, M.; Sergeyev, Y., Lexicographic multi-objective linear programming using Grossone methodology: theory and algorithms, Appl. Math. Comput., 318, 298-311 (2018) · Zbl 1426.90226 · doi:10.1016/j.amc.2017.05.058 |
| [6] | Cococcioni, M.; Cudazzo, A.; Pappalardo, M.; Sergeyev, Y., Solving the Lexicographic multi-objective mixed-integer linear programming problem using Branch-and-Bound and Grossone methodology, Commun. Nonlinear Sci. Numer. Simul., 84, 1-20 (2020) · Zbl 1451.90140 · doi:10.1016/j.cnsns.2020.105177 |
| [7] | Coquand, T.; Danielsson, NA, Isomorphism is equality, Indag. Math., 24, 1105-1120 (2013) · Zbl 1359.03010 · doi:10.1016/j.indag.2013.09.002 |
| [8] | D’Alotto, L., Cellular automata using infinite computations, Appl. Math. Comput., 218, 8077-8082 (2012) · Zbl 1252.37017 · doi:10.1016/j.amc.2011.10.065 |
| [9] | D’Alotto, L., A classification of two-dimensional cellular automata using infinite computations, Indian J. Math., 55, 143-158 (2013) · Zbl 1371.37017 |
| [10] | D’Alotto, L., A classification of one-dimensional cellular automata using infinite computations, Appl. Math. Comput., 255, 15-24 (2015) · Zbl 1338.68177 · doi:10.1016/j.amc.2014.06.087 |
| [11] | De Cosmis, S.; De Leone, R., The use of Grossone in mathematical programming and operations research, Appl. Math. Comput., 218, 8029-8038 (2012) · Zbl 1273.90117 · doi:10.1016/j.amc.2011.07.042 |
| [12] | Fiaschi, L.; Cococcioni, M., Numerical asymptotic results in game theory using Sergeyev’s infinity computing, Int. J. Unconv. Comput., 14, 1-25 (2018) |
| [13] | Flori, C., Fritz, T.: Homotopy Type Theory: Univalent Foundations of Mathematics. Lecture notes of course taught at the University of Waterloo, Canada (http://tobiasfritz.science/2014/HoTTlecturenotes.pdf). (2014) |
| [14] | Fong, B.; Spivak, DI, An Invitation to Applied Category Theory: Seven Sketches in Compositionality (2019), Cambridge (MA): Cambridge University Press, Cambridge (MA) · Zbl 1464.18001 · doi:10.1017/9781108668804 |
| [15] | Friedman, G., An elementary illustrated introduction to simplicial sets, Rocky Mt. J. Math., 42, 353-423 (2012) · Zbl 1248.55001 · doi:10.1216/RMJ-2012-42-2-353 |
| [16] | Grothendieck, A.: Pursuing Stacks, Unpublished Manuscript: http://cm2vivi2002.free.fr/AG-biblio/AG-54.pdf (1983) |
| [17] | Hofmann, M.; Streicher, T., The Groupoid interpretation of type theory, Oxford Logic Guid., 36, 83-111 (1998) · Zbl 0930.03089 |
| [18] | Iudin, D.; Sergeyev, Y.; Hayakawa, M., Interpretation of percolation in terms of infinity computations, Appl. Math. Comput., 218, 8099-8111 (2012) · Zbl 1252.82059 · doi:10.1016/j.amc.2011.11.044 |
| [19] | Johnston, P., Sketches of an Elephant: A Topos Theory Compendium (2002), UK: Oxford University Press, UK · Zbl 1071.18001 |
| [20] | Joyal, A., Quasi-categories and Kan complexes, J. Pure Appl. Alg., 175, 207-222 (2005) · Zbl 1015.18008 · doi:10.1016/S0022-4049(02)00135-4 |
| [21] | Kapulkin, K.- Lumsdaine, P.: The simplicial model of univalent foundations (After Voevodsky), arXiv:1211.2851 (2018) · Zbl 1471.18025 |
| [22] | Kauffman, L., Infinite computations and the Generic finite, Appl. Math. Comput., 255, 25-35 (2015) · Zbl 1338.68083 · doi:10.1016/j.amc.2014.06.054 |
| [23] | Ladyman, J.; Presnell, S., Identity in homotopy type theory, part i: the justification of path induction, Philos. Math., 23, 386-406 (2015) · Zbl 1380.03027 · doi:10.1093/philmat/nkv014 |
| [24] | Licata, D., Brunerie, G.: A cubical approach to synthetic homotopy theory. 30th annual ACM/IEEE symposium on logic in computer science (2015) · Zbl 1395.55019 |
| [25] | Lolli, G., Metamathematical investigations on the theory of Grossone, Appl. Math. Comput., 255, 3-14 (2015) · Zbl 1338.03118 · doi:10.1016/j.amc.2014.03.140 |
| [26] | Lolli, G., Infinitesimals and infinities in the history of mathematics: a brief survey, Appl. Math. Comput., 218, 7979-7988 (2012) · Zbl 1255.01001 · doi:10.1016/j.amc.2011.08.092 |
| [27] | Lumsdaine, P.: Higher categories from type theories, Ph.D. thesis, Carnegie-Mellon University (http://www.mathstat.dal.ca/ p.l.lumsdaine) (2010) · Zbl 1250.03127 |
| [28] | Lurie, J., Higher topos theory (2009), Princeton (NJ): Princeton University Press, Princeton (NJ) · Zbl 1175.18001 · doi:10.1515/9781400830558 |
| [29] | Lurie, J., What is an \(\infty\) category?, Not. Am. Math. Soc., 55, 949-950 (2008) · Zbl 1194.55016 |
| [30] | Margenstern, M., Using Grossone to count the number of elements of infinite sets and the connection with Bijections, P-Adic Num. Ultramet. Anal. Appl., 3, 3, 196-204 (2011) · Zbl 1259.03064 · doi:10.1134/S2070046611030034 |
| [31] | Martin-Löf, P., An intuitionistic theory of types: predicative part, Stud. Logic Foundat. Math., 80, 73-118 (1975) · Zbl 0334.02016 · doi:10.1016/S0049-237X(08)71945-1 |
| [32] | Minsky, M., Computation: finite and infinite machines (1967), Hoboken (NJ): Prentice-Hall, Hoboken (NJ) · Zbl 0195.02402 |
| [33] | Montagna, F.; Simi, G.; Sorbi, A., Taking the Pirahã seriously, Commun. Nonlinear Sci. Numer. Simul., 21, 1-3, 52-69 (2015) · Zbl 1401.03110 · doi:10.1016/j.cnsns.2014.06.052 |
| [34] | Nagel, E.; Newman, JR; Hofstadter, D., Gödel’s proof (2001), NY: New York University Press, NY · Zbl 1101.03300 |
| [35] | Pelayo, A.; Warren, M., Homotopy type theory and Voevodsky’s univalent foundations, Bull. Am. Math. Soc, 51, 597-648 (2014) · Zbl 1432.03019 · doi:10.1090/S0273-0979-2014-01456-9 |
| [36] | Rasekh, N.: A theory of elementary higher toposes, arxiv: 1805.03805 (2018) |
| [37] | Riehl, E., Verity, D.: Elements of \(\infty \)-category theory. Preprint available at www.math.jhu.edu/eriehl/elements.pdf (2018) · Zbl 1492.18001 |
| [38] | Rizza, D., A study of mathematical determination through Bertrand’s Paradox, Philos. Math., 26, 375-395 (2018) · Zbl 1423.60008 · doi:10.1093/philmat/nkx035 |
| [39] | Rizza, D., Numerical Methods for Infinite Decision-making Processes, Int. J. Unconv. Comput., 14, 139-158 (2019) |
| [40] | Sergeyev, Y., Blinking fractals and their quantitative analysis using infinite and infinitesimal numbers, Chaos Solitons Fractals, 33, 50-75 (2007) · doi:10.1016/j.chaos.2006.11.001 |
| [41] | Sergeyev, Y., A new applied approach for executing computations with infinite and infinitesimal quantities, Informatica, 19, 567-596 (2008) · Zbl 1178.68018 · doi:10.15388/Informatica.2008.231 |
| [42] | Sergeyev, YD, Computer System for Storing Infinite, Infinitesimal, and Finite Quantities and Executing Arithmetical Operations with Them, USA Patent, 7, 860, 914 (2010) |
| [43] | Sergeyev, Y.: Arithmetic of Infinity. Edizioni Orizzonti Meridionali, 2nd edition (2013) |
| [44] | Sergeyev, YD, Solving Ordinary Differential Equations by Working with Infinitesimals Numerically on the Infinity Computer, Appl. Math. Comput., 219, 22, 10668-10681 (2013) · Zbl 1303.65061 · doi:10.1016/j.amc.2013.04.019 |
| [45] | Sergeyev, Y., Numerical Infinities and Infinitesimals: Methodology, Applications, and Repercussions on Two Hilbert Problems, EMS Surv. Math. Sci., 4, 219-320 (2017) · Zbl 1390.03048 · doi:10.4171/EMSS/4-2-3 |
| [46] | Sergeyev, Y.; Garro, A., Observability of Turing machines: A Refinement of the Theory of Computation, Informatica, 21, 425-454 (2010) · Zbl 1209.68255 · doi:10.15388/Informatica.2010.298 |
| [47] | Sergeyev, Y.; Garro, A., Single Tape and Multi-Tape Turing Machines through the Lens of the Grossone Methodology, J. Supercomput., 65, 645-663 (2013) · doi:10.1007/s11227-013-0894-y |
| [48] | Sergeyev, Y.; Kvasov, D.; Mukhametzhanov, M., On Strong Homogeneity of a Class of Global Optimization Algorithms Working with Infinite and Infinitesimal Scales, Commun. Nonlinear Sci. Numer. Simul., 59, 319-330 (2018) · Zbl 1510.90292 · doi:10.1016/j.cnsns.2017.11.013 |
| [49] | Shulman, M.: All \((\infty , 1) \)-toposes Have Strict Univalent Universes. arXiv:1904.07004 (2019) |
| [50] | Streicher, T., Semantics of Type Theory: Correctness, Completeness and Independence (2012), Germany: Springer, Germany · Zbl 0790.68068 |
| [51] | Uemura, T.: Homotopies for Free!. arXiv preprint arXiv:1701.07937 (2017) |
| [52] | The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, http://homotopytypetheory.org/book/ (2013) · Zbl 1298.03002 |
| [53] | Voevodsky, V.: The Origins and Motivations of Univalent Foundations: A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes. IDEAS, The Institute Letter, Summer 2014. Institute of Advanced Study https://www.ias.edu/ideas/2014/voevodsky-origins (2014) |
| [54] | Williams, N., On Grothendieck Universes, Compos. Math., 21, 1-3 (1969) · Zbl 0175.00701 |
| [55] | Zhigljavsky, A., Computing sums of conditionally convergent and divergent series using the concept of Grossone, Appl. Math. Comput., 218, 8064-8076 (2012) · Zbl 1254.03123 · doi:10.1016/j.amc.2011.12.034 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
