University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > CaTT, a type-theory to describe weak omega-categories

CaTT, a type-theory to describe weak omega-categories

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jamie Vicary.

The 2000’s have taught us that although mathematicians consider equality as a completely basic notion, and use it everyday without a second thought, a computational approach to (provable) equality is necessarily complicated. Specifically, the identity types that represent equality in Martin-Löf type theory ship with a very intricate algebraic structure called weak omega-groupoids. Several approach have been proposed to handle this complexity, among which is homotopy type theory, whose philosophy is to embrace it, to establish a connection with homotopy theory, another domain where weak omega-groupoids show up. Indeed, those are very complicated to study, and the fact that they appear naturally in weak omega-groupoids are hard to describe and study, and homotopy type theory has provided a concrete way to get a grasp on them. In this talk, I will explore the possibility of repeating the same story, when we replace equality with a (proof-theoretic) notion of rewriting, which can be seen as equality with a prvilidged direction. This is an open problem, for which I will present one step: a description of the corresponding algebraic structure, weak omega-categories, as well as a type theory specifically describe those structure. I will also present a proof-assistant based on this theory and demonstrate how we can use such a tool to gain insight on them.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity