Fibred categories stand out as a pivotal concept within category theory and its application in algebraic geometry, relative topos theory, and categorical logic. Technical challenges with handling the equality of objects and functors in Lean pose formalization hurdles to the standard definition of Grothendieck fibration. I shall discuss different approaches to respond to these challenges. I will also highlight the pros and cons of each approach and explain the reasons for preferring the displayed categories [1] approach as formalized in [2]. Finally, I outline the next steps towards a Lean formalization of fibrational semantics [3] of type theory.

[1]: Benedikt Ahrens, Peter LeFanu Lumsdaine, Displayed Categories, Logical Methods in Computer Science 15 (1), https://arxiv.org/abs/1705.04296

[2]: Sina Hazratpour, A Lean4 Formalization of Fibred Categories, https://github.com/sinhp/LeanFibredCategories/tree/master

[3]: Bart Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.