**The New York City**

**Category Theory Seminar**

**
Department of Computer Science**

Department of Mathematics

The Graduate Center of The City University of New York

365 Fifth Avenue (at 34th Street) map

(Diagonally across from the Empire State Building)

New York, NY 10016-4309

Thursdays 7:00 - 8:30 PM.

Room 6417 .

Contact N. Yanofsky to
schedule a speaker

or to add a name to the
seminar mailing list.

**Fall 2013 - Spring 2015**

The New York Category Theory Seminar and the New York Haskell Meetup is sponsoring a

**Homotopy Type Theory Reading Group**

We will be reading the Homotopy Theory Book
Available here .

We will be meeting roughly every two weeks on Thursdays from 7:00 to 8:30 PM in Room 6417.

The seminar continued through the Spring of 2015 and the Hott book was completed.

Speaker: ** Jean-Pierre Marquis,
Universite de Montreal
.**

Date and Time: ** Thursday April 3, 2014, 7:00 - 8:00 PM., Room 8405.**

Title:** Homotopy type theory as a foundational framework:
some philosophical remarks
. **

Abstract:** Homotopy type theory, a new field at the crossroad of homotopy theory and type theory, is being vigorously investigated and is being presented as a new candidate for the foundations of mathematics. Too many logicians and philosophers, the latter suggestion seems dubitable, to say the least, if only because homotopy types are understood as being too abstract and complicated to provide a convincing foundational framework. In this talk, I will briefly discuss the various desiderata associated with a foundational framework and try to sketch a view that provides a justification for this new approach. **

Speaker: ** Nathan Bouscal.**

Date and Time: ** Thursday March 6, 2014, 7:00 - 8:30 PM., Room 8405.**

Title:** More of Chapter Six. **

Speaker: ** Nathan Bouscal.**

Date and Time: ** Thursday February 6, 2014, 7:00 - 8:30 PM., Room 8405.**

Title:** The Beginning of Chapter Six. **

Speaker: ** Nathan Bouscal.**

Date and Time: ** Thursday January 9, 2014, 7:00 - 8:30 PM., Room 6417.**

Title:** The Beginning of Chapter Three: Sets and Logic. **

Speaker: ** Louis Thrall.**

Date and Time: ** Thursday December 5, 2013, 7:00 - 8:30 PM., Room 6417.**

Title:** The Univalence Axiom. **

Abstract: 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.

Speaker: ** Dustin Mulcahey.**

Date and Time: ** Thursday November 21, 2013, 7:00 - 8:00 PM., Room 6417.**

Title:** An Introduction to Homotopy Theory Part II. **

Speaker: ** Dustin Mulcahey.**

Date and Time: ** Thursday November 7, 2013, 7:00 - 8:30 PM., Room 6417.**

Title:** An Introduction to Homotopy Theory Part I. **

Speaker: ** Perry E. Metzger.**

Date and Time: ** Thursday October 17, 2013, 7:00 - 8:30 PM., Room 6417.**

Title:** An Introduction to Intuitionistic Type Theory. **

Speaker: ** Gershom Bazerman.**

Date and Time: ** Thursday October 3, 2013, 7:00 - 8:30 PM., Room 6417.**

Title:** An Introduction to Intuitionistic Type Theory. **

Abstract:

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.

Speaker: ** Dustin Mulcahey.**

Date and Time: ** Thursday September 12, 2013, 7:00 - 8:30 PM., Room 8405.**

Title:** A General Introduction to Homotopy Type Theory and Orginizational Meeting. **

Abstract:

The reading group is organized by Dustin Mulcahey. 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.