Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics (...) might be expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the ‘HoTT Book’. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous since it explicitly depends upon other fields of mathematics, in particular homotopy theory. We give an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory. 1 Introduction2 What Is a Foundation for Mathematics? 2.1 A characterization of a foundation for mathematics 2.2 Autonomy3 The Basic Features of Homotopy Type Theory 3.1 The rules 3.2 The basic ways to construct types 3.3 Types as propositions and propositions as types 3.4 Identity 3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types 5.1 Tokens as mathematical objects? 5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy 7.1 Framework 7.2 Semantics 7.3 Metaphysics 7.4 Epistemology 7.5 Methodology8 Possible Objections to this Account 8.1 A constructive foundation for mathematics? 8.2 What are concepts? 8.3 Isn’t this just Brouwerian intuitionism? 8.4 Duplicated objects 8.5 Intensionality and substitution salva veritate9 Conclusion 9.1 Advantages of this foundation. (shrink)

For time-independent fields the Aharonov-Bohm effect has been obtained by idealizing the coordinate space as multiply-connected and using representations of its fundamental homotopy group to provide information on what is physically identified as the magnetic flux. With a time-dependent field, multiple-connectedness introduces the same degree of ambiguity; by taking into account electromagnetic fields induced by the time dependence, full physical behavior is again recovered once a representation is selected. The selection depends on a single arbitrary time (hence the so-called (...) holonomies are not unique), although no physical effects depend on the value of that particular time. These features can also be phrased in terms of the selection of self-adjoint extensions, thereby involving yet another question that has come up in this context, namely, boundary conditions for the wave function. (shrink)

Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might (...) be expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the ‘HoTT Book’. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous since it explicitly depends upon other fields of mathematics, in particular homotopy theory. We give an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory, and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory. 1 Introduction2 What Is a Foundation for Mathematics?2.1 A characterization of a foundation for mathematics2.2 Autonomy3 The Basic Features of Homotopy Type Theory3.1 The rules3.2 The basic ways to construct types3.3 Types as propositions and propositions as types3.4 Identity3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types5.1 Tokens as mathematical objects?5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy7.1 Framework7.2 Semantics7.3 Metaphysics7.4 Epistemology7.5 Methodology8 Possible Objections to this Account8.1 A constructive foundation for mathematics?8.2 What are concepts?8.3 Isn’t this just Brouwerian intuitionism?8.4 Duplicated objects8.5 Intensionality and substitution salva veritate9 Conclusion9.1 Advantages of this foundation. (shrink)

Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy provides a reasonably gentle introduction to this new logic, thoroughly motivated by intuitive explanations of the need for all of its component parts, and illustrated through innovative applications of the calculus.

Homotopy Type Theory is a proposed new language and foundation for mathematics, combining algebraic topology with logic. An important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory's types, tokens, and identities as spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. In this paper we give a derivation of path (...) induction, motivated from pre-mathematical considerations, without recourse to homotopy theory. (shrink)

I explore the possibility of a structuralist interpretation of homotopy type theory (HoTT) as a foundation for mathematics. There are two main aspects to HoTT's structuralist credentials. First, it builds on categorical set theory (CST), of which the best-known variant is Lawvere's ETCS. I argue that CST has merit as a structuralist foundation, in that it ascribes only structural properties to typical mathematical objects. However, I also argue that this success depends on the adoption of a strict typing system (...) which undermines the metaphysical seriousness of this structuralism. Homotopy type theory adds to CST a distinctive theory of identity between sets, which arguably allows its objects to be seen as ante rem structures. I examine the prospects for such a view, and address many other interpretive problems as they arise. (shrink)

Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11, 12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical (...) logic, inspired by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature. This paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in [20]. (shrink)

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

