In  this talk, we will begin by discussing application of functions on paths, and the transport lemma (Lemma 2.3.1 of the book). We will then discuss the notion of homotopies, and equivalences, with a few examples. From their we will be able to define a function which will be called “idtoeqv”. Roughly, this function takes equality of types to equivalence of types. This will allow us to state the univalence axiom. If time permits, we will end with how the various type forming constructions behave in the presence of the higher groupoid structure.

Last time we discussed fibrations of sets, spaces, and types. We noted that path induction allows us to prove that the type family of equalities over a given type A is “homotopy equivalent” to A.

This week, we will continue with this and discuss the groupoid structure of spaces (paths) and types (equalities). In doing so, we will establish the “interchange law” for 2-categories, and see that in the particular case of spaces and types that this allows us to prove that the composition law is commutative (up to a higher equivalence) for 2-paths and 2-equivalences that begin and end at the same point.

We shall also discuss how non-dependent functions between types give rise to functors on the associated groupoids of equivalences. This leads to the problem of what to do for dependent functions, and it turns out that fibrations give us a solution to this, and thus we will have come full circle.

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!

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.

This will be the first focused reading of the Homotopy type theory reading group, covering sections 1.1-1.7 of the book. This will serve as an introduction to Intuitionistic Type Theory as developed by Martin-Löf, including notions of decidability and judgmental equality, up through dependent function and pair types (aka Pi and Sigma).

The reading group includes those with type theory background and no homotopy background, with homotopy background but no type theory background, and with no significant background in either but a healthy thirst for knowledge.

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