Blueprint

Stream: Displayed Categories

[Sina Hazratpour 𓃵]

The following Lean blueprint is meant to track the progress on developing the 2-categorical aspects of fibrations via displayed categories.

https://sinhp.github.io/displayed_categories/

[Sina Hazratpour 𓃵]

It is currently minimal, and includes a single file in blueprint/src/chapter, namely displayed.tex which contains two definitions, namely DisplayedStruct and Displayed.

See here:
https://sinhp.github.io/displayed_categories/blueprint/sect0001.html

[Sina Hazratpour 𓃵]

A first task is to write more LaTeX for already existing Lean content in the repository. In particular, we need to create the following files in blueprint/src/chapter

• cartesian.tex corresponding to Cartesian.lean
• fibration.tex corresponding to Fibration.lean