Chapman University — General Algebra, Logic and Artificial Intelligence Seminar

Marco Giustetto examines how synthetic higher category theory can extend the proof methods of homotopy type theory. Internal reasoning in an infinity-topos can establish classical results about spaces in a form suitable for machine verification. For the next categorical dimension, Riehl and Shulman introduced synthetic (infinity, 1)-categories: simplicial objects satisfying finitely many conditions, whose finiteness brings technical advantages. The talk considers the extension to (infinity, n)-categories, identifying which features of the n = 1 theory survive and which cannot generalize. The work is joint with Lyne Moser and Jonathan Weinberger.