GitHub repository: Jlh18/discrete_fibrations
Primary language: Lean
Description: Here we compare the definitions of the category of presheaves as discrete fibrations and as functors into the universe