Drawing on the analogy between any unary first-order quantifier and a "face operator," this paper establishes several connections between model theory and homotopy theory. The concept of simplicial set is brought into play to describe the formulae of any first-order language L, the definable subsets of any L-structure, as well as the type spaces of any theory expressed in L. An adjunction result is then proved between the category of o-minimal structures and a subcategory of the category of linearly (...) ordered simplicial sets with distinguished vertices. (shrink)

Among the most interesting features of Homotopy Type Theory is the way it treats identity, which has various unusual characteristics. We examine the formal features of “identity types” in HoTT, and how they relate to its other features including intensionality, constructive logic, the interpretation of types as concepts, and the Univalence Axiom. The unusual behaviour of identity types might suggest that they be reinterpreted as representing indiscernibility. We explore this by defining indiscernibility in HoTT and examine its relationship with (...) identity. We argue that identity types are a primitive component of HoTT and cannot be reduced to indiscernibility. (shrink)

In [E. Baro, M. Otero, On o-minimal homotopy, Quart. J. Math. 15pp, in press ] o-minimal homotopy was developed for the definable category, proving o-minimal versions of the Hurewicz theorems and the Whitehead theorem. Here, we extend these results to the category of locally definable spaces, for which we introduce homology and homotopy functors. We also study the concept of connectedness in -definable groups — which are examples of locally definable spaces. We show that the various concepts (...) of connectedness associated to these groups, which have appeared in the literature, are non-equivalent. (shrink)

The Hole Argument is primarily about the meaning of general covariance in general relativity. As such it raises many deep issues about identity in mathematics and physics, the ontology of space–time, and how scientific representation works. This paper is about the application of a new foundational programme in mathematics, namely homotopy type theory, to the Hole Argument. It is argued that the framework of HoTT provides a natural resolution of the Hole Argument. The role of the Univalence Axiom in (...) the treatment of the Hole Argument in HoTT is clarified. (shrink)

An appropriate framework is put forward for the construction of $$\lambda $$ -models with $$\infty $$ -groupoid structure, which we call homotopic $$\lambda $$ -models, through the use of an $$\infty $$ -category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $$\lambda $$ -calculus, in the sense that the concept of proof (path) of equality of $$\lambda $$ -terms is raised to higher proof (homotopy).

The Univalence axiom, due to Vladimir Voevodsky, is often taken to be one of the most important discoveries arising from the Homotopy Type Theory research programme. It is said by Steve Awodey that Univalence embodies mathematical structuralism, and that Univalence may be regarded as ‘expanding the notion of identity to that of equivalence’. This article explores the conceptual, foundational and philosophical status of Univalence in Homotopy Type Theory. It extends our Types-as-Concepts interpretation of HoTT to Universes, and offers (...) an account of the Univalence axiom in such terms. We consider Awodey’s informal argument that Univalence is motivated by the principle that reasoning should be invariant under isomorphism, and we examine whether an autonomous and rigorous justification along these lines can be given. We consider two problems facing such a justification. First, there is a difference between equivalence and isomorphism and Univalence must be formulated in terms of the former. Second, the argument as presented cannot establish Univalence itself but only a weaker version of it, and must be supplemented by an additional principle. The article argues that the prospects for an autonomous justification of Univalence are promising. (shrink)

Let T be the theory of dense cyclically ordered sets with at least two elements. We determine the classifying space of $\mathsf {Mod}(T)$ to be homotopically equivalent to $\mathbb {CP}^\infty $. In particular, $\pi _2(\lvert \mathsf {Mod}(T)\rvert )=\mathbb {Z}$, which answers a question in our previous work. The computation is based on Connes’ cycle category $\Lambda $.

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π, and intensional identity types Id, as used in (...) homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: they should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory. (shrink)

of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also has dependent types x : (...) A B(x), which are regarded as indexed families of types. There are simple type forming operations A × B and A → B, as well as operations on dependent types, including in particular the sum x:A B(x) and product x:A B(x) types (see the appendix for details). The Curry-Howard interpretation of the operations A × B and A → B is as propositional conjunction and.. (shrink)

