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)

This paper compares the statement ‘Mathematics is the study of structure’ with the actual practice of mathematics. We present two examples from contemporary mathematical practice where the notion of structure plays different roles. In the first case a structure is defined over a certain set. It is argued firstly that this set may not be regarded as a structure and secondly that what is important to mathematical practice is the relation that exists between the structure and the set. In the (...) second case, from algebraic topology, one point is that an object can be a place in different structures. Which structure one chooses to place the object in depends on what one wishes to do with it. Overall the paper argues that mathematics certainly deals with structures, but that structures may not be all there is to mathematics. (shrink)

Category Theory has developed rapidly. This book aims to present those ideas and methods which can now be effectively used by Mathe­ maticians working in a variety of other fields of Mathematical research. This occurs at several levels. On the first level, categories provide a convenient conceptual language, based on the notions of category, functor, natural transformation, contravariance, and functor category. These notions are presented, with appropriate examples, in Chapters I and II. Next comes the fundamental idea of an adjoint (...) pair of functors. This appears in many substantially equivalent forms: That of universal construction, that of direct and inverse limit, and that of pairs offunctors with a natural isomorphism between corresponding sets of arrows. All these forms, with their interrelations, are examined in Chapters III to V. The slogan is "Adjoint functors arise everywhere". Alternatively, the fundamental notion of category theory is that of a monoid -a set with a binary operation of multiplication which is associative and which has a unit; a category itself can be regarded as a sort of general­ ized monoid. Chapters VI and VII explore this notion and its generaliza­ tions. Its close connection to pairs of adjoint functors illuminates the ideas of universal algebra and culminates in Beck's theorem characterizing categories of algebras; on the other hand, categories with a monoidal structure lead inter alia to the study of more convenient categories of topological spaces. (shrink)

. This paper identifies two aspects of the structuralist position of S. Shapiro which are in conflict with the actual practice of mathematics. The first problem follows from Shapiros identification of isomorphic structures. Here I consider the so called K-group, as defined by A. Grothendieck in algebraic geometry, and a group which is isomorphic to the K-group, and I argue that these are not equal. The second problem concerns Shapiros claim that it is not possible to identify objects in a (...) structure except through the relations and functions that are defined on the structure in which the object has a place. I argue that, in the case of the definition of the so called direct image of a function, it is possible to individuate objects in structures. (shrink)