Here is a partial answer for how Lean 3 handles it, but you probably want to wait for a person in Lean with more knowledge of the category theory library to confirm that my understanding is fully accurate.
Here is the Yoneda lemma in Lean's mathlib. In particular the documenation says
The Yoneda lemma asserts that that the Yoneda pairing (X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F) is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.
As you can see (if I understand correctly), the type
Type is used in place of the category
Set to refer to the presheafs
Cᵒᵖ ⥤ Type. This might seem weird (and I'm not an expert), but let me explain.
The first thing to keep in mind is that in Lean types behave as sets. Informally, I mean that equality of objects in a Lean type is nothing special. If
a=b then there is only one way for them to be equal.
This can be made formal with homotopy type theory, via a formal definition of what it means for a type to be a "set" (or h-set ). So from a category theory standpoint, in Lean, the type
Type plays the same role as the category
Set of small sets.
Type is not technically a category, but it is a Type universe which is itself a type in the universe
Type 1. This is a common situation in Lean, just as the type
real of real numbers is not a topological space, but just a type. So how do we give
Type it's canonical categorical structure (just like we give
Real its canonical topological space structure)? We do this through type classes. So when Lean sees
Cᵒᵖ ⥤ Type (the functors from
Type) it looks up the instance of the
category typeclass for
Type to turn
Type into a category. I didn't trace though exact the route it does this, but I'm sure it is the usual category structure of Set, i.e. the morphisms from
A: Type to
B: Type are exactly the elements of the "hom" type
A -> B in Lean (which again is an element of
Type in Lean, and that is the requirement of the Yoneda lemma as stated in Trebor’s answer).
Third, you asked about internal logic. I'm not great with this either, but my loose intuition is that the logic of Lean when restricted to types in
Type is the internal logic of the category
Set (and when you add the sort
Prop of propositions then you get the internal logic of the topos
Set). So normal math in Lean uses category theoretical ideas implicitly and internally. But since Lean has universes, you can explicitly refer to
Type externally as an object of a higher universe
Type 1, and you can explicitly talk about the categorical structure of Type as well. That is exactly what the mathlib category theory library does, especially its formulation of the Yoneda lemma.
Last, I've only talked about Lean which has built in that all types are sets. I imagine if working in HoTT or cubical type theory in Adga, Coq, or Arend, that you can do the same thing, but in that case, one doesn't use the type
Type of all small types, but instead the type of all small
h-sets (or maybe its truncation to an
h-set to prevent it from becoming a higher category). Indeed in the HoTT book there is a type
Set of small sets and it plays the same role as the category of
Set. The HoTT version of the Yoneda lemma is Theorem 9.5.4 in the book (and I don't think it requires that Set satisfies the axiom of choice). Also, here is the Agda Yoneda lemma which appears to use the category of setoids.
For higher order logic, which is another type theoretic foundation used in HOL Light and Isabelle/HOL, there are not universes, so I think one can't show the category
Set exists. Anyway, here is the Yoneda Lemma in Isabelle's Archive of Formal Proofs, but I'll leave it up to someone else to explain how it works.
You can find more about the Lean category theory library by reading the documentation for the Lean category theory library, watching the videos for Lean for the Curious Mathematician 2020 (or LFTCM 2022 coming this week!) which cover category theory, or doing the category theory exercises for LFTCM 2020. Note that Lean moves quickly (and breaks things) so some of these references may be out of date.