1. The theory referred to by the—perhaps intimidating—main title of this book is an extension of Per Martin-Löf's dependent type theory. Much philosophical work pertaining to dependent type theory...

As a new foundational language for mathematics with its very different idea as to the status of logic, we should expect homotopy type theory to shed new light on some of the problems of philosophy which have been treated by logic. In this article, definite description, and in particular its employment within mathematics, is formulated within the type theory. Homotopy type theory has been proposed as an inherently structuralist foundational language for mathematics. Using the new formulation of definite (...) descriptions, opportunities to express ‘the structure of’ within homotopy type theory are explored, and it is shown there is little or no need for this expression. (shrink)

In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.

The original article has been corrected. The article is published with Open Access but was missing Open Access information. This has been added.

In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.

The aim of the present thesis is twofold. First we propose a constructive solution to Frege's puzzle using an approach based on homotopy type theory, a newly proposed foundation of mathematics that possesses a higher-dimensional treatment of equality. We claim that, from the viewpoint of constructivism, Frege's solution is unable to explain the so-called ‘cognitive significance' of equality statements, since, as we shall argue, not only statements of the form 'a = b', but also 'a = a' may contribute (...) to an extension of knowledge. Second, we study this higher-dimensional account of equality from a constructive (computational) standpoint and, based on these considerations, we offer a new perspective to the project proposed by Peter Aczel of developing conventions and notations for an informal style of doing mathematics in type theory. To that end, we adopt the cubical type theory of Angiuli, Favonia and Harper, a framework that can be seen as constructive refinement of the ideas of homotopy type theory. (shrink)

In this paper, I introduce the idea that some important parts of contemporary pure mathematics are moving away from what I call the extensional point of view. More specifically, these fields are based on criteria of identity that are not extensional. After presenting a few cases, I concentrate on homotopy theory where the situation is particularly clear. Moreover, homotopy types are arguably fundamental entities of geometry, thus of a large portion of mathematics, and potentially to all mathematics, at (...) least according to some speculative research programs. (shrink)

We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from [8] that any Grothendieck fibration of the kind being considered can automatically be upgraded to a two-dimensional fibration, after which the invariance property is (...) reduced to an abstract theorem concerning pseudonatural transformations of morphisms into two-dimensional fibrations. (shrink)

This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our (...) presentation to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman–Hilton duality. (shrink)

A novel conceptual framework is introduced for the Complexity Levels Theory in a Categorical Ontology of Space and Time. This conceptual and formal construction is intended for ontological studies of Emergent Biosystems, Super-complex Dynamics, Evolution and Human Consciousness. A claim is defended concerning the universal representation of an item’s essence in categorical terms. As an essential example, relational structures of living organisms are well represented by applying the important categorical concept of natural transformations to biomolecular reactions and relational structures that (...) emerge from the latter in living systems. Thus, several relational theories of living systems can be represented by natural transformations of organismic, relational structures. The ascent of man and other living organisms through adaptation, is viewed in novel categorical terms, such as variable biogroupoid representations of evolving species. Such precise but flexible evolutionary concepts will allow the further development of the unifying theme of local-to-global approaches to highly complex systems in order to represent novel patterns of relations that emerge in super- and ultra-complex systems in terms of compositions of local procedures. Solutions to such local-to-global problems in highly complex systems with ‘broken symmetry’ might be possible to be reached with the help of higher homotopy theorems in algebraic topology such as the generalized van Kampen theorems (HHvKT). Categories of many-valued, Łukasiewicz-Moisil (LM) logic algebras provide useful concepts for representing the intrinsic dynamic ‘asymmetry’ of genetic networks in organismic development and evolution, as well as to derive novel results for (non-commutative) Quantum Logics. Furthermore, as recently pointed out by Baianu and Poli (Theory and applications of ontology, vol 1. Springer, Berlin, in press), LM-logic algebras may also provide the appropriate framework for future developments of the ontological theory of levels with its complex/entangled/intertwined ramifications in psychology, sociology and ecology. As shown in the preceding two papers in this issue, a paradigm shift towards non-commutative, or non-Abelian, theories of highly complex dynamics—which is presently unfolding in physics, mathematics, life and cognitive sciences—may be implemented through realizations of higher dimensional algebras in neurosciences and psychology, as well as in human genomics, bioinformatics and interactomics. (shrink)

