Quelle  Yoneda.thy

(*  Title:       Yoneda
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter Yoneda

theory Yoneda
imports DualCategory SetCat FunctorCategory
begin

  text‹
 This theory defines the notion of a ``hom-functor'' and gives a proof of the Yoneda Lemma.
 In traditional developments of category theory based on set theories such as ZFC,
 hom-functors are normally defined to be functors into the large category \textbf{Set}
 whose objects are of \emph{all} sets and whose arrows are functions between sets.
 However, in HOL there does not exist a single ``type of all sets'', so the notion of
 the category of \emph{all} sets and functions does not make sense. To work around this,
 we consider a more general setting consisting of a category @{term C} together with
 a set category @{term S} and a function @{term "φ :: 'c * 'c ==> 'c ==> 's"} such that
 whenever @{term b} and @{term a} are objects of C then @{term "φ (b, a)"} maps
 ‹C.hom b a› injectively to ‹S.Univ›. We show that these data induce
 a binary functor ‹Hom› from ‹Cop×C› to @{term S} in such a way that @{term φ}
 is rendered natural in @{term "(b, a)"}. The Yoneda lemma is then proved for the
 Yoneda functor determined by ‹Hom›.
 ›

  section "Hom-Functors"

  text‹
 A hom-functor for a category @{term C} allows us to regard the hom-sets of @{term C}
 as objects of a category @{term S} of sets and functions. Any description of a
 hom-functor for @{term C} must therefore specify the category @{term S} and provide
 some sort of correspondence between arrows of @{term C} and elements of objects of @{term S}.
 If we are to think of each hom-set ‹C.hom b a› of ‹C› as corresponding
 to an object ‹Hom (b, a)› of @{term S} then at a minimum it ought to be the
 case that the correspondence between arrows and elements is bijective between
 ‹C.hom b a› and ‹Hom (b, a)›. The ‹hom_functor› locale defined
 below captures this idea by assuming a set category @{term S} and a function @{term φ}
 taking arrows of @{term C} to elements of ‹S.Univ›, such that @{term φ} is injective
 on each set ‹C.hom b a›. We show that these data induce a functor ‹Hom›
 from ‹Cop×C› to ‹S› in such a way that @{term φ} becomes a natural
 bijection between ‹C.hom b a› and ‹Hom (b, a)›.
 ›

  locale hom_functor =
    C: category C +
    S: set_category S setp
  for C :: "'c comp"      (infixr ‹⋅› 55)
  and S :: "'s comp"      (infixr ‹⋅_S› 55)
  and setp :: "'s set ==> bool"
  and φ :: "'c * 'c ==> 'c ==> 's" +
  assumes maps_arr_to_Univ: "C.arr f ==> φ (C.dom f, C.cod f) f ∈ S.Univ"
  and local_inj: "[ C.ide b; C.ide a ] ==> inj_on (φ (b, a)) (C.hom b a)"
  and small_homs: "[ C.ide b; C.ide a ] ==> setp (φ (b, a) ` C.hom b a)"
  begin

    sublocale Cop: dual_category C ..
    sublocale CopxC: product_category Cop.comp C ..

    notation S.in_hom     (‹«_ : _ →_S _¬›)
    notation CopxC.comp   (infixr ‹⊙› 55)
    notation CopxC.in_hom (‹«_ : _ ⇌ _¬›)

    definition set
    where "set ba ≡ φ (fst ba, snd ba) ` C.hom (fst ba) (snd ba)"

    lemma set_subset_Univ:
    assumes "C.ide b" and "C.ide a"
    shows "set (b, a) ⊆ S.Univ"
      using assms set_def maps_arr_to_Univ CopxC.ide_char by auto

    definition ψ :: "'c * 'c ==> 's ==> 'c"
    where "ψ ba = inv_into (C.hom (fst ba) (snd ba)) (φ ba)"

    lemma φ_mapsto:
    assumes "C.ide b" and "C.ide a"
    shows "φ (b, a) ∈ C.hom b a → set (b, a)"
      using assms set_def maps_arr_to_Univ by auto

    lemma ψ_mapsto:
    assumes "C.ide b" and "C.ide a"
    shows "ψ (b, a) ∈ set (b, a) → C.hom b a"
      using assms set_def ψ_def local_inj by auto

    lemma ψ_φ [simp]:
    assumes "«f : b → a¬"
    shows "ψ (b, a) (φ (b, a) f) = f"
      using assms local_inj [of b a] ψ_def by fastforce

    lemma φ_ψ [simp]:
    assumes "C.ide b" and "C.ide a"
    and "x ∈ set (b, a)"
    shows "φ (b, a) (ψ (b, a) x) = x"
      using assms set_def local_inj ψ_def by auto

    lemma ψ_img_set:
    assumes "C.ide b" and "C.ide a"
    shows "ψ (b, a) ` set (b, a) = C.hom b a"
      using assms ψ_def set_def local_inj by auto

    text‹
 A hom-functor maps each arrow @{term "(g, f)"} of @{term "CopxC"}
 to the arrow of the set category @{term[source=true] S} corresponding to the function
 that takes an arrow @{term h} of @{term C} to the arrow @{term "C f (C h g)"} of @{term C}
 obtained by precomposing with @{term g} and postcomposing with @{term f}.
 ›

    definition map
    where "map gf =
             (if CopxC.arr gf then
                S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf))
                        (φ (CopxC.cod gf) o (λh. snd gf ⋅ h ⋅ fst gf) o ψ (CopxC.dom gf))
              else S.null)"

    lemma arr_map:
    assumes "CopxC.arr gf"
    shows "S.arr (map gf)"
    proof -
      have "φ (CopxC.cod gf) o (λh. snd gf ⋅ h ⋅ fst gf) o ψ (CopxC.dom gf)
              ∈ set (CopxC.dom gf) → set (CopxC.cod gf)"
        using assms φ_mapsto [of "fst (CopxC.cod gf)" "snd (CopxC.cod gf)"]
              ψ_mapsto [of "fst (CopxC.dom gf)" "snd (CopxC.dom gf)"]
        by fastforce
      thus ?thesis
        using assms map_def set_subset_Univ small_homs
        by (simp add: set_def)
    qed

    lemma map_ide [simp]:
    assumes "C.ide b" and "C.ide a"
    shows "map (b, a) = S.mkIde (set (b, a))"
    proof -
      have "map (b, a) = S.mkArr (set (b, a)) (set (b, a))
                                 (φ (b, a) o (λh. a ⋅ h ⋅ b) o ψ (b, a))"
        using assms map_def by auto
      also have "... = S.mkArr (set (b, a)) (set (b, a)) (λh. h)"
      proof -
        have "S.mkArr (set (b, a)) (set (b, a)) (λh. h) = ..."
          using assms set_subset_Univ set_def C.comp_arr_dom C.comp_cod_arr
                S.arr_mkIde small_homs
          by (intro S.mkArr_eqI', simp, fastforce)
        thus ?thesis by auto
      qed
      also have "... = S.mkIde (set (b, a))"
        using assms S.mkIde_as_mkArr set_subset_Univ small_homs set_def by simp
      finally show ?thesis by blast
    qed

    lemma set_map:
    assumes "C.ide a" and "C.ide b"
    shows "S.set (map (b, a)) = set (b, a)"
      using assms map_ide set_subset_Univ small_homs set_def by simp

    text‹
 The definition does in fact yield a functor.
 ›

    sublocale "functor" CopxC.comp S map
    proof
      show "∧gf. ¬ CopxC.arr gf ==> map gf = S.null"
        using map_def by auto
      fix gf
      assume gf: "CopxC.arr gf"
      thus arr: "S.arr (map gf)" using gf arr_map by blast
      show "S.dom (map gf) = map (CopxC.dom gf)"
        using arr gf local.map_def map_ide by auto
      show "S.cod (map gf) = map (CopxC.cod gf)"
        using gf set_subset_Univ ψ_mapsto map_def set_def S.arr_mkIde arr map_ide by auto
      next
      fix gf gf'
      assume gf': "CopxC.seq gf' gf"
      hence seq: "C.arr (fst gf) ∧ C.arr (snd gf) ∧ C.dom (snd gf') = C.cod (snd gf) ∧
                  C.arr (fst gf') ∧ C.arr (snd gf') ∧ C.dom (fst gf) = C.cod (fst gf')"
        by (elim CopxC.seqE C.seqE, auto)
      have 0: "S.arr (map (CopxC.comp gf' gf))"
        using gf' arr_map by blast
      have 1: "map (gf' ⊙ gf) =
                    S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf'))
                            (φ (CopxC.cod gf') o (λh. snd (gf' ⊙ gf) ⋅ h ⋅ fst (gf' ⊙ gf))
                                               o ψ (CopxC.dom gf))"
        using gf' map_def using CopxC.cod_comp CopxC.dom_comp by auto
      also have "... = S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf'))
                               (φ (CopxC.cod gf') ∘ (λh. snd gf' ⋅ h ⋅ fst gf') ∘ ψ (CopxC.dom gf')
                                ∘
                               (φ (CopxC.cod gf) ∘ (λh. snd gf ⋅ h ⋅ fst gf) ∘ ψ (CopxC.dom gf)))"
      proof (intro S.mkArr_eqI')
        show "S.arr (S.mkArr (set (CopxC.dom gf)) (set (CopxC.cod gf'))
                             (φ (CopxC.cod gf') ∘ (λh. snd (gf' ⊙ gf) ⋅ h ⋅ fst (gf' ⊙ gf))
                                                ∘ ψ (CopxC.dom gf)))"
          using 0 1 by simp
        show "∧x. x ∈ set (CopxC.dom gf) ==>
                     (φ (CopxC.cod gf') ∘ (λh. snd (gf' ⊙ gf) ⋅ h ⋅ fst (gf' ⊙ gf)) ∘
                      ψ (CopxC.dom gf)) x =
                     (φ (CopxC.cod gf') ∘ (λh. snd gf' ⋅ h ⋅ fst gf') ∘ ψ (CopxC.dom gf') ∘
                      (φ (CopxC.cod gf) ∘ (λh. snd gf ⋅ h ⋅ fst gf) ∘ ψ (CopxC.dom gf))) x"
          using gf' ψ_mapsto set_def ψ_φ C.comp_assoc by fastforce
      qed
      also have "... = map gf' ⋅_S map gf"
        using seq gf' map_def arr_map [of gf] arr_map [of gf'] S.comp_mkArr by auto
      finally show "map (gf' ⊙ gf) = map gf' ⋅_S map gf"
        using seq gf' by auto
    qed

    lemma is_functor:
    shows "functor CopxC.comp S map" ..

    sublocale binary_functor Cop.comp C S map ..

    lemma is_binary_functor:
    shows "binary_functor Cop.comp C S map" ..

    text‹
 The map @{term φ} determines a bijection between @{term "C.hom b a"} and
 @{term "set (b, a)"} which is natural in @{term "(b, a)"}.
 ›

    lemma φ_local_bij:
    assumes "C.ide b" and "C.ide a"
    shows "bij_betw (φ (b, a)) (C.hom b a) (set (b, a))"
      using assms local_inj inj_on_imp_bij_betw set_def by auto

    lemma φ_natural:
    assumes "C.arr g" and "C.arr f" and "h ∈ C.hom (C.cod g) (C.dom f)"
    shows "φ (C.dom g, C.cod f) (f ⋅ h ⋅ g) = S.Fun (map (g, f)) (φ (C.cod g, C.dom f) h)"
    proof -
      let ?φh = "φ (C.cod g, C.dom f) h"
      have φh: "?φh ∈ set (C.cod g, C.dom f)"
        using assms φ_mapsto set_def by simp
      have gf: "CopxC.arr (g, f)" using assms by simp
      have "S.Fun (map (g, f)) ?φh =
                (φ (C.dom g, C.cod f) ∘ (λh. f ⋅ h ⋅ g) ∘ ψ (C.cod g, C.dom f)) ?φh"
      proof -
        have "S.Fun (map (g, f)) =
                 restrict (φ (C.dom g, C.cod f) ∘ (λh. f ⋅ h ⋅ g) ∘ ψ (C.cod g, C.dom f))
                          (set (C.cod g, C.dom f))"
        proof -
          have "map (g, f) =
                   S.mkArr (set (C.cod g, C.dom f)) (set (C.dom g, C.cod f))
                           (φ (C.dom g, C.cod f) ∘ (λh. f ⋅ h ⋅ g) ∘ ψ (C.cod g, C.dom f))"
            using assms map_def by simp
          moreover have "S.arr (map (g, f))" using gf by simp
          ultimately show ?thesis
            using S.Fun_mkArr by simp
        qed
        thus ?thesis
          using φh by simp
      qed
      also have "... = φ (C.dom g, C.cod f) (f ⋅ h ⋅ g)"
        using assms(3) by simp
      finally show ?thesis by auto
    qed

    lemma Dom_map:
    assumes "C.arr g" and "C.arr f"
    shows "S.Dom (map (g, f)) = set (C.cod g, C.dom f)"
      using assms map_def preserves_arr by auto

    lemma Cod_map:
    assumes "C.arr g" and "C.arr f"
    shows "S.Cod (map (g, f)) = set (C.dom g, C.cod f)"
      using assms map_def preserves_arr by auto

    lemma Fun_map:
    assumes "C.arr g" and "C.arr f"
    shows "S.Fun (map (g, f)) =
             restrict (φ (C.dom g, C.cod f) o (λh. f ⋅ h ⋅ g) o ψ (C.cod g, C.dom f))
                      (set (C.cod g, C.dom f))"
      using assms map_def preserves_arr by force

    lemma map_simp_1:
    assumes "C.arr g" and "C.ide a"
    shows "map (g, a) = S.mkArr (set (C.cod g, a)) (set (C.dom g, a))
                                (φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a))"
    proof -
      have 1: "map (g, a) = S.mkArr (set (C.cod g, a)) (set (C.dom g, a))
                                    (φ (C.dom g, a) o (λh. a ⋅ h ⋅ g) o ψ (C.cod g, a))"
        using assms map_def by force
      also have "... = S.mkArr (set (C.cod g, a)) (set (C.dom g, a))
                               (φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a))"
        using assms 1 preserves_arr [of "(g, a)"] set_def C.in_homI C.comp_cod_arr
        by (intro S.mkArr_eqI) auto
     finally show ?thesis by blast
    qed

    lemma map_simp_2:
    assumes "C.ide b" and "C.arr f"
    shows "map (b, f) = S.mkArr (set (b, C.dom f)) (set (b, C.cod f))
                                (φ (b, C.cod f) o C f o ψ (b, C.dom f))"
    proof -
      have 1: "map (b, f) = S.mkArr (set (b, C.dom f)) (set (b, C.cod f))
                                    (φ (b, C.cod f) o (λh. f ⋅ h ⋅ b) o ψ (b, C.dom f))"
        using assms map_def by force
      also have "... = S.mkArr (set (b, C.dom f)) (set (b, C.cod f))
                               (φ (b, C.cod f) o C f o ψ (b, C.dom f))"
        using assms 1 preserves_arr [of "(b, f)"] set_def C.in_homI C.comp_arr_dom
        by (intro S.mkArr_eqI) auto
      finally show ?thesis by blast
    qed

  end

  text‹
 Every category @{term C} has a hom-functor: take @{term S} to be the replete set category
 generated by the arrow type ‹'a› of @{term C} and take @{term "φ (b, a)"} to be the map
 ‹S.UP :: 'a ==> 'a SC.arr›.
 ›

  context category
  begin

    interpretation S: replete_setcat ‹TYPE('a)› .

    lemma has_hom_functor:
    shows "hom_functor C S.comp S.setp (λ_. S.UP)"
      using S.UP_mapsto S.inj_UP injD inj_onI
      by unfold_locales (auto simp add: inj_def inj_onI)

  end

  text‹
 The locales ‹set_valued_functor› and ‹set_valued_transformation› provide some
 abbreviations that are convenient when working with functors and natural transformations
 into a set category.
 ›

  locale set_valued_functor =
    C: category C +
    S: set_category S setp +
    "functor" C S F
    for C :: "'c comp"
    and S :: "'s comp"
    and setp :: "'s set ==> bool"
    and F :: "'c ==> 's"
  begin

    abbreviation SET :: "'c ==> 's set"
    where "SET a ≡ S.set (F a)"
    
    abbreviation DOM :: "'c ==> 's set"
    where "DOM f ≡ S.Dom (F f)"
    
    abbreviation COD :: "'c ==> 's set"
    where "COD f ≡ S.Cod (F f)"

    abbreviation FUN :: "'c ==> 's ==> 's"
    where "FUN f ≡ S.Fun (F f)"

  end

  locale set_valued_transformation =
    C: category C +
    S: set_category S setp +
    F: set_valued_functor C S setp F +
    G: set_valued_functor C S setp G +
    natural_transformation C S F G τ
  for C :: "'c comp"
  and S :: "'s comp"
  and setp :: "'s set ==> bool"
  and F :: "'c ==> 's"
  and G :: "'c ==> 's"
  and τ :: "'c ==> 's"
  begin
  
    abbreviation DOM :: "'c ==> 's set"
    where "DOM f ≡ S.Dom (τ f)"
    
    abbreviation COD :: "'c ==> 's set"
    where "COD f ≡ S.Cod (τ f)"

    abbreviation FUN :: "'c ==> 's ==> 's"
    where "FUN f ≡ S.Fun (τ f)"

  end

  section "Yoneda Functors"
    
  text‹
 A Yoneda functor is the functor from @{term C} to ‹[Cop, S]› obtained by ``currying''
 a hom-functor in its first argument.
 ›

  locale yoneda_functor =
    C: category C +
    Cop: dual_category C +
    CopxC: product_category Cop.comp C +
    S: set_category S setp +
    Hom: hom_functor C S setp φ
  for C :: "'c comp"      (infixr ‹⋅› 55)
  and S :: "'s comp"      (infixr ‹⋅_S› 55)
  and setp :: "'s set ==> bool"
  and φ :: "'c * 'c ==> 'c ==> 's"
  begin

    sublocale Cop_S: functor_category Cop.comp S ..
    sublocale curried_functor' Cop.comp C S Hom.map ..

    notation Cop_S.in_hom (‹«_ : _ →_[Cop,S] _¬›)

    abbreviation ψ
    where "ψ ≡ Hom.ψ"

    text‹
 An arrow of the functor category ‹[Cop, S]› consists of a natural transformation
 bundled together with its domain and codomain functors. However, when considering
 a Yoneda functor from @{term[source=true] C} to ‹[Cop, S]› we generally are only
 interested in the mapping @{term Y} that takes each arrow @{term f} of @{term[source=true] C}
 to the corresponding natural transformation @{term "Y f"}. The domain and codomain functors
 are then the identity transformations @{term "Y (C.dom f)"} and @{term "Y (C.cod f)"}.
 ›

    definition Y
    where "Y f ≡ Cop_S.Map (map f)"

    lemma Y_simp [simp]:
    assumes "C.arr f"
    shows "Y f = (λg. Hom.map (g, f))"
      using assms preserves_arr Y_def by simp

    lemma Y_ide_is_functor:
    assumes "C.ide a"
    shows "functor Cop.comp S (Y a)"
      using assms Y_def Hom.fixing_ide_gives_functor_2 by force

    lemma Y_arr_is_transformation:
    assumes "C.arr f"
    shows "natural_transformation Cop.comp S (Y (C.dom f)) (Y (C.cod f)) (Y f)"
      using assms Y_def [of f] map_def Hom.fixing_arr_gives_natural_transformation_2
            preserves_dom preserves_cod by fastforce

    lemma Y_ide_arr [simp]:
    assumes a: "C.ide a" and "«g : b' → b¬"
    shows "«Y a g : Hom.map (b, a) →_S Hom.map (b', a)¬"
    and "Y a g = S.mkArr (Hom.set (b, a)) (Hom.set (b', a)) (φ (b', a) o Cop.comp g o ψ (b, a))"
      using assms Hom.map_simp_1 by (fastforce, auto)

    lemma Y_arr_ide [simp]:
    assumes "C.ide b" and "«f : a → a'¬"
    shows "«Y f b : Hom.map (b, a) →_S Hom.map (b, a')¬"
    and "Y f b = S.mkArr (Hom.set (b, a)) (Hom.set (b, a')) (φ (b, a') o C f o ψ (b, a))"
      using assms apply fastforce
      using assms Hom.map_simp_2 by auto

  end

  locale yoneda_functor_fixed_object =
    yoneda_functor +
  fixes a
  assumes ide_a: "C.ide a"
  begin
  
    sublocale "functor" Cop.comp S ‹Y a›
      using ide_a Y_ide_is_functor by auto
    sublocale set_valued_functor Cop.comp S setp ‹Y a› ..

  end

  text‹
 The Yoneda lemma states that, given a category @{term C} and a functor @{term F}
 from @{term Cop} to a set category @{term S}, for each object @{term a} of @{term C},
 the set of natural transformations from the contravariant functor @{term "Y a"}
 to @{term F} is in bijective correspondence with the set ‹F.SET a›
 of elements of @{term "F a"}.

 Explicitly, if @{term e} is an arbitrary element of the set ‹F.SET a›,
 then the functions ‹λx. F.FUN (ψ (b, a) x) e› are the components of a
 natural transformation from @{term "Y a"} to @{term F}.
 Conversely, if @{term τ} is a natural transformation from @{term "Y a"} to @{term F},
 then the component @{term "τ b"} of @{term τ} at an arbitrary object @{term b}
 is completely determined by the single arrow ‹τ.FUN a (φ (a, a) a)))›,
 which is the the element of ‹F.SET a› that corresponds to the image of the
 identity @{term a} under the function ‹τ.FUN a›.
 Then @{term "τ b"} is the arrow from @{term "Y a b"} to @{term "F b"} corresponding
 to the function ‹λx. (F.FUN (ψ (b, a) x) (τ.FUN a (φ (a, a) a)))›
 from ‹S.set (Y a b)› to ‹F.SET b›.
 
 The above expressions look somewhat more complicated than the usual versions due to the
 need to account for the coercions @{term φ} and @{term ψ}.
 ›

  locale yoneda_lemma =
    yoneda_functor_fixed_object C S setp φ a +
    F: set_valued_functor Cop.comp S setp F
  for C :: "'c comp" (infixr ‹⋅› 55)
  and S :: "'s comp" (infixr ‹⋅_S› 55)
  and setp :: "'s set ==> bool"
  and φ :: "'c * 'c ==> 'c ==> 's"
  and F :: "'c ==> 's"
  and a :: 'c
  begin

    text‹
 The mapping that evaluates the component @{term "τ a"} at @{term a} of a
 natural transformation @{term τ} from @{term Y} to @{term F} on the element
 @{term "φ (a, a) a"} of @{term "SET a"}, yielding an element of @{term "F.SET a"}.
 ›

    definition E :: "('c ==> 's) ==> 's"
    where "E τ = S.Fun (τ a) (φ (a, a) a)"

    text‹
 The mapping that takes an element @{term e} of @{term "F.SET a"} and produces
 a map on objects of @{term[source=true] C} whose value at @{term b} is the arrow of
 @{term[source=true] S} corresponding to the function
 @{term "(λx. F.FUN (ψ (b, a) x) e) ∈ Hom.set (b, a) → F.SET b"}.
 ›

    definition T_o :: "'s ==> 'c ==> 's"
    where "T_o e b = S.mkArr (Hom.set (b, a)) (F.SET b) (λx. F.FUN (ψ (b, a) x) e)"

    lemma T_{o_in_hom}:
    assumes e: "e ∈ S.set (F a)" and b: "C.ide b"
    shows "«T_o e b : Y a b →_S F b¬"
    proof -
      have "(λx. F.FUN (ψ (b, a) x) e) ∈ Hom.set (b, a) → F.SET b"
      proof
        fix x
        assume x: "x ∈ Hom.set (b, a)"
        thus "F.FUN (ψ (b, a) x) e ∈ F.SET b"
          using assms e ide_a Hom.ψ_mapsto S.Fun_mapsto [of "F (ψ (b, a) x)"] by force
      qed
      thus ?thesis
        using ide_a b S.mkArr_in_hom Hom.set_subset_Univ S.mkIde_set T_{o_def}
        by (metis C.ideD(1) Cop.ide_char F.preserves_ide Hom.set_map S.setp_set_ide
            preserves_ide Y_simp)
    qed

    text‹
 For each @{term "e ∈ F.SET a"}, the mapping @{term "T_o e"} gives the components
 of a natural transformation @{term T} from @{term "Y a"} to @{term F}.
 ›

    lemma T_{o_induces_transformation}:
    assumes e: "e ∈ S.set (F a)"
    shows "transformation_by_components Cop.comp S (Y a) F (T_o e)"
    proof
      show "∧b. Cop.ide b ==> «T_o e b : Y a b →_S F b¬"
        using ide_a e T_{o_in_hom} by simp
      fix g :: 'c
      assume g: "Cop.arr g"
      let ?b = "Cop.dom g"
      let ?b' = "Cop.cod g"
      show "T_o e (Cop.cod g) ⋅_S Y a g = F g ⋅_S T_o e (Cop.dom g)"
      proof -
        have 1: "T_o e (Cop.cod g) ⋅_S Y a g =
                 S.mkArr (Hom.set (?b, a)) (F.SET ?b')
                         ((λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a)))"
        proof -
          have "S.arr (S.mkArr (Hom.set (?b', a)) (F.SET ?b') (λs. F.FUN (ψ (?b', a) s) e)) ∧
                S.dom (S.mkArr (Hom.set (?b', a)) (F.SET ?b') (λs. F.FUN (ψ (?b', a) s) e))
                   = Y a ?b' ∧
                S.cod (S.mkArr (Hom.set (?b', a)) (F.SET ?b') (λs. F.FUN (ψ (?b', a) s) e))
                   = F ?b'"
            using Cop.cod_char T_{o_def} T_{o_in_hom} e g
            by (metis Cop.ide_char Cop.ide_cod S.in_homE)
          moreover have "Y a g = S.mkArr (Hom.set (?b, a)) (Hom.set (?b', a))
                                         (φ (?b', a) ∘ Cop.comp g ∘ ψ (?b, a))"
            using Y_ide_arr [of a g ?b' ?b] ide_a g by auto
          ultimately show ?thesis
            using ide_a e g Y_ide_arr Cop.cod_char T_{o_def} S.comp_mkArr preserves_arr
            by metis
        qed
        also have "... = S.mkArr (Hom.set (?b, a)) (F.SET ?b')
                                 (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e))"
        proof (intro S.mkArr_eqI')
          show "S.arr (S.mkArr (Hom.set (?b, a)) (F.SET ?b')
                               ((λx. F.FUN (ψ (?b', a) x) e)
                                  o (φ (?b', a) o Cop.comp g o ψ (?b, a))))"
          proof (intro S.arr_mkArrI)
            show "setp (Hom.set (Cop.dom g, a))"
              by (metis C.ideD(1) Cop.arr_dom Cop.ide_char CopxC.arrI_PC Hom.arr_map
                  S.arr_mkIde Cop.ide_dom g Hom.map_ide ide_a)
            show "setp (F.SET (Cop.cod g))"
              using g by force
            show "(λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a))
                      ∈ Hom.set (?b, a) → F.SET ?b'"
            proof -
              have "S.arr (S (T_o e ?b') (Y a g))"
                using ide_a e g T_{o_in_hom} Y_ide_arr(1) Cop.ide_char Cop.ide_cod by blast
              thus ?thesis using 1 by simp
            qed
          qed
          show "∧x. x ∈ Hom.set (?b, a) ==>
                        ((λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a))) x
                        = (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e)) x"
          proof -
            fix x
            assume x: "x ∈ Hom.set (?b, a)"
            have "((λx. (F.FUN o ψ (?b', a)) x e)
                       o (φ (?b', a) o Cop.comp g o ψ (?b, a))) x
                    = F.FUN (ψ (?b', a) (φ (?b', a) (C (ψ (?b, a) x) g))) e"
              by simp
            also have "... = (F.FUN g o (F.FUN o ψ (?b, a)) x) e"
            proof -
              have "«ψ (?b, a) x : ?b → a¬"
                using ide_a x g Hom.ψ_mapsto [of ?b a] by auto
              thus ?thesis
                using assms g Hom.ψ_φ F.preserves_comp by fastforce
            qed
            also have "... = (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e)) x" by fastforce
            finally show "((λx. F.FUN (ψ (?b', a) x) e) o (φ (?b', a) o Cop.comp g o ψ (?b, a))) x
                            = (F.FUN g o (λx. F.FUN (ψ (?b, a) x) e)) x"
              by simp
          qed
        qed
        also have "... = F g ⋅_S T_o e ?b"
        proof -
          have "S.arr (F g) ∧ F g = S.mkArr (F.SET ?b) (F.SET ?b') (F.FUN g)"
            using g S.mkArr_Fun [of "F g"] by simp
          moreover have
              "S.arr (T_o e ?b) ∧
               T_o e ?b = S.mkArr (Hom.set (?b, a)) (F.SET ?b) (λx. F.FUN (ψ (?b, a) x) e)"
            using e g T_{o_def} T_{o_in_hom}
            by (metis C.ide_cod Cop.arr_char Cop.dom_char S.in_homE)
          ultimately show ?thesis
            using S.comp_mkArr by metis
        qed
        finally show ?thesis by blast
      qed
    qed

    definition T :: "'s ==> 'c ==> 's"
    where "T e ≡ transformation_by_components.map Cop.comp S (Y a) (T_o e)"

  end

  locale yoneda_lemma_fixed_e =
    yoneda_lemma +
  fixes e
  assumes E: "e ∈ F.SET a"
  begin

    interpretation Te: transformation_by_components Cop.comp S ‹Y a› F ‹T_o e›
      using E T_{o_induces_transformation} by auto
    sublocale Te: natural_transformation Cop.comp S ‹Y a› F ‹T e›
      unfolding T_def ..

    lemma natural_transformation_Te:
    shows "natural_transformation Cop.comp S (Y a) F (T e)" ..

    lemma Te_ide:
    assumes "Cop.ide b"
    shows "S.arr (T e b)"
    and "T e b = S.mkArr (Hom.set (b, a)) (F.SET b) (λx. F.FUN (ψ (b, a) x) e)"
      using assms apply auto[1]
      using assms T_{o_def} T_def by auto

  end

  locale yoneda_lemma_fixed_τ =
    yoneda_lemma +
    τ: natural_transformation Cop.comp S ‹Y a› F τ
  for τ
  begin

    sublocale τ: set_valued_transformation Cop.comp S setp ‹Y a› F τ ..

    text‹
 The key lemma: The component @{term "τ b"} of @{term τ} at an arbitrary object @{term b}
 is completely determined by the single element @{term "τ.FUN a (φ (a, a) a) ∈ F.SET a"}.
 ›

    lemma τ_ide:
    assumes b: "Cop.ide b"
    shows "τ b = S.mkArr (Hom.set (b, a)) (F.SET b)
                         (λx. (F.FUN (ψ (b, a) x) (τ.FUN a (φ (a, a) a))))"
    proof -
      let ?φa = "φ (a, a) a"
      have φa: "φ (a, a) a ∈ Hom.set (a, a)" using ide_a Hom.φ_mapsto by fastforce
      have 1: "τ b = S.mkArr (Hom.set (b, a)) (F.SET b) (τ.FUN b)"
        using ide_a b S.mkArr_Fun [of "τ b"] Hom.set_map by auto
      also have
          "... = S.mkArr (Hom.set (b, a)) (F.SET b) (λx. (F.FUN (ψ (b, a) x) (τ.FUN a ?φa)))"
      proof (intro S.mkArr_eqI')
        show 2: "S.arr (S.mkArr (Hom.set (b, a)) (F.SET b) (τ.FUN b))"
          using ide_a b 1 S.mkArr_Fun [of "τ b"] Hom.set_map by auto
        show "∧x. x ∈ Hom.set (b, a) ==> τ.FUN b x = (F.FUN (ψ (b, a) x) (τ.FUN a ?φa))"
        proof -
          fix x
          assume x: "x ∈ Hom.set (b, a)"
          let ?ψx = "ψ (b, a) x"
          have ψx: "«?ψx : b → a¬"
            using ide_a b x Hom.ψ_mapsto [of b a] by auto
          show "τ.FUN b x = (F.FUN (ψ (b, a) x) (τ.FUN a ?φa))"
          proof -
            have "τ.FUN b x = S.Fun (τ b ⋅_S Y a ?ψx) ?φa"
            proof -
              have "τ.FUN b x = τ.FUN b ((φ (b, a) o Cop.comp ?ψx) a)"
                using ide_a b x ψx Hom.φ_ψ
                by (metis C.comp_cod_arr C.in_homE C.ide_dom Cop.comp_def comp_apply)
              also have "... = (τ.FUN b o (φ (b, a) o Cop.comp ?ψx o ψ (a, a))) ?φa"
                using ide_a b C.ide_in_hom by simp
              also have "... = S.Fun (τ b ⋅_S Y a ?ψx) ?φa"
              proof -
                have "S.seq (τ b) (Y a ?ψx) ∧
                      τ b ⋅_S Y a ?ψx =
                         S.mkArr (Hom.set (a, a)) (F.SET b)
                                 (τ.FUN b o (φ (b, a) ∘ Cop.comp ?ψx ∘ ψ (a, a)))"
                proof
                  show "S.seq (τ b) (Y a ?ψx)"
                    using ψx τ.naturality2 by fastforce
                  show "τ b ⋅_S Y a ?ψx =
                           S.mkArr (Hom.set (a, a)) (F.SET b)
                                   (τ.FUN b o (φ (b, a) ∘ Cop.comp ?ψx ∘ ψ (a, a)))"
                    by (metis 1 2 Cop.arrI Cop.hom_char S.comp_mkArr Y_ide_arr(2)
                        ψx ide_a preserves_arr)
                qed
                thus ?thesis
                  using ide_a b x Hom.φ_mapsto S.Fun_mkArr by force
              qed
              finally show ?thesis by auto
            qed
            also have "... = S.Fun (F ?ψx ⋅_S τ a) ?φa"
              using ide_a b ψx τ.naturality by force
            also have "... = F.FUN ?ψx (τ.FUN a ?φa)"
            proof -
              have "restrict (S.Fun (F ?ψx ⋅_S τ a)) (Hom.set (a, a))
                               = restrict (F.FUN (ψ (b, a) x) o τ.FUN a) (Hom.set (a, a))"
              proof -
                have "S.arr (F ?ψx ⋅_S τ a) ∧
                      F ?ψx ⋅_S τ a = S.mkArr (Hom.set (a, a)) (F.SET b) (F.FUN ?ψx o τ.FUN a)"
                proof
                  show 1: "S.seq (F ?ψx) (τ a)"
                    using ψx ide_a τ.preserves_cod F.preserves_dom
                    by (elim C.in_homE, auto)
                  show "F ?ψx ⋅_S τ a = S.mkArr (Hom.set (a, a)) (F.SET b) (F.FUN ?ψx o τ.FUN a)"
                  proof -
                    have "τ a = S.mkArr (Hom.set (a, a)) (F.SET a) (τ.FUN a)"
                      using ide_a 1 S.mkArr_Fun [of "τ a"] Hom.set_map by auto
                    moreover have "F ?ψx = S.mkArr (F.SET a) (F.SET b) (F.FUN ?ψx)"
                      using x ψx 1 S.mkArr_Fun [of "F ?ψx"] by fastforce
                    ultimately show ?thesis
                      using 1 S.comp_mkArr [of "Hom.set (a, a)" "F.SET a" "τ.FUN a"
                                               "F.SET b" "F.FUN ?ψx"]
                      by (elim S.seqE, auto)
                  qed
                qed
                thus ?thesis by force
              qed
              thus "S.Fun (F (ψ (b, a) x) ⋅_S τ a) ?φa = F.FUN ?ψx (τ.FUN a ?φa)"
                 using ide_a φa restr_eqE [of "S.Fun (F ?ψx ⋅_S τ a)"
                                              "Hom.set (a, a)" "F.FUN ?ψx o τ.FUN a"]
                 by simp
            qed
            finally show ?thesis by simp
          qed
        qed
      qed
      finally show ?thesis by auto
    qed

    text‹
 Consequently, if @{term τ'} is any natural transformation from @{term "Y a"} to @{term F}
 that agrees with @{term τ} at @{term a}, then @{term "τ' = τ"}.
 ›

    lemma eqI:
    assumes "natural_transformation Cop.comp S (Y a) F τ'" and "τ' a = τ a"
    shows "τ' = τ"
    proof (intro natural_transformation_eqI)
      interpret τ': natural_transformation Cop.comp S ‹Y a› F τ' using assms by auto
      interpret T': yoneda_lemma_fixed_τ C S setp φ F a τ' ..
      show "natural_transformation Cop.comp S (Y a) F τ" ..
      show "natural_transformation Cop.comp S (Y a) F τ'" ..
      show "∧b. Cop.ide b ==> τ' b = τ b"
        using assms(2) τ_ide T'.τ_ide by simp
    qed

  end

  context yoneda_lemma
  begin

    text‹
 One half of the Yoneda lemma:
 The mapping @{term T} is an injection, with left inverse @{term E},
 from the set @{term "F.SET a"} to the set of natural transformations from
 @{term "Y a"} to @{term F}.
 ›

    lemma T_is_injection:
    assumes "e ∈ F.SET a"
    shows "natural_transformation Cop.comp S (Y a) F (T e)" and "E (T e) = e"
    proof -
      interpret yoneda_lemma_fixed_e C S setp φ F a e
        using assms by (unfold_locales, auto)
      show "natural_transformation Cop.comp S (Y a) F (T e)" ..
      show "E (T e) = e"
        unfolding E_def
        using assms Te_ide S.Fun_mkArr Hom.φ_mapsto Hom.ψ_φ ide_a
              F.preserves_ide S.Fun_ide restrict_apply C.ide_in_hom
        by (auto simp add: Pi_iff)
    qed

    lemma Eτ_mapsto:
    assumes "natural_transformation Cop.comp S (Y a) F τ"
    shows "E τ ∈ F.SET a"
    proof -
      interpret τ: natural_transformation Cop.comp S ‹Y a› F τ
        using assms by auto
      interpret yoneda_lemma_fixed_τ C S setp φ F a τ ..
      show ?thesis
      proof (unfold E_def)
        have "τ.FUN a ∈ Hom.set (a, a) → F.SET a"
        proof -
          have "S.arr (τ a) ∧ S.Dom (τ a) = Hom.set (a, a) ∧ S.Cod (τ a) = F.SET a"
            using ide_a Hom.set_map by auto
          thus ?thesis
            using S.Fun_mapsto by blast
        qed
        thus "τ.FUN a (φ (a, a) a) ∈ F.SET a"
          using ide_a Hom.φ_mapsto by fastforce
      qed
    qed

    text‹
 The other half of the Yoneda lemma:
 The mapping @{term T} is a surjection, with right inverse @{term E},
 taking natural transformations from @{term "Y a"} to @{term F}
 to elements of @{term "F.SET a"}.
 ›

    lemma T_is_surjection:
    assumes "natural_transformation Cop.comp S (Y a) F τ"
    shows "T (E τ) = τ"
    proof -
      interpret natural_transformation Cop.comp S ‹Y a› F τ
        using assms by auto
      interpret yoneda_lemma_fixed_τ C S setp φ F a τ ..
      interpret yoneda_lemma_fixed_e C S setp φ F a ‹E τ›
        using assms Eτ_mapsto by unfold_locales auto
      show "T (E τ) = τ"
        using ide_a τ_ide [of a] Te_ide E_def natural_transformation_Te
        by (intro eqI) auto
    qed
     
    text‹
 The main result.
 ›

    theorem yoneda_lemma:
    shows "bij_betw T (F.SET a) {τ. natural_transformation Cop.comp S (Y a) F τ}"
      using Eτ_mapsto T_is_injection T_is_surjection
      by (intro bij_betwI) auto

  end

  text‹
 We now consider the special case in which @{term F} is the contravariant
 functor @{term "Y a'"}. Then for any @{term e} in ‹Hom.set (a, a')›
 we have @{term "T e = Y (ψ (a, a') e)"}, and @{term T} is a bijection from
 ‹Hom.set (a, a')› to the set of natural transformations from @{term "Y a"}
 to @{term "Y a'"}. It then follows that that the Yoneda functor @{term Y}
 is a fully faithful functor from @{term C} to the functor category ‹[Cop, S]›.
 ›

  locale yoneda_lemma_for_hom =
    yoneda_functor_fixed_object C S setp φ a +
    Ya': yoneda_functor_fixed_object C S setp φ a' +
    yoneda_lemma C S setp φ "Y a'" a
  for C :: "'c comp" (infixr ‹⋅› 55)
  and S :: "'s comp" (infixr ‹⋅_S› 55)
  and setp :: "'s set ==> bool"
  and φ :: "'c * 'c ==> 'c ==> 's"
  and a :: 'c
  and a' :: 'c +
  assumes ide_a': "C.ide a'"
  begin

    text‹
 In case @{term F} is the functor @{term "Y a'"}, for any @{term "e ∈ Hom.set (a, a')"}
 the induced natural transformation @{term "T e"} from @{term "Y a"} to @{term "Y a'"}
 is just @{term "Y (ψ (a, a') e)"}.
 ›

    lemma app_T_equals:
    assumes e: "e ∈ Hom.set (a, a')"
    shows "T e = Y (ψ (a, a') e)"
    proof -
      let ?ψe = "ψ (a, a') e"
      have ψe: "«?ψe : a → a'¬" using ide_a ide_a' e Hom.ψ_mapsto by auto
      interpret Ye: natural_transformation Cop.comp S ‹Y a› ‹Y a'› ‹Y ?ψe›
        using Y_arr_is_transformation [of ?ψe] ψe by (elim C.in_homE, auto)
      interpret yoneda_lemma_fixed_e C S setp φ ‹Y a'› a e
        using ide_a ide_a' e Hom.set_map
        by (unfold_locales, simp_all)
      interpret yoneda_lemma_fixed_τ C S setp φ ‹Y a'› a ‹T e› ..
      have "natural_transformation Cop.comp S (Y a) (Y a') (Y ?ψe)" ..
      moreover have "natural_transformation Cop.comp S (Y a) (Y a') (T e)" ..
      moreover have "T e a = Y ?ψe a"
      proof -
        have 1: "T e a = S.mkArr (Hom.set (a, a)) (Ya'.SET a) (λx. Ya'.FUN (ψ (a, a) x) e)"
          using ide_a T_{o_def} Te_ide by simp
        also have
            "... = S.mkArr (Hom.set (a, a)) (Hom.set (a, a')) (φ (a, a') o C ?ψe o ψ (a, a))"
        proof (intro S.mkArr_eqI)
          show "S.arr (S.mkArr (Hom.set (a, a)) (Ya'.SET a) (λx. Ya'.FUN (ψ (a, a) x) e))"
            using ide_a e 1 Te.preserves_reflects_arr
            by (metis Cop.ide_char Te_ide(1))
          show "Hom.set (a, a) = Hom.set (a, a)" ..
          show 2: "Ya'.SET a = Hom.set (a, a')"
            using ide_a ide_a' Y_simp Hom.set_map by simp
          show "∧x. x ∈ Hom.set (a, a) ==>
                      Ya'.FUN (ψ (a, a) x) e = (φ (a, a') o C ?ψe o ψ (a, a)) x"
          proof -
            fix x
            assume x: "x ∈ Hom.set (a, a)"
            have ψx: "«ψ (a, a) x : a → a¬"
              using ide_a x Hom.ψ_mapsto [of a a] by auto
            have "S.arr (Y a' (ψ (a, a) x)) ∧
                  Y a' (ψ (a, a) x) = S.mkArr (Hom.set (a, a')) (Hom.set (a, a'))
                                              (φ (a, a') ∘ Cop.comp (ψ (a, a) x) ∘ ψ (a, a'))"
              using Y_ide_arr ide_a ide_a' ψx by blast
            hence "Ya'.FUN (ψ (a, a) x) e = (φ (a, a') ∘ Cop.comp (ψ (a, a) x) ∘ ψ (a, a')) e"
              using e 2 S.Fun_mkArr Ya'.preserves_reflects_arr [of "ψ (a, a) x"] by simp
            also have "... = (φ (a, a') o C ?ψe o ψ (a, a)) x" by simp
            finally show "Ya'.FUN (ψ (a, a) x) e = (φ (a, a') o C ?ψe o ψ (a, a)) x" by auto
          qed
        qed
        also have "... = Y ?ψe a"
          using ide_a ide_a' Y_arr_ide ψe by simp
        finally show "T e a = Y ?ψe a" by auto
      qed
      ultimately show ?thesis using eqI by auto
    qed

    lemma is_injective_on_homs:
    shows "inj_on map (C.hom a a')"
    proof (intro inj_onI)
      fix f f'
      assume f: "f ∈ C.hom a a'" and f': "f' ∈ C.hom a a'"
      assume eq: "map f = map f'"
      show "f = f'"
      proof -
        have "f = ψ (a, a') (E (Y (ψ (a, a') (φ (a, a') f))))"
          by (metis (no_types, lifting) C.comp_arr_dom C.ide_in_hom Hom.φ_natural
              Hom.ψ_φ E_def category.in_homE f ide_a mem_Collect_eq
              Y_simp yoneda_functor_axioms yoneda_functor_def)
        also have "... = ψ (a, a') (E (T (φ (a, a') f')))"
          using f f' eq Hom.φ_mapsto [of a a'] ide_a Hom.ψ_φ Y_def
                app_T_equals [of "φ (a, a') f'"]
          by fastforce
        also have "... = f'"
          by (metis C.ideD(1) Hom.φ_mapsto Hom.ψ_φ Hom.set_map PiE Y_simp
              T_is_injection(2) f' ide_a ide_a' mem_Collect_eq)
        finally show ?thesis by auto
      qed
    qed

  end

  context yoneda_functor
  begin

    sublocale faithful_functor C Cop_S.comp map
    proof
      fix f :: 'c and f' :: 'c
      assume par: "C.par f f'" and ff': "map f = map f'"
      show "f = f'"
      proof -
        interpret Ya': yoneda_functor_fixed_object C S setp φ ‹C.cod f›
          using par by (unfold_locales, auto)
        interpret yoneda_lemma_for_hom C S setp φ ‹C.dom f› ‹C.cod f›
          using par by (unfold_locales, auto)
        show "f = f'"
          using par ff' is_injective_on_homs inj_on_def [of map "C.hom (C.dom f) (C.cod f)"]
          by force
      qed
    qed

    lemma is_faithful_functor:
    shows "faithful_functor C Cop_S.comp map"
      ..

    sublocale full_functor C Cop_S.comp map
    proof
      fix a :: 'c and a' :: 'c and t
      assume a: "C.ide a" and a': "C.ide a'"
      assume t: "«t : map a →_[Cop,S] map a'¬"
      show "∃e. «e : a → a'¬ ∧ map e = t"
      proof
        interpret Ya': yoneda_functor_fixed_object C S setp φ a'
          using a' by (unfold_locales, auto)
        interpret yoneda_lemma_for_hom C S setp φ a a'
          using a a' by (unfold_locales, auto)
        have NT: "natural_transformation Cop.comp S (Y a) (Y a') (Cop_S.Map t)"
          using t a' Y_def Cop_S.Map_dom Cop_S.Map_cod Cop_S.dom_char Cop_S.cod_char
                Cop_S.in_homE Cop_S.arrE
          by metis
        hence 1: "E (Cop_S.Map t) ∈ Hom.set (a, a')"
          using Eτ_mapsto ide_a ide_a' Hom.set_map by simp
        moreover have "map (ψ (a, a') (E (Cop_S.Map t))) = t"
        proof (intro Cop_S.arr_eqI)
          have 2: "«map (ψ (a, a') (E (Cop_S.Map t))) : map a →_[Cop,S] map a'¬"
            using 1 ide_a ide_a' Hom.ψ_mapsto [of a a'] by blast
          show "Cop_S.arr t" using t by blast
          show "Cop_S.arr (map (ψ (a, a') (E (Cop_S.Map t))))" using 2 by blast
          show 3: "Cop_S.Map (map (ψ (a, a') (E (Cop_S.Map t)))) = Cop_S.Map t"
            using NT 1 Y_def T_is_surjection app_T_equals Eτ_mapsto by metis
          show 4: "Cop_S.Dom (map (ψ (a, a') (E (Cop_S.Map t)))) = Cop_S.Dom t"
            using t 2 functor_axioms Cop_S.Map_dom by (metis Cop_S.in_homE)
          show "Cop_S.Cod (map (ψ (a, a') (E (Cop_S.Map t)))) = Cop_S.Cod t"
            using 2 3 4 t Cop_S.Map_cod by (metis Cop_S.in_homE)
        qed
        ultimately show "«ψ (a, a') (E (Cop_S.Map t)) : a → a'¬ ∧
                         map (ψ (a, a') (E (Cop_S.Map t))) = t"
          using ide_a ide_a' Hom.ψ_mapsto by auto
      qed
    qed

    lemma is_full_functor:
    shows "full_functor C Cop_S.comp map"
      ..

    sublocale fully_faithful_functor C Cop_S.comp map ..

  end

end