The received notion of axiomatic theory, which stems from Hilbert, is that of set T of propositions (either contentful or non-interpreted aka propositional forms) with subset A of axioms provided with a notion of consequence, which generates T from A in the obvious way. I argue that this standard notion is too narrow for being an adequate theoretical model of many mathematical theories; the class of such counter-examples is apparently very large and it includes such different theories as the geometrical theory of Euclid’s Elements, Book 1, and the more recent Homotopy type theory. In order to fix this problem I introduce a more general notion of theory, which uses typing and a generalized notion of consequence applicable also to objects of other types than propositions. I call such a theory constructive axiomatic theory and show that this particular conception of being constructive indeed captures many important ideas concerning the mathematical constructivity found in the earlier literature from Hilbert to Kolmogorov to Martin-Lof. Finally I provide an epistemological argument intended to show that the notion of constructive axiomatic theory is more apt to be useful in natural sciences and other empirical contexts than the standard notion. Disclaimer: The notion of constructive axiomatic theory is not my invention. The idea and its technical implementation are found in Martin-Lof ‘s constructive type theory if not already in Euclid. My aim is to make this notion explicit and introduce it into the continuing discussions on axiomatic method and mathematical and logical constructivity.

As we continue our foray into the book, we begin to view types as spaces (or, “equivalently”, as omega groupoids). My goal for this section is to focus on the path induction rule and argue that it corresponds to the path-loop fibration.

More specifically, we can make an analogy between the path space over a space X and the type of all equivalences over a type A. The path space of X is homotopy equivalent to X, and I argue that path induction says “essentially the same thing” about the type of all equivalences over A. I aim to make this analogy as formal as possible, and then delve further into the material in chapter 2.

I would also like to go over some exercises. I’ve done a few, but if anyone wants to come up to the board and show off, then they are welcome!

The goal of this group is to study this:
http://homotopytypetheory.org/book/

Homotopy type theory is a new foundation for mathematics based upon type theory and the univalence axiom. This is a topic that unifies the foundations of mathematics, computer science, algebraic topology, and type theory.

Our first meeting will be on Thursday, September 12th at the CUNY Graduate Center, 365 Fifth Ave, NYC. The time will be 7pm and the room is 8405.

The first talk will be given by Dustin Mulcahey, and will consist of an informal overview of the work. We can also take this time to discuss how we should organize the seminar and split up the talks.

We will be meeting (roughly) every two weeks.

Jointly organized by:

New York Haskell Meetup

New York Category Theory Seminar