Formalization of Infinity Category Theory

Explore a comprehensive lecture on the formalization of ∞ category theory presented by Jonathan Weinberger from Johns Hopkins University. Delve into the world of category theory and its applications in unifying and translating constructions and theorems across mathematics, computer science, and physics. Learn about the concept of ∞-categories as infinite-dimensional structures that model composition in various settings. Discover the main elements of a formal language for reasoning about ∞-categories in a "synthetic" way, extending homotopy type theory. Gain insights into the Rzk proof assistant that implements this formal language. Examine the Yoneda Lemma, the fundamental theorem of category theory, and its easier proof for ∞-categories in the synthetic setting compared to 1-categories in classical set theory. This talk, part of the Orange County Inland Empire (OCIE) Seminar series in History and Philosophy of Mathematics, offers a deep dive into advanced mathematical concepts and their formalization.

Formalization of ∞ category theory (Jonathan Weinberger, Johns Hopkins University)