This one is a little bit more interesting, first let's look at the definition in mathlib:

      class Small (α : Type v) : Prop where
        /-- If a type is `Small.{w}`, 
          then there exists an equivalence with some `S : Type w` -/
        equiv_small : ∃ S : Type w, Nonempty (α ≃ S)

      ...
      class LocallySmall (C : Type u) [Category.{v} C] : Prop where
        /-- A locally small category has small hom-types. -/
        hom_small : ∀ X Y : C, Small.{w} (X ⟶ Y) := by infer_instance
    

So we can see that in lean a locally small category is defined as a normal category with the added property that for every pair of objects \(X, Y \in \mathrm {Ob}\) the hom-type \(X ⟶ Y\) is \(\texttt {Small}\), which as we can see from the definition of \(\texttt {Small}\) means that there exists some type \(\texttt {S : Type w}\) such that there is an equivalence \(α ≃ S\). We can informally correspond to the lean definition as follows:

• Our objects \(\texttt {C : Type u}\) live in some universe level \(u\) which we assoicate with being a class i.e. possibly large collection.
• The morphisms between any two objects \(\texttt {X, Y : C}\) live in some other universe level \(w\) where the equivalence to some type \(\texttt {S : Type w}\) expresses the notion that the hom-sets are small sets.

Honestly I think quite reasonably its fair to ask: wait what how does that represent smallness ? What is \(\texttt {w}\) even supposed to be? So I think an example is warranted.

This is arguably a bit contrived but let's consider objects as being containers for types in some universe level \(0\) i.e. sets. So we can define our objects and morphisms as follows:

      structure TWrapper : Type 1 where
        carrier : Type 0

      /-- Morphisms are functions - each Hom(A,B) is a set -/
      def TWHom (A B : TWrapper) : Type 0 := A.carrier → B.carrier
    

Importantly we can note here that the type of objects \(\texttt {TWrapper : Type 1}\) lives in universe level \(1\) which we can think of as a class of sets. However the morphisms between any two objects \(\texttt {TWHom (A B : TWrapper) : Type 0}\) live in universe level \(0\) which we can think of as small sets. Using this we can define a category instance:

      instance TWrapper.category : Category TWrapper where
        -- The data
        Hom     := TWHom
        id      := fun _ => id
        comp    := 
          fun {X Y Z} (f : TWHom X Y) (g : TWHom Y Z) => fun x => g (f x)

        -- The laws
        id_comp := fun _ => rfl
        comp_id := fun _ => rfl
        assoc := fun _ _ _ => rfl
    

Now we want to define the locally small instance:

      instance TWrapper.locallySmall : LocallySmall.{0} TWrapper where
        hom_small := fun X Y => ⟨⟨TWHom X Y, ⟨Equiv.refl _⟩⟩⟩
    

This now answers a few questions that arose earlier:

• We instantiated the universe level of our hom-sets \(\texttt {w}\) to \(0\) which corresponds to small sets.
• The equivalence \(\texttt {α ≃ S}\) in this case is just the identity equivalence \(\texttt {Equiv.refl}\) since our hom-sets are already small sets. On other words here:

  
          Small.{w} (X ⟶ Y)
        

  We have that \(\texttt {X ⟶ Y}\) represents our set which exists in universe level \(0\), since we are instantiating \(\texttt {w}\) to \(0\) the \(\texttt {Small}\) definition is satisfied by the identity equivalence.

So we can see that in the context of lean a locally small category is just a category where the objects live in some universe level (class) and the hom-sets live in some smaller universe level (set) and we must provide an equivalence showing that the hom-sets are indeed small sets.

We can again examine the definition in mathlib:

      /-- A category is `EssentiallySmall.{w}` if there exists
      an equivalence to some `S : Type w` with `[SmallCategory S]`. -/
      @[pp_with_univ]
      class EssentiallySmall (C : Type u) [Category.{v} C] : Prop where
        /-- An ES category is equivalent to some small category. -/
        equiv_smallCategory : ∃ (S : Type w) (_ : SmallCategory S), Nonempty (C ≌ S)
    

We can see quite nicely here how the lean definition corresponds to the informal one. We have our category \(\texttt {C : Type u}\) living in some universe level \(u\) (class) and we require the existence of some small category \(\texttt {S : Type w}\) living in some smaller universe level \(w\) (set) such that there exists an equivalence \(\texttt {C ≌ S}\).

As an example we will take the categories \(\texttt {FinSet}\) and \(\texttt {FinOrd}\). Starting with the former, the category of finite sets \(\texttt {FinSet}\) is defined as follows:

      /-- Finite sets as a category - objects are Fin n for various n -/
      structure FinSetObj : Type 1 where
        n : ℕ
        carrier : Type 0
        equiv   : carrier ≃ Fin n  -- witness that carrier has exactly n elements

      /-- Morphisms are functions between the carriers -/
      def FSHom (A B : FinSetObj) : Type 0 := A.carrier → B.carrier

      /-- First, we need a Category instance -/
      instance FinSetObj.category : Category FinSetObj where
        Hom     := FSHom
        id      := fun _ => id
        comp    :=
          fun {X Y Z} (f : FSHom X Y) (g : FSHom Y Z) => fun x => g (f x)

        id_comp := fun _ => rfl
        comp_id := fun _ => rfl
        assoc   := fun _ _ _ => rfl
    

It's defined as the category who's objects are finite sets and who's morphisms are functions between said sets. Here we are defining a custom variant of a finite set object \(\texttt {FinSetObj}\) which contains:

• A natural number \(\texttt {n : ℕ}\) representing the cardinality of the set.
• A carrier type \(\texttt {carrier : Type 0}\) representing the actual elements of the set.
• An equivalence \(\texttt {equiv : carrier ≃ Fin n}\) which acts as a witness that the carrier has exactly \(\texttt {n}\) elements.

We then define our morphisms as functions between the carrier types of two finite set objects. Finally we provide a category instance in the standard way.

Next we want to define the category of all finite ordinal numbers \(\texttt {FinOrd}\). This is defined as follows:

      /-- The skeleton: the discrete category on ℕ -/
      abbrev FinSetSkeleton := ℕ

      /-- The skeleton category: 
        objects are ℕ, morphisms are functions between Fin types -/
      structure FinSkel : Type 0 where
        n : ℕ

      instance : SmallCategory FinSkel where
        Hom   := fun A B => Fin A.n → Fin B.n
        id    := fun _ => id
        comp  := fun f g => g ∘ f
    

In our case we can define the finite ordinals as the skeleton of the finite sets category. So our objects are just natural numbers \(\texttt {n : ℕ}\) representing the finite ordinals and our morphisms are functions between the corresponding finite sets \(\texttt {Fin n}\). Again we provide a small category instance in the standard way.

Now central to the definition of an essentially small category is the existence of an equivalence, in other words we need to functors with a natural transformation witnessing the equivalence. We'll start by defining the functor from the finite ordinals to the finite sets:

      /-- Canonical embedding of FinSkel into FinSetObj -/
      def skelToFinSetObj : FinSkel ⥤ FinSetObj where
        obj       := fun A => ⟨A.n, Fin A.n, Equiv.refl _⟩
        map       := fun f => f
        map_id    := fun _ => rfl
        map_comp  := fun _ _ => rfl
    

We can note here that:

• The object mapping takes a finite ordinal \(\texttt {A : FinSkel}\) and maps it to the corresponding finite set object with carrier \(\texttt {Fin A.n}\). The equivalence is just the identity equivalence since \(\texttt {Fin A.n}\) obviously has exactly \(\texttt {A.n}\) elements.
• The morphism mapping is just the identity since morphisms in both categories are functions between finite sets.
• The functor laws are satisfied by reflexivity.

The other way around is a little bit more involved, we can construct the functor as follows:

      def finSetObjToSkel : FinSetObj ⥤ FinSkel where
        obj := fun A => ⟨A.n⟩
        map := fun {A B} f => B.equiv ∘ f ∘ A.equiv.symm
        map_id := fun A => by
          funext x
          show A.equiv ((id : A.carrier → A.carrier) (A.equiv.symm x)) 
            = (id : Fin A.n → Fin A.n) x

          simp only [id_eq, Equiv.apply_symm_apply]
        map_comp := fun {A B C} f g => by
          funext x
          show C.equiv (g (f (A.equiv.symm x))) 
            = (C.equiv ∘ g ∘ B.equiv.symm) ((B.equiv ∘ f ∘ A.equiv.symm) x)

          simp only [Function.comp_apply, Equiv.symm_apply_apply]
    

Again to break this down by components:

• In the object mapping we are taking in a finite set object \(\texttt {A : FinSetObj}\) and mapping it to the corresponding finite ordinal represented by the natural number \(\texttt {A.n}\).
• Our morphism mapping is a bit more complex, since we are going from the category of finite sets our source and target objects \(\texttt {A}\) and \(\texttt {B}\) represent the finite set objects. For all pairs of objects the map function demands:

  
            ∀ {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y))
          

  we are provided with the set of morphisms \(\texttt {f : A.carrier → B.carrier}\) and we need to produce a function between the corresponding finite sets \(\texttt {Fin A.n → Fin B.n}\). Here we utilize an important property that comes with equivalences: they can be used to transport functions between types. To explain what this means let's consider the isolated example:

          variable (A B : FinSetObj) (f : FinSetObj.category.Hom A B)

          #check B.equiv ∘ f      -- ⇑B.equiv ∘ f : A.carrier → Fin B.n
          #check f ∘ A.equiv.symm -- f ∘ ⇑A.equiv.symm : Fin A.n → B.carrier
        

Whats going on here is that the composition coerces the equivalences into functions i.e.

          @[simp, norm_cast]
          lemma _root_.EquivLike.coe_coe {F} [EquivLike F α β] (e : F) :
              ((e : α ≃ β) : α → β) = e := rfl
        

Since the equivalence is between the carrier (set) type and the upper bound witness we have the function

          ⇑B.equiv      B.carrier → Fin B.n
          ⇑A.equiv.symm Fin A.n   → A.carrier
        

hence composing this with our morphism gives

          A.carrier → B.carrier → Fin B.n -- so A.carrier → Fin B.n
          Fin A.n → A.carrier → B.carrier -- so Fin A.n → B.carrier
        