Homotopy type theory is a new branch of mathematics that connects algebraic topology with logic and computer science, and which has been proposed as a new language and conceptual framework for math- ematical practice. Much of the power of HoTT lies in the correspondence between the formal type theory and ideas from homotopy theory, in par- ticular the interpretation of types, tokens, and equalities as spaces, points, and paths. Fundamental to the use of identity and equality in HoTT (...) is the powerful proof technique of path induction. In the ‘HoTT Book’ this principle is justified through the homotopy interpretation of type theory, by treating identifications as paths and the induction step as a homotopy between paths. This is incompatible with HoTT being an au- tonomous foundation for mathematics, since any such foundation must be able to justify its principles without recourse to existing areas of mathemat- ics. In this paper it is shown that path induction can be motivated from pre-mathematical considerations, and in particular without recourse to ho- motopy theory. This makes HoTT a candidate for being an autonomous foundation for mathematics. (shrink)

I apply homotopy type theory to the hole argument as formulated by Earman and Norton. I argue that HoTT gives a precise sense in which diffeomorphism-related Lorentzian manifolds represent the same spacetime, undermining Earman and Norton’s verificationist dilemma and common formulations of the hole argument. However, adopting this account does not alleviate worries about determinism: general relativity formulated on Lorentzian manifolds is indeterministic using this standard of sameness and the natural formalization of determinism in HoTT. Fixing this indeterminism results (...) in a more faithful mathematical representation of general relativity as used by physicists. It also gives a substantive notion of general covariance. (shrink)

0. The ancient and honorable role of philosophy as a servant to the learning, development and use of scientific knowledge, though sadly underdeveloped since Grassmann, has been re-emerging from within the particular science of mathematics due to the latter's internal need; making this relationship more explicit (as well as further investigating the reasons for the decline) will, it is hoped, help to germinate the seeds of a brighter future for philosophy as well as help to guide the much wider learning (...) of mathematics and hence of all the sciences. 1. The unity of interacting opposites "space vs. quantity", with the accompanying "general vs. particular" and the resulting division of variable quantity into the interacting opposites "extensive vs. intensive", is susceptible, with the aid of categories, functors, and natural transformations, of a formulation which is on the one hand precise enough to admit proved theorems and considerable technical development and yet is on the other hand general enough to admit incorporation of almost any specialized hypothesis. Readers armed with the mathematical definitions of basic category theory should be able to translate the discussion in this section into symbols and diagrams for calculations. 2. The role of space as an arena for quantitative "becoming" underlies the qualitative transformation of a spatial category into a homotopy category, on which extensive and intensive quantities reappear as homology and cohomology. 3. The understanding of an object in a spatial category can be approached through definite Moore-Postnikov levels; each of these levels constitutes a mathematically precise "unity and identity of opposites", and their ensemble bears features strongly reminiscent of Hegel's Science of Logic. This resemblance suggests many mathematical and philosophical problems which now seem susceptible of exact solution. (shrink)

In this paper, we try to establish that some mathematical theories, like K-theory, homology, cohomology, homotopy theories, spectral sequences, modern Galois theory (in its various applications), representation theory and character theory, etc., should be thought of as (abstract) machines in the same way that there are (concrete) machines in the natural sciences. If this is correct, then many epistemological and ontological issues in the philosophy of mathematics are seen in a different light. We concentrate on one problem which immediately (...) follows the recognition of the particular status of these theories: the demarcation problem between ‘natural kinds’ and ‘artefacts’. (shrink)

