Definition 4.7.1.  Let u, v ∈ ℕ, C be a/an u-small category, D be a/an v-small category. We define:
Fun(C, D) :=: {(C → DX ↦ YX(f : A → B) ↦ gA,B,f) | YX ∈ D for each X ∈ C, gA,B,f : YA → YB is a morphism for each A, B ∈ C and f : A → B, [∀ A ∈ C : gA,A,idA = idYA], [∀ A, B, C ∈ C, d : A → B, e : B → C : gA,C,e∘d = gB,C,e ∘ gA,B,d]}
(C → DX ↦ YX(f : A → B) ↦ gA,B,f) = (C → DX ↦ Y'X(f : A → B) ↦ g'A,B,f)  :⇔  ∃ iX : YX ↔ Y'X f.e. X ∈ C : ∀ A, B ∈ C, f : A → B : iB ∘ gA,B,f = g'A,B,f ∘ iA  (YX ∈ D for each X ∈ C, gA,B,f : YA → YB is a morphism for each A, B ∈ C and f : A → B, Y'X ∈ D for each X ∈ C, g'A,B,f : Y'A → Y'B is a morphism for each A, B ∈ C and f : A → B with suitable conditions)
We write “let F : C → D be a functor” for “let F ∈ Fun(C, D).”
We write “F :  C → DX ↦ YX(f : A → B) ↦ gA,B,f” for “F := (C → DX ↦ YX(f : A → B) ↦ gA,B,f).”
References.