andrei rodin Andrei Rodin's blog about History and Philosophy of Mathematics

April 24, 2019

Directed Homotopy Type Theory and the (In)vertibility of Mathematics

Filed under: Uncategorized — Andrei Rodin @ 12:22 pm

Speaker: Andrei Rodin, Russian Academy of Sciences

When: Wednesday April 24, 2019, 7:00 – 8:30 PM.

Where: Graduate Centre CUNY, (365 5th Ave, New York, NY 10016), room 6417


Directed Homotopy Type theory (DHTT) is a generalization of Homotopy Type theory (HoTT) where fundamental groupoids of spaces are replaced by more general (higher) categories. Along with type formers for identity types which admit the standard HoTT interpretation in terms of invertible paths and their homotopies, DHTT comprises type formers for non-invertable homomorphisms of all levels which admit an interpreation in terms of non-invertable paths in appropriate spaces. The choice between DHTT and HoTT as foundational formal frameworks for building mathematical theories has an epistemological dimension, which concerns the epistemic significance of the invertibility condition. While HoTT and the related notion of Univalent Foundations support Mathematical Structuralism DHTT supports a more dynamic conception of Mathematics, which I shall outline in my talk. 


Powered by WordPress