We prove that the unification type of Łukasiewicz logic and of its equivalent algebraic semantics, the variety of MV-algebras, is nullary. The proof rests upon Ghilardiʼs algebraic characterisation of unification types in terms of projective objects, recent progress by Cabrer and Mundici in the investigation of projective MV-algebras, the categorical duality between finitely presented MV-algebras and rational polyhedra, and, finally, a homotopy-theoretic argument that exploits lifts of continuous maps to the universal covering space of the circle. We discuss the (...) background to such diverse tools. In particular, we offer a detailed proof of the duality theorem for finitely presented MV-algebras and rational polyhedra—a fundamental result that, albeit known to specialists, seems to appear in print here for the first time. (shrink)

We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy (...) type as the free groupoid generated by G. (shrink)

Ladyman and Presnell have recently argued that the Hole argument is naturally resolved when spacetime is represented within homotopy type theory rather than set theory. The core idea behind their proposal is that the argument does not confront us with any indeterminism, since the set-theoretically different representations of spacetime involved in the argument are homotopy type-theoretically identical. In this article, we will offer a new resolution based on ZFC set theory to the argument. It neither relies on a (...) constructive-intuitionistic form of mathematics, as used by Ladyman and Presnell, nor is foundationally problematic, such as the existing set-theoretic suggestions. (shrink)

We review the issues of nonseparability and seemingly acausal propagation of information in EPR, as displayed by experiments and the failure of Bell's inequalities. We show that global effects are in the very nature of the geometric structure of modern physical theories, occurring even at the classical level. The Aharonov-Bohm effect, magnetic monopoles, instantons, etc. result from the topology and homotopy features of the fiber bundle manifolds of gauge theories. The conservation of probabilities, a supposedly highly quantum effect, is (...) also achieved through global geometry equations. The EPR observables all fit in such geometries, and space-time is a truncated representation and is not the correct arena for their understanding. Relativistic quantum field theory represents the global action of the measurement operators as the zero-momentum (and therefore spatially infinitely spread) limit of their wave functions (form factors). We also analyze the collapse of the state vector as a case of spontaneous symmetry breakdown in the apparatus-observed state interaction. (shrink)

We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category EFF. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category EFF one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in (...) other words, this class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets. (shrink)

A novel conceptual framework is introduced for the Complexity Levels Theory in a Categorical Ontology of Space and Time. This conceptual and formal construction is intended for ontological studies of Emergent Biosystems, Super-complex Dynamics, Evolution and Human Consciousness. A claim is defended concerning the universal representation of an item’s essence in categorical terms. As an essential example, relational structures of living organisms are well represented by applying the important categorical concept of natural transformations to biomolecular reactions and relational structures that (...) emerge from the latter in living systems. Thus, several relational theories of living systems can be represented by natural transformations of organismic, relational structures. The ascent of man and other living organisms through adaptation, is viewed in novel categorical terms, such as variable biogroupoid representations of evolving species. Such precise but flexible evolutionary concepts will allow the further development of the unifying theme of local-to-global approaches to highly complex systems in order to represent novel patterns of relations that emerge in super- and ultra-complex systems in terms of compositions of local procedures. Solutions to such local-to-global problems in highly complex systems with ‘broken symmetry’ might be possible to be reached with the help of higher homotopy theorems in algebraic topology such as the generalized van Kampen theorems (HHvKT). Categories of many-valued, Łukasiewicz-Moisil (LM) logic algebras provide useful concepts for representing the intrinsic dynamic ‘asymmetry’ of genetic networks in organismic development and evolution, as well as to derive novel results for (non-commutative) Quantum Logics. Furthermore, as recently pointed out by Baianu and Poli (Theory and applications of ontology, vol 1. Springer, Berlin, in press), LM-logic algebras may also provide the appropriate framework for future developments of the ontological theory of levels with its complex/entangled/intertwined ramifications in psychology, sociology and ecology. As shown in the preceding two papers in this issue, a paradigm shift towards non-commutative, or non-Abelian, theories of highly complex dynamics—which is presently unfolding in physics, mathematics, life and cognitive sciences—may be implemented through realizations of higher dimensional algebras in neurosciences and psychology, as well as in human genomics, bioinformatics and interactomics. (shrink)

