Univalent Higher Categories via Complete Semi-Segal Types

Watch a 26-minute conference presentation from POPL 2018 exploring the mathematical foundations of category theory in homotopy type theory, focusing on complete semi-Segal types as a framework for univalent higher categories. Learn how researchers Paolo Capriotti and Nicolai Kraus from the University of Nottingham address the challenges of expressing categorical laws in homotopy type theory by developing an approach based on simplicial strategy. Discover how their work demonstrates the equivalence between complete semi-Segal n-types and univalent n-categories for n∈{0,1,2}, supported by formalization in the Agda proof assistant. Explore their solution for capturing naturally occurring higher categorical structures that extends beyond the limitations of truncated types used in established univalent category theory.