and composing these two results in the desired function \(\texttt {Fin A.n → Fin B.n}\).
• Next we want to show that the functor preserves identities. In our case this means the following:

  
            map_id : ∀ (A : FinSetObj), 
              ⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm = 𝟙 { n := A.n }
          

  As our probelm is of the shape \[ (\forall x, f x = g x) \] We can apply the \(\texttt {funext}\) tactic which reduces the goal to showing that the two sides are equal when applied to an arbitrary input \(\texttt {x}\). Our goal then becomes:

  
            (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x = (𝟙 { n := A.n }) x
          

  It might be helpful at this point to take a look at the underlying types:

  
            ... : Fin { n := A.n }.n → Fin { n := A.n }.n 
            = 
            ... :     { n := A.n }   ⟶     { n := A.n }
          

  The purpose of the \(\texttt {show}\) tactic here is to explicitly specify the goal we want to prove, i.e. create a definitionally equal variant of the goal to replace the current one with, if we look at the goals before and after the show tactic we have:

  
            -- before
            ⊢ (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x = 𝟙 { n := A.n } x
  
            -- after 
            ⊢ A.equiv (id (A.equiv.symm x)) = id x
          

  looking at the types of the goal after the \(\texttt {show}\) tactic we have:

  
            ... : Fin A.n
            = 
            ... : Fin A.n
          

  our final two simplifications then do

  
            A.equiv (id (A.equiv.symm x)) = A.equiv (A.equiv.symm x)
            
            -- id_eq : ... (a : α), id a = a
            A.equiv (A.equiv.symm x) = x
  
            -- apply_symm_apply : ... (e : α ≃ β) (x : β), e (e.symm x) = x
            x = x
          

  For the sake of completeness I want to go into the \(\texttt {show}\) tactic a bit more. Startign with the right hand side, after the funext we have:

  
            𝟙 { n := A.n } x 
          

  The braces here are just syntactic sugar for defining a FinSkel structure inline, so unfolding it we can equivalently display this as:

  
            variable (A : FinSetObj) (x : Fin (FinSkel.mk A.n).n)
            #check FinSkel.cat.id (FinSkel.mk A.n) x
          

  but what we can notice if we look at the definition of our category is that the arrows between objects are actually arrows between their \(\texttt {n}\) fields (with the Fin proof) i.e.

  
            fun A B => Fin A.n → Fin B.n
          

  so in reality our identity morphism is actually:

  
            𝟙 { n := A.n } : Fin A.n → Fin A.n
          

  hence applying it to \(\texttt {x}\) gives us:

  
            (𝟙 { n := A.n }) x = id x
          

  The left hand side follows a similar logic, in that we can again replace the identity morphism on the object with the identity function on the carrier type directly so we have:

  
            (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x 
              -> (⇑A.equiv ∘ id ∘ ⇑A.equiv.symm) x
          

  and then if we avoid the syntactic sugar of function composition we have:

  
            ⇑A.equiv (id (⇑A.equiv.symm x)) 
          

  we can equivalently just automate this step by just prepending \(\texttt {Function.comp}\) into our simplification steps.
• For the case of showing that our functor preserves composition of morphisms we have a similar situation as to the identity case, here just to keep things not dragging on too long i'll just say that again we are more or less following the same logic as before. We are using show to reduce or goal into a form that is easier to reason about, and then we are just simplifying using the properties of equivalences and function composition.

Moving on we now have two create our natural transformations, here things should now be rather straightforward. In lean we have:

      def unitNatTrans 
          : 𝟭 FinSetObj ⟶ finSetObjToSkel ⋙ skelToFinSetObj where
        app := fun A => (A.equiv : A.carrier → Fin A.n)
        naturality := fun A B f => by
          funext x
          show B.equiv (f x) 
            = (B.equiv ∘ f ∘ A.equiv.symm) (A.equiv x)
          simp only [Function.comp_apply, Equiv.symm_apply_apply]

      def unitInvNatTrans 
          : finSetObjToSkel ⋙ skelToFinSetObj ⟶ 𝟭 FinSetObj where
        app := fun A => (A.equiv.symm : Fin A.n → A.carrier)
        naturality := fun A B f => by
          funext x
          show B.equiv.symm ((B.equiv ∘ f ∘ A.equiv.symm) x) 
            = f (A.equiv.symm x)
          simp only [Function.comp_apply, Equiv.symm_apply_apply]

      /-- The unit isomorphism -/
      def unitIsoFinSetObj : 𝟭 FinSetObj ≅ finSetObjToSkel ⋙ skelToFinSetObj where
        hom := unitNatTrans
        inv := unitInvNatTrans
        hom_inv_id := by
          ext A
          funext x
          show A.equiv.symm (A.equiv x) = x
          simp only [Equiv.symm_apply_apply]
        inv_hom_id := by
          ext A
          funext x
          show A.equiv (A.equiv.symm x) = x
          simp only [Equiv.apply_symm_apply]
    

in lean composition of functors is denoted by the operator \(\texttt {⋙}\) so we can see that our unit natural transformation has the correct type. The components of the natural transformation are just given by the equivalences we have in our finite set objects, and the naturality conditions again follow from unfolding the definitions and simplifying.

      /-- Naturality lemma for counit transformations -/
      lemma counit_naturality {A B : FinSkel} (f : A ⟶ B) :
        (𝟭 FinSkel).map f ≫ id = id ≫ (skelToFinSetObj ⋙ finSetObjToSkel).map f := by
        simp only [Functor.id_obj, Functor.comp_obj, skelToFinSetObj, finSetObjToSkel]
        simp only [Functor.id_map, Functor.comp_map]
        rfl

      /-- The counit natural transformation: skelToFinSetObj ⋙ finSetObjToSkel → id -/
      def counitNatTrans : skelToFinSetObj ⋙ finSetObjToSkel ⟶ 𝟭 FinSkel where
        app := λ _ => id
        naturality := fun _ _ f => counit_naturality f |>.symm

      /-- The inverse of counit -/
      def counitInvNatTrans : 𝟭 FinSkel ⟶ skelToFinSetObj ⋙ finSetObjToSkel where
        app := λ _ => id
        naturality := fun _ _ f => counit_naturality f

      /-- The counit isomorphism -/
      def counitIsoFinSkel : skelToFinSetObj ⋙ finSetObjToSkel ≅ 𝟭 FinSkel where
        hom := counitNatTrans
        inv := counitInvNatTrans
        hom_inv_id := by ext A; rfl
        inv_hom_id := by ext A; rfl
    

Finally we can define the equivalence and then construct the essentially small instance:

      /-- The equivalence between FinSetObj and FinSkel -/
      def finSetObjEquiv : FinSetObj ≌ FinSkel where
        functor := finSetObjToSkel
        inverse := skelToFinSetObj
        unitIso := unitIsoFinSetObj
        counitIso := counitIsoFinSkel
        functor_unitIso_comp := fun A => by
          funext x
          show (id : Fin A.n → Fin A.n) (A.equiv (A.equiv.symm x)) = x
          simp only [id_eq, Equiv.apply_symm_apply]

      /-- Now we show FinSetObj is essentially small.
          We construct an explicit equivalence with the small category FinSkel. -/
      instance FinSetObj.essentiallySmall : EssentiallySmall.{0} FinSetObj :=
        EssentiallySmall.mk' finSetObjEquiv