The phrase ‘mathematical foundation’ has shifted in meaning since the end of the nineteenth century. It used to mean a consistent general theory in mathematics, based on basic principles and ideas to which the rest of mathematics could be reduced. There was supposed to be only one foundational theory and it was to carry the philosophical weight of giving the ultimate ontology and truth of mathematics. Under this conception of ‘foundation’ pluralism in foundations of mathematics is a contradiction.More recently, the (...) phrase has come to mean a perspective from which we can see, or in which we can interpret, much of mathematics; it has lost the realist-type metaphysical, essentialist importance. The latter has been replaced with an emphasis on epistemology. The more recent use of the phrase shows a lack of concern for absolute ontology, truth, uniqueness and sometimes even consistency. It is only under the more modern conception of ‘foundation’ that pluralism in mathematical foundations is conceptually possible.Several problems beset the pluralist in mathematical foundations. The problems include, at least: paradox, rampant relativism, loss of meaning, insurmountable complexity and a rising suspicion that we can say anything meaningful about truth and objectivity in mathematics. Many of these are related to each other, and many can be overcome, explained, accounted for and dissolved by concentrating on crosschecking, fixtures and rigour of proof. Moreover, apart from being a defensible position, there are a lot of advantages to pluralism in foundations. These include: a sensitivity to the practice of mathematics, a more faithful account of the objectivity of mathematics and a deeper understanding of mathematics.The claim I defend in the paper is that we stand to learn more, not less, by adopting a pluralist attitude. I defend the claim by looking at the examples of set theory and homotopy type theory, as alternative viewpoints from which we can learn about mathematics. As the claim is defended, it will become apparent that ‘pluralism in mathematical foundations’ is neither an oxymoron, nor a contradiction, at least not in any threatening sense. On the contrary, it is the tension between different foundations that spurs new developments in mathematics. The tension might be called ‘a fruitful meta-contradiction’.I take my prompts from Kauffman’s idea of eigenform, Hersh’s idea of thinking of mathematical theories as models and from my own philosophical position: pluralism in mathematics. I also take some hints from the literature on philosophy of chemistry, especially the pluralism of Chang and Schummer. (shrink)

The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inference rules, which can be interpreted by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, (...) known as $ D_{\infty }$, to represent the $\lambda $-terms as the typical functions of set theory, where it is not allowed to apply a function to itself. Here we propose a construction of an $\infty $-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case $D_{\infty }$, and we see that the Scott topology does not provide enough information about the relationship between higher homotopies. This motivates a new line of research focused on the exploration of $\lambda $-models with the structure of a non-trivial $\infty $-groupoid to generalize the proofs of term conversion to higher-proofs in $\lambda $-calculus. (shrink)

We develop an intersection theory for definable Cp-manifolds in an o-minimal expansion of a real closed field and we prove the invariance of the intersection numbers under definable Cp-homotopies . In particular we define the intersection number of two definable submanifolds of complementary dimensions, the Brouwer degree and the winding numbers. We illustrate the theory by deriving in the o-minimal context the Brouwer fixed point theorem, the Jordan-Brouwer separation theorem and the invariance of the Lefschetz numbers under definable Cp-homotopies. A. (...) Pillay has shown that any definable group admits an abstract manifold structure. We apply the intersection theory to definable groups after proving an embedding theorem for abstract definably compact Cp-manifolds. In particular using the Lefschetz fixed point theorem we show that the Lefschetz number of the identity map on a definably compact group, which in the classical case coincides with the Euler characteristic, is zero. (shrink)