Role of `Type` in the Yoneda lemma in Lean

Stream: general

[Jason Rute]

On the Proof Assistant Stack exchange someone asked about the replacement of the category Set in the Yoneda Lemma when formalizing it in type theory. I tried (possibly incorrectly) to explain how it is done in Lean using Type instead of Set. If anyone wants to look over my answer or give their own more correct answer, feel free: https://proofassistants.stackexchange.com/questions/1584/how-are-the-parts-of-category-theory-which-make-explicit-reference-to-set-differ