Algebra/Topology seminar

Speaker: Thomas Jan Mikhail

Title: Type Theory for (oo,oo)-Categories

Abstract: Finster and Mimram introduced the type theory CaTT, which gives a type-theoretic description of (oo,oo)-categories. In this talk I will begin by explaining the rules of this type theory. I will then describe a set of alternative rules for CaTT, and present a definition of lax (oo,oo)-limits for finitely generated diagrams in CaTT. No prior knowledge of type theory will be assumed.