COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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-categoriesAdd 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
- Computer Laboratory talks
- Computing and Mathematics
- 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. |
## Other listsWolfson Research Event 2017 Cambridge American History Events criminology## Other talksTropical development Making the Most of Massive Clusters Biostatistics for chronic diseases The Arctic at the End of the World: Hannah Arendt and the Narration of Apocalypse All To Play For: How sport can reboot our future The inner inner halo of the Milky Way according to APOGEE and Gaia |