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

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

• Thibaut Benjamin, CEA Tech
• Friday 22 October 2021, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.