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...