A took given on March 20, 2024 on Zoom.

Abstract: Fibred categories are one of the most important and useful concepts in category theory and its application in categorical logic. In this talk I present my recent formalization of fibred categories in the interactive theorem prover Lean 4. I begin by highlighting certain technical challenges associated with handling the equality of objects and functors within the extensional dependent type system of Lean, and how they can be overcome. In this direction, I will demonstrate how we can take advantage of dependent coercion, instance synthesis, and automation tactics from of the Lean toolbox. Finally I will discuss a formalization of Homotopy Type Theory in Lean 4 using a fired categorical framework.