Function types in the category of all Lean types

Stream: general

[Arnav Sabharwal]

If we considered the category of all Lean types, how would we interpret function types? Would we differentiate between a morphism from 'a' to 'b' and the function type 'a -> b'? Thanks!

[Johan Commelin]

In this case, a morphism from a to b is by definition a term of the function type a -> b.
When defining a category in Lean, you have to specify the Hom-sets, and in this case they are defined to be the function types.