Is Lean a Category? (like much debated: is Hask(ell) a Category) "In this section we set up the theory so that Lean's types and functions between them can be

Is Lean a Category? (like much debated: is Hask(ell) a Category) "In this section we set up the theory so that Lean's types and functions between them can be viewed as a `LargeCategory` in our framework." So it seems to be proven that there is a Category Lean! https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Types.lean https://github.com/leanprover-community/mathlib4/blob/master...