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

Wednesdays 7:00 - 8:30 PM.

Room 6417 .

Some of the talks are videoed and available here.

Contact N. Yanofsky to schedule a speaker

or to add a name to the seminar mailing list.

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

The list for announcements and scheduling regarding this group is also at the hott-nyc google group:

https://groups.google.com/forum/#!forum/hott-nyc

We meet the first and third Wednesdays of each month from 7:00 to 8:30 PM in Room 6417. The meetings are run by Gershom Bazerman.

In this talk I introduce an extension of the simply typed λ-calculus which is equivalent to IEL via an extension of the Curry-Howard correspondence. The categorical semantics of the type theory are interesting in that the interpretation of the modality in a syntactic category forms part of a non-idempotent monad. I will then show that by introducing a judgmental equality we transform the monad into an idempotent monad in a quotient category, and that the new monad corresponds to propositional truncation in the new calculus.

This will be an expository talk. All terms will be defined and explained. This is joint work with Jeremy Russell.

This talk is given in conjunction with the Women in Quantum Meetup (NYC). No category theory or quantum mechanics is needed for this talk. The only prerequisite is the ability to multiply two matrices with complex entries.

Related papers:

Paige North, Towards a Directed Homotopy Type Theory, arXiv:1807.10566

Andrei Rodin, Categories Without Structures, arXiv: 0907.5143 (published in Philosophia Mathematica 19/1 (2011), p. 20-46)

Michael Warren, Directed Type Theory (video of talk in IAS Princeton)

THEOREM: A locally anisotropic topos has no higher isotropy. Equivalently, its isotropy quotient is anisotropic. Furthermore, a locally anisotropic topos is recovered as the topos of actions for a connected groupoid internal to its isotropy quotient.

COROLLARY: An etendue, or locally localic topos, has no higher isotropy. An etendue may be recovered as the topos of actions for a connected groupoid internal to its isotropy quotient.

Our argumentation of the theorem brings into focus how isotropy theory and Galois theory for toposes meet in a natural and evidently effective way.

Joint work with Pieter Hofstra.

(1) * can consistency of PA be established by means expressible in PA?*

FT: * any proof by means expressible in PA admits Gödel’s arithmetization.*

Note that the aforementioned negative answer to (1) is unwarranted: here is a counter-example to FT. Let

We provide a positive answer to (1). We offer a mathematical proof of PA-consistency,

*No finite sequence of formulas is a PA-proof of 0=1, *