Yoneda Lemma

Category3.thy

definition (in Category) Iso where
  "Iso f g ≡ (f ∘ g ≈ id (dom g)) & (g ∘ f ≈ id (dom f))"

definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where
  "𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. f ∈ Hom[𝒞][A,B] & g ∈ Hom[𝒞][B,A] & Category.Iso 𝒞 f g)"

record 'c setmap =
  setdom :: "'c set"
  setcod :: "'c set"
  setfunction :: "'c ⇒ 'c"

definition setmap where
  "setmap f ≡ (∀x. x∈setdom f ⟶ setfunction f x ∈ setcod f)"

definition setmap_eq where
  "setmap_eq f g ≡ setmap f & setmap g & setdom f = setdom g & setcod f = setcod g & (∀ x ∈ setdom f. setfunction f x = setfunction g x)"

definition Set where
  "Set ≡ ⦇
    Obj = UNIV,
    Arr = {f. setmap f},
    Dom = setdom,
    Cod = setcod,
    Id = (λX. ⦇ setdom = X, setcod = X, setfunction = λx. x ⦈),
    comp = (λg f. ⦇ setdom = setdom f, setcod = setcod g, setfunction = λx. setfunction g (setfunction f x) ⦈),
    eq = setmap_eq
  ⦈"

lemma Set_category: "Category Set"
proof (auto simp add: Category_def Set_def)
  fix X :: "'a set"
  show "setmap ⦇setdom = X, setcod = X, setfunction = λx. x⦈" by (simp add: setmap_def)
next
  fix f g :: "'a setmap"
  assume a: "setmap f" "setmap g" "setcod f = setdom g"
  show "setmap ⦇setdom = setdom f, setcod = setcod g, setfunction = λx. setfunction g (setfunction f x)⦈"
    apply (simp add: setmap_def)
    using a(1) a(3) a(2) apply (auto simp add: setmap_def)
    done
next
  show "equiv (Collect setmap) {(x, y). setmap_eq x y}"
    apply (rule equivI)
      apply (rule refl_onI, auto simp add: setmap_eq_def)
      apply (rule symI, auto)
      apply (simp add: transp_trans [symmetric], rule transpI, auto)
    done
next
  fix f :: "'a setmap"
  assume a: "setmap f"
  thus "setmap_eq ⦇setdom = setdom f, setcod = setcod f, setfunction = setfunction f⦈ f"
    by (simp add: setmap_eq_def setmap_def)
next
  fix f g h :: "'a setmap"
  assume a: "setmap f" "setmap g" "setmap h" "setcod f = setdom g" "setcod g = setdom h"
  show "setmap_eq
        ⦇setdom = setdom f, setcod = setcod h, setfunction = λx. setfunction h (setfunction g (setfunction f x))⦈
        ⦇setdom = setdom f, setcod = setcod h, setfunction = λx. setfunction h (setfunction g (setfunction f x))⦈"
    apply (simp add: setmap_eq_def setmap_def)
    using a apply (simp add: setmap_def)
    done
next
  fix f g h i :: "'a setmap"
  assume a: "setmap f" "setmap g" "setmap h" "setmap i" "setmap_eq f g" "setmap_eq h i" "setcod h = setdom f"
  show "setmap_eq
        ⦇setdom = setdom h, setcod = setcod f, setfunction = λx. setfunction f (setfunction h x)⦈
        ⦇setdom = setdom i, setcod = setcod g, setfunction = λx. setfunction g (setfunction i x)⦈"
    proof (auto simp add: setmap_eq_def setmap_def)
      fix x
      {
        assume "x ∈ setdom h"
        hence "setfunction h x ∈ setcod h"
          using a(3) by (simp add: setmap_def)
        thus "setfunction f (setfunction h x) ∈ setcod f"
          using a(1) by (simp add: a(7) setmap_def)
      }
      {
        assume "x ∈ setdom i"
        hence "setfunction i x ∈ setdom g"
          using a by (simp add: setmap_def setmap_eq_def)
        thus "setfunction g (setfunction i x) ∈ setcod g"
          using a by (simp add: setmap_def setmap_eq_def)
      }
      {
        assume "x ∈ setdom h" thus "x ∈ setdom i"
          using a by (simp add: setmap_def setmap_eq_def)
      }
      {
        assume "x ∈ setdom i" thus "x ∈ setdom h"
          using a by (simp add: setmap_def setmap_eq_def)
      }
      {
        assume "x ∈ setcod f" thus "x ∈ setcod g"
          using a by (simp add: setmap_def setmap_eq_def)
      }
      {
        assume "x ∈ setcod g" thus "x ∈ setcod f"
          using a by (simp add: setmap_def setmap_eq_def)
      }
      {
        assume "x ∈ setdom h" thus "setfunction f (setfunction h x) = setfunction g (setfunction i x)"
          using a by (simp add: setmap_def setmap_eq_def)
      }
    qed
qed


record ('o,'a,'c,'o2,'a2,'d) Functor =
  domCat :: "('o,'a,'c) Category_scheme"
  codCat :: "('o2,'a2,'d) Category_scheme"
  fobj :: "'o ⇒ 'o2"
  fmap :: "'a ⇒ 'a2"

locale Functor =
  fixes F :: "('o,'a,'c,'o2,'a2,'d,'f) Functor_scheme" (structure)

  assumes dom_category: "Category (domCat F)"
  and cod_category: "Category (codCat F)"
  and obj_mapping: "X ∈ Obj (domCat F) ⟹ fobj F X ∈ Obj (codCat F)"
  and arr_mapping: "f ∈ Hom[domCat F][A,B] ⟹ fmap F f ∈ Hom[codCat F][fobj F A,fobj F B]"

  and preserve_id: "X ∈ Obj (domCat F) ⟹ fmap F (Id (domCat F) X) ≈[codCat F] Id (codCat F) (fobj F X)"
  and preserve_comp:
    "⟦ f ∈ Arr (domCat F); g ∈ Arr (domCat F); Cod (domCat F) f = Dom (domCat F) g ⟧
    ⟹ fmap F (g ∘[domCat F] f) ≈[codCat F] fmap F g ∘[codCat F] fmap F f"

abbreviation Functor_type ("Functor' _ : _ ⟶ _" [81] 90) where
  "Functor' F : 𝒞 ⟶ 𝒟 ≡ Functor F & domCat F = 𝒞 & codCat F = 𝒟"

lemma FunctorE: "Functor' F : 𝒞 ⟶ 𝒟 ⟹
  (Category 𝒞 ⟹
   Category 𝒟 ⟹
   (X ∈ Obj 𝒞 ⟹ fobj F X ∈ Obj 𝒟) ⟹
   (f ∈ Hom[𝒞][A,B] ⟹ fmap F f ∈ Hom[𝒟][fobj F A,fobj F B]) ⟹ thesis) ⟹ thesis"
by (auto simp add: Functor_def)

record ('o,'a,'c,'o2,'a2,'d,'f,'f2) Nat =
  domFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor"
  codFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor"
  component :: "'o ⇒ 'a2"

locale Nat =
  fixes η :: "('o,'a,'c,'o2,'a2,'d,'f,'f2,'n) Nat_scheme"

  assumes same_dom: "domCat (domFunctor η) = domCat (codFunctor η)"
  and same_cod: "codCat (domFunctor η) = codCat (codFunctor η)"
  and dom_functor: "Functor' (domFunctor η) : domCat (domFunctor η) ⟶ codCat (domFunctor η)"
  and cod_functor: "Functor' (codFunctor η) : domCat (codFunctor η) ⟶ codCat (codFunctor η)"
  and component_mapping: "X ∈ Obj (domCat (domFunctor η))
    ⟹ component η X ∈ Hom[codCat (domFunctor η)][fobj (domFunctor η) X, fobj (codFunctor η) X]"
  and naturality: "⟦ f ∈ Hom[domCat (domFunctor η)][A,B]; A ∈ Obj (domCat (domFunctor η)); B ∈ Obj (domCat (domFunctor η)) ⟧
    ⟹ (component η B ∘[codCat (domFunctor η)] fmap (domFunctor η) f) ≈[codCat (domFunctor η)]
        (fmap (codFunctor η) f ∘[codCat (domFunctor η)] component η A)"

abbreviation Nat_type ("Nat' _ : _ ⟶ _" [81] 90) where
  "Nat' η : F ⟶ G ≡ Nat η & Nat.domFunctor η = F & Nat.codFunctor η = G"

lemma NatE: "Nat' η : F ⟶ G ⟹
  (Functor' F : domCat F ⟶ codCat F ⟹
   Functor' G : domCat G ⟶ codCat G ⟹
   domCat F = domCat G ⟹ codCat F = codCat G ⟹
   (X ∈ Obj (domCat F) ⟹ component η X ∈ Hom[codCat F][fobj F X,fobj G X]) ⟹
   (f ∈ Hom[domCat F][A,B] ⟹ A ∈ Obj (domCat F) ⟹ B ∈ Obj (domCat F) ⟹ (component η B ∘[codCat F] fmap F f) ≈[codCat F] (fmap G f ∘[codCat F] component η A)) ⟹
  thesis) ⟹ thesis"
by (auto simp add: Nat_def)

lemma NatE_naturality:
  "⟦ Nat' η : F ⟶ G; f ∈ Hom[domCat F][A,B]; A ∈ Obj (domCat F); B ∈ Obj (domCat F) ⟧ ⟹ (component η B ∘[codCat F] fmap F f) ≈[codCat F] (fmap G f ∘[codCat F] component η A)"
by (rule NatE, auto)

lemma NatI:
  assumes "Functor' F : 𝒞 ⟶ 𝒟" "Functor' G : 𝒞 ⟶ 𝒟" "domFunctor η = F" "codFunctor η = G"
  and "⋀X. X ∈ Obj 𝒞 ⟹ component η X ∈ Hom[𝒟][fobj F X,fobj G X]"
  and "⋀f A B. ⟦ f ∈ Hom[𝒞][A,B]; A ∈ Obj 𝒞; B ∈ Obj 𝒞 ⟧
    ⟹ ((component η B ∘[𝒟] fmap F f) ≈[𝒟] fmap G f ∘[𝒟] component η A)"
  shows "Nat' η : F ⟶ G"
by (rule, auto simp add: Nat_def assms)

definition idNat where
  "idNat F ≡ ⦇ domFunctor = F, codFunctor = F, component = λX. Id (codCat F) (fobj F X) ⦈"

lemma idNat_is_Nat:
  assumes "Functor' F : 𝒞 ⟶ 𝒟"
  shows "Nat' (idNat F) : F ⟶ F"
proof (simp add: Nat_def idNat_def, auto simp add: assms)
  have D_cat: "Category 𝒟" by (rule FunctorE [OF assms], simp)

  {
    fix X
    assume "X ∈ Obj 𝒞"
    then have FX_in: "fobj F X ∈ Obj 𝒟"
      by (metis assms Functor.obj_mapping)
    show "id⇘𝒟⇙ fobj F X ∈ Hom[𝒟][fobj F X,fobj F X]"
      apply (rule CategoryE [OF D_cat])
      using FX_in by auto
  }
  {
    fix f A B
    assume "f ∈ Hom[𝒞][A,B]"
    then have Ff_in: "fmap F f ∈ Hom[𝒟][fobj F A, fobj F B]"
      by (metis assms Functor.arr_mapping)
    show "((id⇘𝒟⇙ fobj F B) ∘[𝒟] fmap F f) ≈[𝒟] (fmap F f ∘[𝒟] (id⇘𝒟⇙ fobj F A))" (is "?L ≈[_] ?R")
      proof-
        have "?L ≈[𝒟] fmap F f"
          by (rule CategoryE_left_id, rule D_cat, rule Ff_in)
        moreover have "fmap F f ≈[𝒟] ?R"
          using CategoryE_right_id [OF D_cat Ff_in]
          by (rule Category.eq_sym [OF D_cat])
        ultimately
          show ?thesis by (rule Category.eq_trans [OF D_cat])
      qed
  }
qed

definition compNat ("_ ∘[Nat] _") where
  "compNat η ε ≡ ⦇
    domFunctor = Nat.domFunctor ε, codFunctor = Nat.codFunctor η,
    component = λX. component η X ∘[codCat (Nat.domFunctor η)] component ε X
  ⦈"

lemma compNat_nat:
  assumes η_nat: "Nat' η : G ⟶ H"
  and     ε_nat: "Nat' ε : F ⟶ G"
  shows   "Nat' (η ∘[Nat] ε) : F ⟶ H"
apply (rule NatI)
apply (rule NatE [OF ε_nat], simp)
apply (rule NatE [OF η_nat], simp)
apply (simp add: compNat_def, simp add: ε_nat)
apply (simp add: compNat_def, simp add: η_nat)
apply (simp add: compNat_def, simp add: assms)
proof-
  have codG_cat: "Category (codCat G)"
    apply (rule NatE [OF η_nat])
    apply (metis FunctorE)
    done
  have codH_cat: "Category (codCat H)"
    apply (rule NatE [OF η_nat])
    apply (metis FunctorE)
    done
  have F_functor: "Functor' F : domCat F ⟶ codCat F"
    by (rule NatE [OF ε_nat], simp)
  have G_functor: "Functor' G : domCat F ⟶ codCat F"
    by (rule NatE [OF ε_nat], simp)
  have H_functor: "Functor' H : domCat G ⟶ codCat G"
    by (rule NatE [OF η_nat], simp)

  have codGH: "codCat G = codCat H"
    by (rule NatE [OF η_nat], auto)

  {
    fix X
    assume X_in: "X ∈ Obj (domCat G)"
    have 1: "component η X ∈ Hom[codCat H][fobj G X,fobj H X]"
      apply (rule NatE [OF η_nat])
      using X_in by auto
    have 2: "component ε X ∈ Hom[codCat G][fobj F X,fobj G X]"
      apply (rule NatE [OF ε_nat])
      using X_in by auto
    show "(component η X ∘[codCat G] component ε X) ∈ Hom[codCat G][fobj F X,fobj H X]"
      apply (rule NatE [OF η_nat], simp)
      by (metis CategoryE codG_cat 1 2)
  }
  {
    fix f A B
    assume f_in: "f ∈ Hom[domCat G][A,B]"
    and A_in: "A ∈ Obj (domCat G)"
    and B_in: "B ∈ Obj (domCat G)"
    show "(component (η ∘[Nat] ε) B ∘[codCat G] fmap F f) ≈[codCat G] (fmap H f ∘[codCat G] component (η ∘[Nat] ε) A)" (is "?L ≈[_] ?R")
      proof-
        have 1: "component η B ∈ Hom[codCat G][fobj G B, fobj H B]"
          apply (rule NatE [OF η_nat]) using B_in by auto
        have 11: "component η A ∈ Hom[codCat G][fobj G A, fobj H A]"
          apply (rule NatE [OF η_nat]) using A_in by auto
        have 2: "component ε B ∈ Hom[codCat G][fobj F B, fobj G B]"
          apply (rule NatE [OF ε_nat]) using B_in by auto
        have 21: "component ε A ∈ Hom[codCat G][fobj F A, fobj G A]"
          apply (rule NatE [OF ε_nat]) using A_in by auto
        have 3: "fmap F f ∈ Hom[codCat G][fobj F A, fobj F B]"
          apply (rule NatE [OF ε_nat], simp)
          apply (rule FunctorE [OF F_functor])
          using f_in by auto
        have 4: "fmap G f ∈ Hom[codCat G][fobj G A, fobj G B]"
          apply (rule NatE [OF ε_nat], simp)
          apply (rule FunctorE [OF G_functor])
          using f_in by auto
        have 41: "fmap G f ∈ Hom[codCat H][fobj G A, fobj G B]"
          apply (rule NatE [OF η_nat])
          using 4 by auto
        have 5: "fmap H f ∈ Hom[codCat H][fobj H A, fobj H B]"
          apply (rule NatE [OF η_nat], simp)
          apply (rule FunctorE [OF H_functor])
          using f_in by auto

        have "?L ≈[codCat G] (component η B ∘[codCat G] component ε B) ∘[codCat G] fmap F f"
          apply (simp add: compNat_def η_nat)
          apply (rule CategoryE_refl [OF codG_cat CategoryE_comp_exist [OF codG_cat 3 CategoryE_comp_exist [OF codG_cat 2 1]]])
          done
        moreover have "… ≈[codCat G] component η B ∘[codCat G] (component ε B ∘[codCat G] fmap F f)"
          apply (rule CategoryE [OF codG_cat])
          using 1 2 3 by auto
        ultimately
          have a: "?L ≈[codCat G] component η B ∘[codCat G] (component ε B ∘[codCat G] fmap F f)"
            by (rule Category.eq_trans [OF codG_cat])

        have "… ≈[codCat G] component η B ∘[codCat G] (fmap G f ∘[codCat G] component ε A)"
          apply (rule CategoryE_eq_comp [OF codG_cat 1 1])
          apply (rule CategoryE_comp_exist [OF codG_cat 3 2])
          apply (rule CategoryE_comp_exist [OF codG_cat 21 4])
          apply (rule CategoryE_refl [OF codG_cat 1])
          defer
          using CategoryE_comp_exist [OF codG_cat 3 2] 1 apply (simp add: hom_def)
          proof-
            have 1: "codCat F = codCat G" by (rule NatE [OF ε_nat], auto)
            have 2: "domCat F = domCat G" by (rule NatE [OF ε_nat], auto)
            show "(component ε B ∘[codCat G] fmap F f) ≈[codCat G] (fmap G f ∘[codCat G] component ε A)"
              apply (simp add: 1 [symmetric])
              apply (rule NatE_naturality [OF ε_nat])
              using f_in A_in B_in by (auto simp add: 2)
          qed
        moreover have "… ≈[codCat G] (component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A"
          by (metis "1" "21" "4" Category.eq_sym CategoryE_assoc codG_cat)
        ultimately
          have b: "(component η B ∘[codCat G] (component ε B ∘[codCat G] fmap F f)) ≈[codCat G] (component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A"
            by (rule Category.eq_trans [OF codG_cat])

        have "… ≈[codCat G] (fmap H f ∘[codCat G] component η A) ∘[codCat G] component ε A"
          apply (rule CategoryE_eq_comp [OF codG_cat])
          apply (rule CategoryE_comp_exist [OF codG_cat 4 1])
          apply (rule CategoryE_comp_exist [OF codG_cat 11]) using 5 apply (simp add: codGH)
          apply (rule 21, rule 21)
          apply (rule NatE_naturality [OF η_nat f_in A_in B_in])
          apply (rule CategoryE_refl [OF codG_cat 21])
          using CategoryE_comp_exist [OF codG_cat 4 1] 21 apply (simp add: hom_def)
          done
        moreover have "… ≈[codCat G] fmap H f ∘[codCat G] (component η A ∘[codCat G] component ε A)"
          using CategoryE_assoc codG_cat by (metis "11" "21" "5" H_functor)
        ultimately
          have c: "((component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A) ≈[codCat G] fmap H f ∘[codCat G] (component η A ∘[codCat G] component ε A)"
            by (rule Category.eq_trans [OF codG_cat])

        have d: "… ≈[codCat G] ?R"
          apply (simp add: compNat_def η_nat)
          apply (rule CategoryE_refl [OF codG_cat CategoryE_comp_exist [OF codG_cat CategoryE_comp_exist [OF codG_cat 21 11]]])
          using 5 by (simp add: codGH)
        show ?thesis
          proof-
            have 1: "?L ≈[codCat G] (component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A" by (rule Category.eq_trans [OF codG_cat a b])
            have 2: "((component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A) ≈[codCat G] ?R" by (rule Category.eq_trans [OF codG_cat c d])
            show ?thesis by (rule Category.eq_trans [OF codG_cat 1 2])
          qed
      qed
  }
qed

definition nat_eq where
  "nat_eq η ε ≡ (∀X ∈ Obj (domCat (domFunctor η)). component η X = component ε X)"

definition FunCat where
  "FunCat 𝒞 𝒟 = ⦇
    Obj = {F. Functor' F : 𝒞 ⟶ 𝒟},
    Arr = {η. ∃F∈{F. Functor' F : 𝒞 ⟶ 𝒟}. ∃G∈{F. Functor' F : 𝒞 ⟶ 𝒟}. Nat' η : F ⟶ G},
    Dom = domFunctor,
    Cod = codFunctor,
    Id = idNat,
    comp = compNat,
    eq = nat_eq
  ⦈"

lemma
  assumes "Category 𝒞" "Category 𝒟"
  shows "Category (FunCat 𝒞 𝒟)"
apply (unfold Category_def)

Yoneda.thy

theory Category
imports Main
begin

no_notation Fun.comp (infixl "∘" 55)

record ('o,'a) Category =
  Obj :: "'o set"
  Arr :: "'a set"
  Dom :: "'a ⇒ 'o" ("domı _" [80] 90)
  Cod :: "'a ⇒ 'o" ("codı _" [80] 90)
  Id :: "'o ⇒ 'a"  ("idı _" [80] 90)
  comp :: "'a ⇒ 'a ⇒ 'a" (infixr "∘ı" 60)

locale Category =
  fixes 𝒞 :: "('o,'a,'c) Category_scheme" (structure)
  assumes dom_obj [intro]: "f ∈ Arr 𝒞 ⟹ dom f ∈ Obj 𝒞"
  and     cod_obj [intro]: "f ∈ Arr 𝒞 ⟹ cod f ∈ Obj 𝒞"
  and     id_exist [intro]: "X ∈ Obj 𝒞 ⟹ id X ∈ Arr 𝒞 & dom (id X) = X & cod (id X) = X"
  and     comp_exist [intro]: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; cod f = dom g ⟧
    ⟹ g ∘ f ∈ Arr 𝒞 & dom (g ∘ f) = dom f & cod (g ∘ f) = cod g"

  and     left_id [simp]: "f ∈ Arr 𝒞 ⟹ id (cod f) ∘ f = f"
  and     right_id [simp]: "f ∈ Arr 𝒞 ⟹ f ∘ id (dom f) = f"
  and     assoc [iff]: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; h ∈ Arr 𝒞; cod f = dom g; cod g = dom h ⟧
    ⟹ (h ∘ g) ∘ f = h ∘ (g ∘ f)"
begin
abbreviation Hom ("_ → _" [70] 100) where
  "Hom A B ≡ {f ∈ Arr 𝒞. dom f = A & cod f = B}"

lemma arr_type [simp]:
  assumes "f ∈ Arr 𝒞" shows "f : (dom f) → (cod f)"
by (metis (mono_tags, lifting) assms mem_Collect_eq)

lemma id_type [simp]:
  assumes "X ∈ Obj 𝒞" shows "id X : X → X"
using assms id_exist by auto

lemma comp_hom [simp]:
  assumes "f : A → B" and "g : B → C"
  shows "g ∘ f : A → C"
using assms comp_exist by auto

lemma assoc_hom [simp]:
  assumes "f : A → B" and "g : B → C" and "h : C → D"
  shows "(h ∘ g) ∘ f = h ∘ (g ∘ f)"
by (metis (mono_tags, lifting) assms assoc mem_Collect_eq)
end

abbreviation comp_category ("_ ∘[_] _" [60] 100) where
  "f ∘[𝒞] g ≡ comp 𝒞 f g"

abbreviation hom_category ("_ -[_]→ _" [70] 100) where
  "a -[𝒞]→ b ≡ Category.Hom 𝒞 a b"

definition opposite ("_ {^op}" 100) where
  "opposite 𝒞 ≡ ⦇
    Obj = Obj 𝒞,
    Arr = Arr 𝒞,
    Dom = Cod 𝒞,
    Cod = Dom 𝒞,
    Id = Id 𝒞,
    comp = (λf g. comp 𝒞 g f)
  ⦈"

lemma opposite_category:
  assumes "Category 𝒞"
  shows "Category (𝒞 {^op})"
unfolding opposite_def Category_def
by (auto simp add: assms Category.cod_obj Category.dom_obj
    Category.id_exist Category.comp_exist
    Category.right_id Category.left_id Category.assoc)

definition (in Category) Iso where
  "Iso f g ≡ f ∘ g = id (dom g) & g ∘ f = id (dom f)"

definition (in Category) Iso_on_objects ("IsoObj _ _") where
  "IsoObj A B ≡ ∃f∈Arr 𝒞. ∃g∈Arr 𝒞. (f : A → B) & (g : B → A) & Iso f g"

definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where
  "𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. (f : A -[𝒞]→ B) & (g : B -[𝒞]→ A) & Category.Iso 𝒞 f g)"

record 'c setmap =
  setdom :: "'c set"
  setcod :: "'c set"
  setfunction :: "'c ⇒ 'c"

definition setmap where
  "setmap f ≡ (∀x. x∈setdom f ⟶ setfunction f x ∈ setcod f)"

axiomatization where
  setmap_eq : "⟦ setmap f; setmap g; setdom f = setdom g; setcod f = setcod g; ∀x∈setdom f. setfunction f x = setfunction g x ⟧
    ⟹ f = g"

definition Set where
  "Set ≡ ⦇
    Obj = UNIV,
    Arr = {f. setmap f},
    Dom = setdom,
    Cod = setcod,
    Id = (λX. ⦇ setdom = X, setcod = X, setfunction = λx. x ⦈),
    comp = (λg f. ⦇ setdom = setdom f, setcod = setcod g, setfunction = λx. setfunction g (setfunction f x) ⦈)
  ⦈"

lemma Set_category: "Category Set"
unfolding Set_def Category_def
apply (simp add: setmap_eq)
by (auto simp add: setmap_def)

record ('o,'a,'c,'o2,'a2,'d) Functor =
  domCat :: "('o,'a,'c) Category_scheme"
  codCat :: "('o2,'a2,'d) Category_scheme"
  fobj :: "'o ⇒ 'o2"
  fmap :: "'a ⇒ 'a2"

locale Functor =
  fixes F :: "('o,'a,'c,'o2,'a2,'d,'f) Functor_scheme" (structure)

  assumes fdom_category [intro]: "Category (domCat F)"
  and     fcod_category [intro]: "Category (codCat F)"
  and     fobj_mapping [intro]: "X ∈ Obj (domCat F) ⟹ fobj F X ∈ Obj (codCat F)"
  and     fmap_mapping [intro]: "f ∈ Arr (domCat F) ⟹ fmap F f ∈ Arr (codCat F)
                                  & Dom (codCat F) (fmap F f) = fobj F (Dom (domCat F) f)
                                  & Cod (codCat F) (fmap F f) = fobj F (Cod (domCat F) f)"

  and     preserve_id [simp]: "X ∈ Obj (domCat F) ⟹ fmap F (Id (domCat F) X) = Id (codCat F) (fobj F X)"
  and     covariant [simp]:
    "⟦ f ∈ Arr (domCat F); g ∈ Arr (domCat F); Cod (domCat F) f = Dom (domCat F) g ⟧
    ⟹ fmap F (g ∘[domCat F] f) = fmap F g ∘[codCat F] fmap F f"
begin
lemma fmap_mapping_hom:
  assumes "f : a -[domCat F]→ b"
  shows "fmap F f : fobj F a -[codCat F]→ fobj F b"
using fmap_mapping [of f] assms by auto

lemma fmap_type:
  assumes "f ∈ Arr (domCat F)"
  shows "fmap F f : fobj F (Dom (domCat F) f) -[codCat F]→ fobj F (Cod (domCat F) f)"
using Category.arr_type assms fmap_mapping by auto
end

abbreviation Functor_type ("Functor' _ : _ ⟶ _" [81] 90) where
  "Functor' F : 𝒞 ⟶ 𝒟 ≡ Functor F & domCat F = 𝒞 & codCat F = 𝒟"

record ('o,'a,'c,'o2,'a2,'d,'f,'f2) Nat =
  domFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor"
  codFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor"
  component :: "'o ⇒ 'a2"

locale Nat =
  fixes η :: "('o,'a,'c,'o2,'a2,'d,'f,'f2,'n) Nat_scheme"

  assumes dom_functor [intro]: "Functor' (domFunctor η) : domCat (domFunctor η) ⟶ codCat (domFunctor η)"
  and     cod_functor [intro]: "Functor' (codFunctor η) : domCat (codFunctor η) ⟶ codCat (codFunctor η)"
  and     same_dom [intro]: "domCat (domFunctor η) = domCat (codFunctor η)"
  and     same_cod [intro]: "codCat (domFunctor η) = codCat (codFunctor η)"
  and     component_mapping [intro]: "X ∈ Obj (domCat (domFunctor η))
    ⟹ component η X : fobj (domFunctor η) X -[codCat (domFunctor η)]→ fobj (codFunctor η) X"

  and     naturality [simp]:
    "f ∈ Arr (domCat (domFunctor η))
    ⟹ (component η (Cod (domCat (domFunctor η)) f) ∘[codCat (domFunctor η)] fmap (domFunctor η) f)
      = (fmap (codFunctor η) f ∘[codCat (domFunctor η)] component η (Dom (domCat (domFunctor η)) f))"
begin
lemma domFunctor_category [intro]:
  assumes "Nat η"
  shows "Category (domCat (domFunctor η)) & Category (codCat (domFunctor η))"
by (metis assms Nat.dom_functor Functor.fdom_category Functor.fcod_category)

lemma codFunctor_category [intro]:
  assumes "Nat η"
  shows "Category (domCat (codFunctor η)) & Category (codCat (codFunctor η))"
by (metis assms Nat.cod_functor Functor.fdom_category Functor.fcod_category)

lemma naturality_hom [intro]:
  assumes "f ∈ Arr (domCat (domFunctor η))"
  shows "⟦ a ∈ Obj (domCat (domFunctor η)); b ∈ Obj (domCat (domFunctor η)); f : a -[domCat (domFunctor η)]→ b ⟧
    ⟹ (component η b ∘[codCat (domFunctor η)] fmap (domFunctor η) f)
      = (fmap (codFunctor η) f ∘[codCat (domFunctor η)] component η a)"
by auto
end

abbreviation Nat_type ("Nat' _ : _ ⟶ _" [81] 90) where
  "Nat' η : F ⟶ G ≡ Nat η & Nat.domFunctor η = F & Nat.codFunctor η = G"

axiomatization where
  nat_eq [iff]: "⟦ Functor' F: 𝒞 ⟶ 𝒟; Functor' G: 𝒞 ⟶ 𝒟; Nat' η: F ⟶ G; Nat' ε: F ⟶ G; (∀X∈Obj 𝒞. component η X = component ε X) ⟧
    ⟹ η = ε"

definition idNat where
  "idNat F ≡ ⦇ domFunctor = F, codFunctor = F, component = λX. Id (codCat F) (fobj F X) ⦈"

lemma idNat_nat:
  assumes "Functor F"
  shows "Nat' (idNat F) : F ⟶ F"
unfolding idNat_def Nat_def apply (auto simp add: assms)
apply (metis Category.id_exist Functor.fcod_category Functor.fobj_mapping assms)
apply (metis Category.id_exist Functor.fcod_category Functor.fobj_mapping assms)
apply (metis Category.id_exist Functor.fcod_category Functor.fobj_mapping assms)
proof-
  fix f
  assume f_in: "f ∈ Arr (domCat F)"
  have codF_cat: "Category (codCat F)" using assms Functor.fcod_category by auto
  have Ff_type: "fmap F f : fobj F (dom⇘domCat F⇙ f) -[codCat F]→ fobj F (cod⇘domCat F⇙ f)"
    using Functor.fmap_type [of F f] assms f_in by auto
  show "((id⇘codCat F⇙ fobj F (cod⇘domCat F⇙ f)) ∘[codCat F] fmap F f) = fmap F f ∘[codCat F] id⇘codCat F⇙ fobj F (dom⇘domCat F⇙ f)"
    proof-
      have "((id⇘codCat F⇙ fobj F (cod⇘domCat F⇙ f)) ∘[codCat F] fmap F f) = fmap F f"
        using Category.left_id codF_cat Ff_type by (metis (mono_tags, lifting) mem_Collect_eq)
      also have "… = fmap F f ∘[codCat F] id⇘codCat F⇙ fobj F (dom⇘domCat F⇙ f)"
        using Category.right_id codF_cat Ff_type by (metis (mono_tags, lifting) mem_Collect_eq)
      finally show ?thesis by auto
    qed
qed

definition compNat ("Nat'[_ ∘ _]") where
  "compNat η ε ≡ ⦇
    domFunctor = Nat.domFunctor ε, codFunctor = Nat.codFunctor η,
    component = λX. Category.comp (codCat (Nat.domFunctor η)) (component η X) (component ε X)
  ⦈"

lemma compNat_nat:
  assumes η_nat: "Nat' η : G ⟶ H"
  and     ε_nat: "Nat' ε : F ⟶ G"
  shows   "Nat' (compNat η ε) : F ⟶ H"
unfolding compNat_def
apply (auto simp add: Nat_def η_nat ε_nat)
using Nat.dom_functor ε_nat apply fastforce
using Nat.cod_functor η_nat apply fastforce
using Nat.same_dom [of η] η_nat Nat.same_dom [of ε] ε_nat apply fastforce
using Nat.same_cod [of η] η_nat Nat.same_cod [of ε] ε_nat apply fastforce
proof -
  def 𝒞 ≡ "domCat F"
  def 𝒟 ≡ "codCat F"
  have F_functor: "Functor' F : 𝒞 ⟶ 𝒟" using Nat.dom_functor [of ε] by (auto simp add: ε_nat 𝒞_def 𝒟_def)
  have G_functor: "Functor' G : 𝒞 ⟶ 𝒟" using Nat.same_dom [of ε] Nat.same_cod [of ε] ε_nat by (metis Nat.dom_functor 𝒞_def 𝒟_def η_nat)
  have H_functor: "Functor' H : 𝒞 ⟶ 𝒟" using Nat.dom_functor [of η] by (metis G_functor Nat.cod_functor Nat.same_cod Nat.same_dom η_nat)
  have C_cat: "Category 𝒞" by (metis Functor.fdom_category F_functor)
  have D_cat: "Category 𝒟" by (metis Functor.fcod_category F_functor)
  {
    fix X
    assume X_in: "X ∈ Obj (domCat F)"
  
    have ηεX_type: "(component η X ∘[codCat G] component ε X) : fobj F X -[codCat F]→ fobj H X"
      using X_in Nat.component_mapping [of η] Nat.component_mapping [of ε]
      apply (auto simp add: η_nat ε_nat)
      apply (auto simp add: G_functor F_functor)
      by (auto simp add: D_cat Category.comp_exist)
    show "(component η X ∘[codCat G] component ε X) ∈ Arr (codCat F)" using ηεX_type by auto
    show "dom⇘codCat F⇙ (component η X ∘[codCat G] component ε X) = fobj F X" using ηεX_type by auto
    show "cod⇘codCat F⇙ (component η X ∘[codCat G] component ε X) = fobj H X" using ηεX_type by auto
  }
  {
    fix f
    assume f_in: "f ∈ Arr (domCat F)"

    show "((component η (cod⇘domCat F⇙ f) ∘[codCat G] component ε (cod⇘domCat F⇙ f)) ∘[codCat F] fmap F f) =
           (fmap H f ∘[codCat F] (component η (dom⇘domCat F⇙ f) ∘[codCat G] component ε (dom⇘domCat F⇙ f)))"
      proof (auto simp add: F_functor G_functor)
        have 1: "component η (cod⇘𝒞⇙ f) : fobj G (cod⇘𝒞⇙ f) -[𝒟]→ fobj H (cod⇘𝒞⇙ f)"
          using Nat.component_mapping [of η] η_nat f_in apply (simp add: F_functor G_functor)
          using C_cat Category.cod_obj by fastforce
        have 2: "component ε (cod⇘𝒞⇙ f) : fobj F (cod⇘𝒞⇙ f) -[𝒟]→ fobj G (cod⇘𝒞⇙ f)"
          using Nat.component_mapping [of ε] ε_nat f_in apply (simp add: F_functor G_functor)
          using C_cat Category.cod_obj by fastforce
        have 3: "fmap F f : fobj F (dom⇘𝒞⇙ f) -[𝒟]→ fobj F (cod⇘𝒞⇙ f)"
          using Functor.fmap_type [of F f] f_in by (simp add: F_functor)
        have 4: "component ε (dom⇘𝒞⇙ f) : fobj F (dom⇘𝒞⇙ f) -[𝒟]→ fobj G (dom⇘𝒞⇙ f)"
          using Nat.component_mapping [of ε] ε_nat f_in apply (simp add: F_functor G_functor)
          using C_cat Category.dom_obj by fastforce
        have 5: "fmap G f : fobj G (dom⇘𝒞⇙ f) -[𝒟]→ fobj G (cod⇘𝒞⇙ f)"
          using Functor.fmap_type [of G f] f_in by (simp add: F_functor G_functor)
        have 6: "component η (dom⇘𝒞⇙ f) : fobj G (dom⇘𝒞⇙ f) -[𝒟]→ fobj H (dom⇘𝒞⇙ f)"
          using Nat.component_mapping [of η] η_nat f_in apply (simp add: F_functor G_functor)
          using C_cat Category.dom_obj by fastforce
        have 7: "fmap H f : fobj H (dom⇘𝒞⇙ f) -[𝒟]→ fobj H (cod⇘𝒞⇙ f)"
          using Functor.fmap_type [of H f] f_in by (simp add: F_functor H_functor)

        have "((component η (cod⇘𝒞⇙ f) ∘[𝒟] component ε (cod⇘𝒞⇙ f)) ∘[𝒟] fmap F f)
              = component η (cod⇘𝒞⇙ f) ∘[𝒟] (component ε (cod⇘𝒞⇙ f) ∘[𝒟] fmap F f)"
          using Category.assoc [OF D_cat] 1 2 3 by auto
        also have "… = component η (cod⇘𝒞⇙ f) ∘[𝒟] (fmap G f ∘[𝒟] component ε (dom⇘𝒞⇙ f))"
          using Nat.naturality [of ε f] f_in by (simp add: ε_nat F_functor)
        also have "… = (component η (cod⇘𝒞⇙ f) ∘[𝒟] fmap G f) ∘[𝒟] component ε (dom⇘𝒞⇙ f)"
          using Category.assoc [OF D_cat] 1 4 5 by auto
        also have "… = (fmap H f ∘[𝒟] component η (dom⇘𝒞⇙ f)) ∘[𝒟] component ε (dom⇘𝒞⇙ f)"
          using Nat.naturality [of η f] f_in by (simp add: η_nat F_functor G_functor)
        also have "… = fmap H f ∘[𝒟] (component η (dom⇘𝒞⇙ f) ∘[𝒟] component ε (dom⇘𝒞⇙ f))"
          using Category.assoc [OF D_cat] 4 6 7 by auto
        finally
          show "((component η (cod⇘𝒞⇙ f) ∘[𝒟] component ε (cod⇘𝒞⇙ f)) ∘[𝒟] fmap F f) =
                fmap H f ∘[𝒟] (component η (dom⇘𝒞⇙ f) ∘[𝒟] component ε (dom⇘𝒞⇙ f))"
            by auto
      qed
  }
qed

definition FunCat where
  "FunCat 𝒞 𝒟 = ⦇
    Obj = {F. Functor' F : 𝒞 ⟶ 𝒟},
    Arr = {η. ∃F∈{F. Functor' F : 𝒞 ⟶ 𝒟}. ∃G∈{F. Functor' F : 𝒞 ⟶ 𝒟}. Nat' η : F ⟶ G},
    Dom = domFunctor,
    Cod = codFunctor,
    Id = idNat,
    comp = compNat
  ⦈"

lemma FunCat_category:
  assumes C_cat: "Category 𝒞" and D_cat: "Category 𝒟"
  shows "Category (FunCat 𝒞 𝒟)" (is "Category ?FC")
proof
  fix f
  assume f_in: "f ∈ Arr ?FC"
  show "dom⇘FunCat 𝒞 𝒟⇙ f ∈ Obj (FunCat 𝒞 𝒟)" using f_in unfolding FunCat_def by auto
  show "cod⇘FunCat 𝒞 𝒟⇙ f ∈ Obj (FunCat 𝒞 𝒟)" using f_in unfolding FunCat_def by auto
next
  fix F
  assume F_in: "F ∈ Obj ?FC"
  show "id⇘FunCat 𝒞 𝒟⇙ F ∈ Arr (FunCat 𝒞 𝒟) ∧ dom⇘FunCat 𝒞 𝒟⇙ id⇘FunCat 𝒞 𝒟⇙ F = F ∧ cod⇘FunCat 𝒞 𝒟⇙ id⇘FunCat 𝒞 𝒟⇙ F = F"
    using F_in unfolding FunCat_def by (auto simp add: idNat_nat [of F])
next
  fix f g
  assume 0: "f ∈ Arr ?FC" "g ∈ Arr ?FC" "cod⇘FunCat 𝒞 𝒟⇙ f = dom⇘FunCat 𝒞 𝒟⇙ g"
  then obtain F G H where
    F_functor: "(Functor' F : 𝒞 ⟶ 𝒟)" and G_functor: "(Functor' G : 𝒞 ⟶ 𝒟)" and H_functor: "(Functor' H : 𝒞 ⟶ 𝒟)" and
    f_nat: "(Nat' f : F ⟶ G)" and g_nat: "(Nat' g : G ⟶ H)"
    unfolding FunCat_def by auto
  show "((g ∘[?FC] f) ∈ Arr ?FC) ∧ (dom⇘?FC⇙ (g ∘[?FC] f) = dom⇘?FC⇙ f) ∧ (cod⇘?FC⇙ (g ∘[?FC] f) = cod⇘?FC⇙ g)"
    using compNat_nat [OF g_nat f_nat] unfolding compNat_def apply simp
    unfolding FunCat_def apply simp
    by (auto simp add: compNat_def f_nat g_nat F_functor G_functor H_functor)
next
  fix f
  assume f_in: "f ∈ Arr ?FC"
  hence f_nat: "∃F∈Obj ?FC. ∃G∈Obj ?FC. Nat' f : F ⟶ G" unfolding FunCat_def by auto
  then obtain F G where
    FG: "Functor' F : 𝒞 ⟶ 𝒟" "Functor' G : 𝒞 ⟶ 𝒟" "Nat' f : F ⟶ G"
    unfolding FunCat_def by auto
  show "((id⇘?FC⇙ (cod⇘?FC⇙ f)) ∘[?FC] f) = f"
    unfolding FunCat_def apply auto
    proof (rule_tac nat_eq [of F 𝒞 𝒟 G] , auto simp add: FG)
      show "Category.Nat Nat[idNat G ∘ f]" using compNat_nat [of _ G G f F] FG idNat_nat [of G] by auto
      show "domFunctor Nat[idNat G ∘ f] = F" unfolding compNat_def by (auto simp add: FG)
      show "codFunctor Nat[idNat G ∘ f] = G" unfolding compNat_def idNat_def by auto
      {
        fix X
        assume X_in: "X ∈ Obj 𝒞"
        show "component Nat[idNat G ∘ f] X = component f X"
          unfolding compNat_def idNat_def
          proof (auto simp add: FG)
            have "component f X : fobj F X -[𝒟]→ fobj G X" using Nat.component_mapping [of f X] FG X_in by fastforce
            thus "((id⇘𝒟⇙ fobj G X) ∘[𝒟] component f X) = component f X" using Category.left_id [OF D_cat] by fastforce
          qed
      }
    qed
  show "(f ∘[?FC] id⇘?FC⇙ dom⇘?FC⇙ f) = f"
    unfolding FunCat_def apply simp
    proof (rule_tac nat_eq , auto simp add: FG)
      show "Category.Nat Nat[f ∘ idNat F]" using compNat_nat [of f F G _ F] idNat_nat FG by auto
      show "domFunctor Nat[f ∘ idNat F] = F" unfolding compNat_def idNat_def by auto
      show "codFunctor Nat[f ∘ idNat F] = G" unfolding compNat_def by (auto simp add: FG)
      {
        fix X
        assume X_in: "X ∈ Obj 𝒞"
        show "component Nat[f ∘ idNat F] X = component f X"
          unfolding compNat_def idNat_def
          proof (auto simp add: FG)
            have "component f X : fobj F X -[𝒟]→ fobj G X" using Nat.component_mapping [of f X] FG X_in by fastforce
            thus "(component f X ∘[𝒟] (id⇘𝒟⇙ fobj F X)) = component f X" using Category.right_id [OF D_cat] by fastforce
          qed
      }
    qed
next
  fix f g h
  assume "f ∈ Arr ?FC" "g ∈ Arr ?FC" "h ∈ Arr ?FC" "cod⇘FunCat 𝒞 𝒟⇙ f = dom⇘FunCat 𝒞 𝒟⇙ g" "cod⇘FunCat 𝒞 𝒟⇙ g = dom⇘FunCat 𝒞 𝒟⇙ h"
  then obtain F G H I where
    FGHI: "Functor' F: 𝒞 ⟶ 𝒟" "Functor' G: 𝒞 ⟶ 𝒟" "Functor' H: 𝒞 ⟶ 𝒟" "Functor' I: 𝒞 ⟶ 𝒟" and
    fgh_nat: "Nat' f : F ⟶ G" "Nat' g : G ⟶ H" "Nat' h : H ⟶ I"
    unfolding FunCat_def by auto
  have 1: "Nat' ((h ∘[FunCat 𝒞 𝒟] g) ∘[FunCat 𝒞 𝒟] f) : F ⟶ I"
    unfolding FunCat_def by (auto simp add: compNat_nat fgh_nat)
  have 2: "Nat' (h ∘[FunCat 𝒞 𝒟] (g ∘[FunCat 𝒞 𝒟] f)) : F ⟶ I"
    unfolding FunCat_def by (auto simp add: compNat_nat fgh_nat)
  show "((h ∘[FunCat 𝒞 𝒟] g) ∘[FunCat 𝒞 𝒟] f) = h ∘[FunCat 𝒞 𝒟] (g ∘[FunCat 𝒞 𝒟] f)"
    apply (rule_tac nat_eq [of F 𝒞 𝒟 I])
    apply (auto simp add: FGHI(1) FGHI(4))
    apply (auto simp add: 1 2)
    proof-
      fix X
      assume X_in: "X ∈ Obj 𝒞"
      show "component ((h ∘[FunCat 𝒞 𝒟] g) ∘[FunCat 𝒞 𝒟] f) X = component (h ∘[FunCat 𝒞 𝒟] (g ∘[FunCat 𝒞 𝒟] f)) X"
        unfolding FunCat_def apply simp
        unfolding compNat_def apply simp
        proof (simp add: fgh_nat FGHI)
          have 1: "component h X : fobj H X -[𝒟]→ fobj I X" using fgh_nat(3) Nat.component_mapping [of h X] X_in FGHI by auto
          have 2: "component g X : fobj G X -[𝒟]→ fobj H X" using fgh_nat(2) Nat.component_mapping [of g X] X_in FGHI by auto
          have 3: "component f X : fobj F X -[𝒟]→ fobj G X" using fgh_nat(1) Nat.component_mapping [of f X] X_in FGHI by auto
          show "((component h X ∘[𝒟] component g X) ∘[𝒟] component f X) = component h X ∘[𝒟] (component g X ∘[𝒟] component f X)"
            using Category.assoc [OF D_cat] 1 2 3 by auto
        qed
    qed
qed

definition Presheaf ("PSh(_)") where
  "PSh(𝒞) ≡ FunCat (𝒞 {^op}) Set"

definition contraHom ("Hom{_}[-,_]") where
  "Hom{𝒞}[-,r] ≡ ⦇
    domCat = 𝒞 {^op},
    codCat = Set,
    fobj = λx. Category.Hom 𝒞 x r,
    fmap = λf. ⦇ setdom = Category.Hom 𝒞 (Cod 𝒞 f) r, setcod = Category.Hom 𝒞 (Dom 𝒞 f) r, setfunction = λu. u ∘[𝒞] f ⦈
  ⦈"

lemma contraHom_functor:
  assumes C_cat: "Category 𝒞" and r_in: "r ∈ Obj 𝒞"
  shows "Functor' Hom{𝒞}[-,r] : 𝒞 {^op} ⟶ Set"
unfolding Functor_def contraHom_def apply simp
apply (auto simp add: C_cat opposite_category)
apply (auto simp add: Set_category)
proof -
  fix X assume "X ∈ Obj (𝒞 {^op})" show "Category.Hom 𝒞 X r ∈ Obj Set" unfolding Set_def by auto
next
  fix f assume "f ∈ Arr (𝒞 {^op})"
  thus "⦇setdom = Category.Hom 𝒞 (cod⇘𝒞⇙ f) r, setcod = Category.Hom 𝒞 (dom⇘𝒞⇙ f) r, setfunction = λu. u ∘[𝒞] f⦈ ∈ Arr Set"
    unfolding Set_def setmap_def opposite_def by (auto simp add: Category.comp_exist C_cat)
next
  fix f x
  assume assm: "f ∈ Arr (𝒞 {^op})" "x ∈ dom⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] f⦈"
  show "x ∈ Arr 𝒞" using assm unfolding Set_def by auto
  show "dom⇘𝒞⇙ x = dom⇘𝒞 {^op}⇙ f" using assm unfolding opposite_def Set_def by auto
  show "cod⇘𝒞⇙ x = r" using assm unfolding Set_def by auto
next
  fix f x
  assume "f ∈ Arr (𝒞 {^op})" "x ∈ Arr 𝒞" "dom⇘𝒞⇙ x = dom⇘𝒞 {^op}⇙ f" "r = cod⇘𝒞⇙ x"
  thus "x ∈ dom⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setfunction = λu. u ∘[𝒞] f⦈"
    unfolding Set_def opposite_def by auto
next
  fix f x
  assume assm: "f ∈ Arr (𝒞 {^op})" "x ∈ cod⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] f⦈"
  show "x ∈ Arr 𝒞" using assm unfolding Set_def by auto
  show "dom⇘𝒞⇙ x = cod⇘𝒞 {^op}⇙ f" using assm unfolding Set_def opposite_def by auto
  show "cod⇘𝒞⇙ x = r" using assm unfolding Set_def opposite_def by auto
next
  fix f x
  assume assm: "f ∈ Arr (𝒞 {^op})" "x ∈ Arr 𝒞" "dom⇘𝒞⇙ x = cod⇘𝒞 {^op}⇙ f" "r = cod⇘𝒞⇙ x"
  show "x ∈ cod⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setfunction = λu. u ∘[𝒞] f⦈"
    using assm unfolding Set_def opposite_def by auto
next
  fix X
  assume "X ∈ Obj (𝒞 {^op})"
  thus "⦇setdom = (cod⇘𝒞⇙ (id⇘𝒞 {^op}⇙ X)) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ (id⇘𝒞 {^op}⇙ X)) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] (id⇘𝒞 {^op}⇙ X)⦈ = id⇘Set⇙ (X -[𝒞]→ r)"
    apply (rule_tac setmap_eq)
    apply (auto simp add: opposite_def setmap_def)
    apply (auto simp add: C_cat Category.id_exist Category.right_id Category.left_id)
    by (auto simp add: Set_def)
next
  fix f g
  assume "f ∈ Arr (𝒞 {^op})" "g ∈ Arr (𝒞 {^op})" "cod⇘𝒞 {^op}⇙ f = dom⇘𝒞 {^op}⇙ g"
  thus "⦇setdom = (cod⇘𝒞⇙ (g ∘[𝒞 {^op}] f)) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ (g ∘[𝒞 {^op}] f)) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] (g ∘[𝒞 {^op}] f)⦈ =
        ⦇setdom = (cod⇘𝒞⇙ g) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ g) -[𝒞]→ r,
          setfunction = λu. u ∘[𝒞] g⦈ ∘[Set] ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] f⦈"
    unfolding Set_def opposite_def
    apply (rule_tac setmap_eq)
    apply (auto simp add: setmap_def)
    by (auto simp add: C_cat Category.assoc Category.comp_exist)
qed

definition contraHomNat ("HomNat{_}[-,_]") where
  "HomNat{𝒞}[-,f] ≡ ⦇
    domFunctor = Hom{𝒞}[-,Dom 𝒞 f],
    codFunctor = Hom{𝒞}[-,Cod 𝒞 f],
    component = λx. ⦇ setdom = Category.Hom 𝒞 x (Dom 𝒞 f), setcod = Category.Hom 𝒞 x (Cod 𝒞 f), setfunction = λu. f ∘[𝒞] u ⦈
  ⦈"

lemma contraHomNat_nat:
  assumes C_cat: "Category 𝒞" "f ∈ Arr 𝒞"
  shows "Nat' HomNat{𝒞}[-,f] : Hom{𝒞}[-,Dom 𝒞 f] ⟶ Hom{𝒞}[-,Cod 𝒞 f]"
unfolding Nat_def contraHomNat_def
apply (auto simp add: contraHom_functor assms Category.dom_obj Category.cod_obj)
proof -
  fix X
  assume "X ∈ Obj (𝒞 {^op})" thus "⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈ ∈ Arr Set"
    unfolding Set_def setmap_def by (auto simp add: assms Category.comp_exist)
next
  fix X x
  assume "X ∈ Obj (𝒞 {^op})" "x ∈ dom⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈"
  thus "x ∈ fobj Hom{𝒞}[-,dom⇘𝒞⇙ f] X" unfolding opposite_def Set_def contraHom_def by auto
next
  fix X x
  assume "X ∈ Obj (𝒞 {^op})" "x ∈ fobj Hom{𝒞}[-,dom⇘𝒞⇙ f] X"
  thus "x ∈ dom⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈"
    unfolding opposite_def contraHom_def Set_def by auto
next
  fix X x
  assume "X ∈ Obj (𝒞 {^op})" "x ∈ cod⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈"
  thus "x ∈ fobj Hom{𝒞}[-,cod⇘𝒞⇙ f] X"
    unfolding opposite_def contraHom_def Set_def by auto
next
  fix X x
  assume "X ∈ Obj (𝒞 {^op})" "x ∈ fobj Hom{𝒞}[-,cod⇘𝒞⇙ f] X"
  thus "x ∈ cod⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈"
    unfolding opposite_def contraHom_def Set_def by auto
next
  fix fa
  assume "fa ∈ Arr (𝒞 {^op})"
  thus "(⦇setdom = (cod⇘𝒞 {^op}⇙ fa) -[𝒞]→ dom⇘𝒞⇙ f, setcod = (cod⇘𝒞 {^op}⇙ fa) -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈
            ∘[Set] (fmap Hom{𝒞}[-,dom⇘𝒞⇙ f] fa)) =
          fmap Hom{𝒞}[-,cod⇘𝒞⇙ f] fa
            ∘[Set] ⦇setdom = (dom⇘𝒞 {^op}⇙ fa) -[𝒞]→ dom⇘𝒞⇙ f, setcod = (dom⇘𝒞 {^op}⇙ fa) -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈"
    apply (rule_tac setmap_eq)
    unfolding setmap_def opposite_def Set_def contraHom_def
    apply (auto simp add: assms Category.comp_exist)
    apply (auto simp add: assms Category.assoc)
    done
qed

lemma setmap_functor_fmap:
  assumes "Functor' F : 𝒞 ⟶ Set" "f ∈ Arr 𝒞"
  shows "setmap (fmap F f)"
using assms Functor.fmap_type unfolding Set_def by fastforce

lemma setmap_nat_component:
  assumes "Nat η" "Functor' (domFunctor η) : 𝒞 ⟶ Set" "X ∈ Obj 𝒞"
  shows "setmap (component η X)"
using assms Nat.component_mapping unfolding Set_def by fastforce

definition yoneda where
  "yoneda 𝒞 ≡ ⦇
    domCat = 𝒞,
    codCat = PSh(𝒞),
    fobj = contraHom 𝒞,
    fmap = contraHomNat 𝒞
  ⦈"

lemma yoneda_functor:
  assumes "Category 𝒞"
  shows "Functor' (yoneda 𝒞) : 𝒞 ⟶ PSh(𝒞)"
unfolding Functor_def apply auto
unfolding yoneda_def Presheaf_def
apply (auto simp add: assms FunCat_category opposite_category Set_category)
apply (auto simp add: assms FunCat_def contraHom_functor contraHomNat_nat)
apply (auto simp add: assms Category.dom_obj Category.cod_obj FunCat_def contraHom_functor)
proof-
  fix X
  assume "X ∈ Obj 𝒞" thus "HomNat{𝒞}[-,id⇘𝒞⇙ X] = idNat Hom{𝒞}[-,X]"
    apply (rule_tac nat_eq)
    apply (auto simp add: assms Category.id_exist Nat.dom_functor contraHomNat_nat)
    apply (auto simp add: assms contraHom_functor idNat_nat)
    proof -
      fix Xa
      assume "X ∈ Obj 𝒞" "Xa ∈ Obj (𝒞 {^op})"
      thus "component HomNat{𝒞}[-,id⇘𝒞⇙ X] Xa = component (idNat Hom{𝒞}[-,X]) Xa"
        unfolding contraHomNat_def apply auto
        unfolding idNat_def apply auto
        unfolding contraHom_def apply auto
        apply (auto simp add: assms Category.id_exist)
        apply (rule setmap_eq)
        by (auto simp add: setmap_def Set_def assms Category.left_id Category.right_id)
    qed
next
  fix f g
  assume fg: "f ∈ Arr 𝒞" "g ∈ Arr 𝒞" "cod⇘𝒞⇙ f = dom⇘𝒞⇙ g"
  hence gf:"(g ∘[𝒞] f) ∈ Arr 𝒞" by (auto simp add: assms Category.comp_exist)
  let ?Cop = "𝒞 {^op}"
  show "HomNat{𝒞}[-,g ∘[𝒞] f] = Nat[HomNat{𝒞}[-,g] ∘ HomNat{𝒞}[-,f]]" (is "?L = ?R")
    apply (rule_tac nat_eq [of _ ?Cop Set _ ?L ?R] , auto)
    apply (auto simp add: contraHomNat_nat fg assms Category.comp_exist)
    apply (auto simp add: contraHom_functor Category.dom_obj Category.cod_obj fg assms)
    apply (auto simp add: compNat_nat contraHomNat_nat fg assms)
    proof -
      fix X
      assume X_in: "X ∈ Obj (𝒞 {^op})"
      show "component HomNat{𝒞}[-,g ∘[𝒞] f] X = component Nat[HomNat{𝒞}[-,g] ∘ HomNat{𝒞}[-,f]] X" (is "?L = ?R")
        proof -
          have "setmap ?L"
            using setmap_nat_component [OF _ _ X_in] contraHom_functor [OF assms] contraHomNat_nat [OF assms gf]
            using Category.cod_obj [OF assms gf] Nat.dom_functor Nat.same_cod Nat.same_dom by metis
          moreover have "setmap ?R"
            using setmap_nat_component [OF _ _ X_in] contraHom_functor [OF assms] contraHomNat_nat [OF assms] fg
            using Category.dom_obj [OF assms fg(1)] compNat_nat by metis
          moreover have "setdom ?L = setdom ?R"
            proof-
              have 0: "setdom ?L = X -[𝒞]→ (dom⇘𝒞⇙ (g ∘[𝒞] f))"
                unfolding contraHomNat_def by auto
              have "setdom ?R = setdom (component HomNat{𝒞}[-,g] X ∘[codCat (domFunctor HomNat{𝒞}[-,g])] component HomNat{𝒞}[-,f] X)"
                unfolding compNat_def by auto
              also have "… = setdom (component HomNat{𝒞}[-,g] X ∘[Set] component HomNat{𝒞}[-,f] X)"
                unfolding contraHomNat_def contraHom_functor fg X_in by (simp add: contraHom_def)
              also have "… = setdom (component HomNat{𝒞}[-,f] X)"
                unfolding Set_def by auto
              also have "… = X -[𝒞]→ (dom⇘𝒞⇙ f)"
                unfolding contraHomNat_def by auto
              finally
                show ?thesis using 0 assms Category.comp_exist fg by fastforce
            qed
          moreover have "setcod ?L = setcod ?R"
            proof-
              have 0: "setcod ?L = X -[𝒞]→ (cod⇘𝒞⇙ (g ∘[𝒞] f))"
                unfolding contraHomNat_def by auto
              have "setcod ?R = setcod (component HomNat{𝒞}[-,g] X ∘[codCat (domFunctor HomNat{𝒞}[-,g])] component HomNat{𝒞}[-,f] X)"
                unfolding compNat_def by auto
              also have "… = setcod (component HomNat{𝒞}[-,g] X ∘[Set] component HomNat{𝒞}[-,f] X)"
                unfolding contraHomNat_def contraHom_functor fg X_in by (simp add: contraHom_def)
              also have "… = setcod (component HomNat{𝒞}[-,g] X)"
                unfolding Set_def by auto
              also have "… = X -[𝒞]→ (cod⇘𝒞⇙ g)"
                unfolding contraHomNat_def by auto
              finally
                show ?thesis using 0 assms Category.comp_exist fg by fastforce
            qed
          moreover have "∀f∈setdom ?L. setfunction ?L f = setfunction ?R f"
            proof
              fix fa
              assume "fa ∈ setdom (component HomNat{𝒞}[-,g ∘[𝒞] f] X)"
              hence "fa : X -[𝒞]→ (Dom 𝒞 f)"
                unfolding contraHomNat_def by (auto simp add: assms fg Category.comp_exist)
              thus "setfunction (component HomNat{𝒞}[-,g ∘[𝒞] f] X) fa = setfunction (component Nat[HomNat{𝒞}[-,g] ∘ HomNat{𝒞}[-,f]] X) fa"
                unfolding compNat_def contraHomNat_def contraHom_def Set_def
                by (auto simp add: assms Category.assoc fg)
            qed
          ultimately
            show ?thesis using setmap_eq [of ?L ?R] by auto
        qed
    qed
qed

abbreviation arrow (infixr "→" 80) where
  "A → B ≡ {f. ∀x∈A. f x ∈ B}"

definition Bijective ("_ ≅ _") where
  "A ≅ B ≡ ∃f ∈ A → B. ∃g ∈ B → A. (∀x ∈ A. g (f x) = x) & (∀y ∈ B. f (g y) = y)"

definition nat_to_obj where
  "nat_to_obj 𝒞 F r ≡ λα. setfunction (component α r) (Id 𝒞 r)"

lemma nat_to_obj_arrow:
  assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "r ∈ Obj 𝒞"
  shows "nat_to_obj 𝒞 F r : Category.Hom (PSh(𝒞)) (fobj (yoneda 𝒞) r) F → fobj F r"
proof
  show "∀α∈(fobj (yoneda 𝒞) r -[PSh(𝒞)]→ F). nat_to_obj 𝒞 F r α ∈ fobj F r"
    proof
      fix α
      assume "α ∈ fobj (yoneda 𝒞) r -[PSh(𝒞)]→ F"
      hence "Nat' α : fobj (yoneda 𝒞) r ⟶ F"
        unfolding Presheaf_def FunCat_def by auto
      hence "component α r : Category.Hom 𝒞 r r -[Set]→ fobj F r"
        proof -
          have r_in: "r ∈ Obj (𝒞 {^op})"
            unfolding opposite_def by (auto simp add: assms(3))
          assume α_nat: "Nat' α : fobj (yoneda 𝒞) r ⟶ F"
          hence "Functor' (domFunctor α) : 𝒞 {^op} ⟶ Set"
            unfolding yoneda_def
            using contraHom_functor [of 𝒞 r] assms by auto
          hence "component α r : fobj (domFunctor α) r -[Set]→ fobj (codFunctor α) r"
            using Nat.component_mapping [of α r] α_nat r_in by auto
          thus ?thesis
            using α_nat yoneda_def [of 𝒞] contraHom_def [of 𝒞 r] by auto
        qed
      thus "nat_to_obj 𝒞 F r α ∈ fobj F r"
        unfolding nat_to_obj_def Set_def setmap_def
        using assms(1) assms (3) Category.id_exist [of 𝒞 r]
        by auto
    qed
qed

definition obj_to_nat where
  "obj_to_nat 𝒞 F r ≡ λx. ⦇
    domFunctor = (fobj (yoneda 𝒞) r),
    codFunctor = F,
    component = λd. ⦇ setdom = fobj (fobj (yoneda 𝒞) r) d, setcod = fobj F d
                    , setfunction = λu. setfunction (fmap F u) x ⦈
  ⦈"

lemma obj_to_nat_arrow:
  assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "r ∈ Obj 𝒞"
  shows "obj_to_nat 𝒞 F r : fobj F r → Category.Hom (PSh(𝒞)) (fobj (yoneda 𝒞) r) F"
proof auto
  fix x
  assume x_in: "x ∈ fobj F r"
  have nat: "Nat' (obj_to_nat 𝒞 F r x) : (fobj (yoneda 𝒞) r) ⟶ F"
    proof
      show "Category.Nat (obj_to_nat 𝒞 F r x)" (is "Category.Nat ?f")
        proof
          have 1: "Functor' (fobj (yoneda 𝒞) r) : 𝒞 {^op} ⟶ Set"
            unfolding yoneda_def using contraHom_functor [of 𝒞 r] assms by auto
          have 2: "Functor' F : 𝒞 {^op} ⟶ Set" using assms(2) unfolding Presheaf_def FunCat_def by auto
          thus "Functor' (domFunctor ?f) : domCat (domFunctor ?f) ⟶ codCat (domFunctor ?f)"
            unfolding obj_to_nat_def apply auto
            using assms(2) unfolding Presheaf_def FunCat_def yoneda_def
            using contraHom_functor [of 𝒞 r] assms by auto
          show "Functor' (codFunctor ?f) : domCat (codFunctor ?f) ⟶ codCat (codFunctor ?f)"
            unfolding obj_to_nat_def using assms(2) unfolding Presheaf_def FunCat_def by auto
          show "domCat (domFunctor ?f) = domCat (codFunctor ?f)"
            unfolding obj_to_nat_def using 1 2 by auto
          show "codCat (domFunctor ?f) = codCat (codFunctor ?f)"
            unfolding obj_to_nat_def using 1 2 by auto

          fix xa
          assume xa_in: "xa ∈ Obj (domCat (domFunctor ?f))"
          show "component ?f xa ∈ fobj (domFunctor ?f) xa -[codCat (domFunctor ?f)]→ fobj (codFunctor ?f) xa"
            apply (auto simp add: obj_to_nat_def 1)
            unfolding Set_def apply auto
            unfolding yoneda_def apply auto
            unfolding contraHom_def apply auto
            proof (unfold setmap_def , auto)
              fix xb
              assume xb_assm: "xb ∈ Arr 𝒞" "xa = dom⇘𝒞⇙ xb" "r = cod⇘𝒞⇙ xb"
              hence "xb : r -[𝒞 {^op}]→ xa"
                unfolding opposite_def by auto
              hence Fxb_type: "fmap F xb : fobj F r -[Set]→ fobj F xa"
                using Functor.fmap_mapping [of F xb] 2 by auto
              hence "setmap (fmap F xb)"
                unfolding Set_def by auto
              thus "setfunction (fmap F xb) x ∈ fobj F (dom⇘𝒞⇙ xb)"
                unfolding setmap_def using x_in xb_assm Fxb_type
                unfolding Set_def by auto
            qed
        next
          have 1: "Functor' (fobj (yoneda 𝒞) r) : 𝒞 {^op} ⟶ Set"
            unfolding yoneda_def using contraHom_functor [of 𝒞 r] assms by auto
          have 2: "Functor' F : 𝒞 {^op} ⟶ Set" using assms(2) unfolding Presheaf_def FunCat_def by auto
          fix f
          assume "f ∈ Arr (domCat (domFunctor ?f))"
          hence f_in: "f : (cod⇘𝒞⇙ f) -[𝒞 {^op}]→ (dom⇘𝒞⇙ f)"
            using contraHom_functor [of 𝒞 r] assms
            unfolding opposite_def obj_to_nat_def yoneda_def
            by auto
          show "(component ?f (cod⇘domCat (domFunctor ?f)⇙ f) ∘[codCat (domFunctor ?f)] fmap (domFunctor ?f) f) =
                (fmap (codFunctor ?f) f ∘[codCat (domFunctor ?f)] component ?f (dom⇘domCat (domFunctor ?f)⇙ f))"
            apply (auto simp add: obj_to_nat_def 1 opposite_def)
            unfolding yoneda_def apply auto
            unfolding contraHom_def apply auto
            proof (rule setmap_eq , auto simp add: Set_def)
              show "setmap ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = fobj F (dom⇘𝒞⇙ f),
                            setfunction = λxa. setfunction (fmap F (xa ∘[𝒞] f)) x⦈"
                unfolding setmap_def
                proof auto
                  fix xa
                  assume "xa ∈ Arr 𝒞" "dom⇘𝒞⇙ xa = cod⇘𝒞⇙ f" "r = cod⇘𝒞⇙ xa"
                  hence "(f ∘[𝒞 {^op}] xa) : r -[𝒞 {^op}]→ (dom⇘𝒞⇙ f)"
                    using f_in unfolding opposite_def by (auto simp add: Category.comp_exist assms(1))
                  hence "fmap F (f ∘[𝒞 {^op}] xa) : fobj F r -[Set]→ fobj F (dom⇘𝒞⇙ f)"
                    using Functor.fmap_mapping 2 by fastforce
                  thus "setfunction (fmap F (xa ∘[𝒞] f)) x ∈ fobj F (dom⇘𝒞⇙ f)"
                    unfolding opposite_def Set_def setmap_def using x_in by auto
                qed
              show "setmap ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = setcod (fmap F f),
                            setfunction = λxa. setfunction (fmap F f) (setfunction (fmap F xa) x)⦈"
                unfolding setmap_def
                proof auto
                  fix xa
                  assume xa_assms: "xa ∈ Arr 𝒞" "dom⇘𝒞⇙ xa = cod⇘𝒞⇙ f" "r = cod⇘𝒞⇙ xa"
                  hence "fmap F f : fobj F (cod⇘𝒞⇙ f) -[Set]→ fobj F (dom⇘𝒞⇙ f)" "fmap F xa : fobj F r -[Set]→ fobj F (dom⇘𝒞⇙ xa)"
                    using Functor.fmap_mapping 2 f_in apply fastforce
                    using Functor.fmap_mapping [of F xa] 2 xa_assms unfolding opposite_def by auto
                  thus "setfunction (fmap F f) (setfunction (fmap F xa) x) ∈ setcod (fmap F f)"
                    unfolding Set_def setmap_def using x_in xa_assms by auto
                qed
            next
              have Ff_type: "fmap F f : fobj F (cod⇘𝒞⇙ f) -[Set]→ fobj F (dom⇘𝒞⇙ f)"
                using f_in Functor.fmap_type 2 unfolding opposite_def by fastforce
              fix x
              assume "x ∈ fobj F (dom⇘𝒞⇙ f)" thus "x ∈ setcod (fmap F f)"
                using Ff_type unfolding Set_def by auto
            next
              have Ff_type: "fmap F f : fobj F (cod⇘𝒞⇙ f) -[Set]→ fobj F (dom⇘𝒞⇙ f)"
                using f_in Functor.fmap_type 2 unfolding opposite_def by fastforce
              fix x
              assume "x ∈ setcod (fmap F f)" thus "x ∈ fobj F (dom⇘𝒞⇙ f)"
                using Ff_type unfolding Set_def by auto
            next
              fix xa
              assume xa_assms: "xa ∈ Arr 𝒞" "dom⇘𝒞⇙ xa = cod⇘𝒞⇙ f" "r = cod⇘𝒞⇙ xa"
              have "setfunction (fmap F (f ∘[𝒞 {^op}] xa)) x = setfunction (fmap F f) (setfunction (fmap F xa) x)" (is "?L = ?R")
                proof-
                  have "?L = setfunction (fmap F f ∘[Set] fmap F xa) x"
                    using Functor.covariant [of F xa f] 2 f_in xa_assms
                    by (metis (no_types, lifting) Category.Category.select_convs(2) Category.Category.select_convs(3) Category.Category.select_convs(4) mem_Collect_eq opposite_def)
                  also have "… = ?R"
                    unfolding Set_def by auto
                  finally show ?thesis by simp
                qed
              thus "setfunction (fmap F (xa ∘[𝒞] f)) x = setfunction (fmap F f) (setfunction (fmap F xa) x)"
                unfolding opposite_def by auto
            qed
        qed
      show "domFunctor (obj_to_nat 𝒞 F r x) = fobj (yoneda 𝒞) r ∧ codFunctor (obj_to_nat 𝒞 F r x) = F"
        unfolding obj_to_nat_def by auto
    qed
    show "obj_to_nat 𝒞 F r x ∈ Arr PSh(𝒞)"
      unfolding Presheaf_def FunCat_def apply auto
      using nat apply auto
      unfolding yoneda_def apply auto
      using contraHom_functor [OF assms(1) assms(3)] apply auto
      using assms(2) unfolding Presheaf_def FunCat_def apply auto
      done
    show "dom⇘PSh 𝒞⇙ obj_to_nat 𝒞 F r x = fobj (yoneda 𝒞) r"
      unfolding obj_to_nat_def Presheaf_def FunCat_def by auto
    show "cod⇘PSh 𝒞⇙ obj_to_nat 𝒞 F r x = F"
      unfolding obj_to_nat_def Presheaf_def FunCat_def by auto
qed

lemma YonedaLemma:
  assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "r ∈ Obj 𝒞"
  shows "(Category.Hom (PSh(𝒞)) (fobj (yoneda 𝒞) r) F) ≅ (fobj F r)"
unfolding Bijective_def
proof -
  let ?f = "nat_to_obj 𝒞 F r"
  let ?g = "obj_to_nat 𝒞 F r"
  let ?Cop = "𝒞 {^op}"
  have "?f ∈ (fobj (yoneda 𝒞) r -[PSh 𝒞]→ F) → fobj F r"
    using nat_to_obj_arrow assms by fastforce
  moreover have "?g ∈ fobj F r → (fobj (yoneda 𝒞) r -[PSh 𝒞]→ F)"
    using obj_to_nat_arrow assms by fastforce
  moreover have "∀x∈fobj (yoneda 𝒞) r -[PSh 𝒞]→ F. ?g (?f x) = x" (is "∀x∈?yoneda -[_]→ _. _")
    apply auto
    proof (rule nat_eq [of ?yoneda ?Cop Set F])
      fix x
      assume 1: "x ∈ Arr PSh 𝒞" "dom⇘PSh 𝒞⇙ x = fobj (yoneda 𝒞) r" "F = cod⇘PSh 𝒞⇙ x"
      hence x_arrow: "x : fobj (yoneda 𝒞) r -[PSh 𝒞]→ F" by auto
      hence x_nat: "Nat' x : fobj (yoneda 𝒞) r ⟶ F"
        unfolding Presheaf_def FunCat_def by auto
      show "Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set"
        unfolding yoneda_def by (auto simp add: contraHom_functor assms)
      show "Functor' F : 𝒞 {^op} ⟶ Set"
        using assms(2) unfolding Presheaf_def FunCat_def by auto
      show "Nat' obj_to_nat 𝒞 (cod⇘PSh 𝒞⇙ x) r (nat_to_obj 𝒞 (cod⇘PSh 𝒞⇙ x) r x) : fobj (yoneda 𝒞) r ⟶ F"
        using nat_to_obj_arrow [OF assms] obj_to_nat_arrow [OF assms] x_arrow
        unfolding Presheaf_def FunCat_def by auto
      show "Nat' x : fobj (yoneda 𝒞) r ⟶ F" by fact
      show "∀X∈Obj (𝒞 {^op}). component (obj_to_nat 𝒞 (cod⇘PSh 𝒞⇙ x) r (nat_to_obj 𝒞 (cod⇘PSh 𝒞⇙ x) r x)) X = component x X"
        apply (auto simp add: `F = cod⇘PSh 𝒞⇙ x` [symmetric])
        proof (rule_tac setmap_eq)
          fix X assume X_in: "X ∈ Obj (𝒞 {^op})"
          have 2: "nat_to_obj 𝒞 F r x ∈ fobj F r"
            using nat_to_obj_arrow [OF assms]
            using x_arrow by auto
          have "Nat (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x))"
            using obj_to_nat_arrow [OF assms] 2 unfolding Presheaf_def FunCat_def by auto
          moreover have "Functor' (domFunctor (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x))) : 𝒞 {^op} ⟶ Set"
            unfolding obj_to_nat_def yoneda_def using contraHom_functor [OF assms(1) assms(3)] by auto
          ultimately
            show "setmap (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X)"
              using setmap_nat_component [OF _ _ X_in] by auto
          show "setmap (component x X)"
            using setmap_nat_component [OF _ _ X_in] x_nat unfolding yoneda_def
            by (metis `Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set` yoneda_def)
          show "setdom (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X) = setdom (component x X)"
            unfolding obj_to_nat_def nat_to_obj_def apply simp
            using Nat.component_mapping [of x X] apply (simp add: x_nat)
            by (simp add: `Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set` Set_def X_in)
          show "setcod (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X) = setcod (component x X)"
            unfolding obj_to_nat_def nat_to_obj_def apply simp
            using Nat.component_mapping [of x X] apply (simp add: x_nat)
            by (simp add: `Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set` Set_def X_in)
          show "∀xa∈setdom (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X).
            setfunction (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X) xa =
            setfunction (component x X) xa"
            unfolding obj_to_nat_def nat_to_obj_def yoneda_def apply simp
            unfolding contraHom_def
            proof auto
              fix xa assume xa_assms: "xa ∈ Arr 𝒞" "X = dom⇘𝒞⇙ xa" "r = cod⇘𝒞⇙ xa"
              have "(fmap F xa ∘[Set] component x r) = component x X ∘[Set] fmap (fobj (yoneda 𝒞) r) xa"
                using Nat.naturality [of x xa] x_nat apply auto
                unfolding yoneda_def apply simp unfolding contraHom_def apply simp
                unfolding opposite_def by (auto simp add: xa_assms)
              hence 2: "setfunction (fmap F xa) (setfunction (component x r) (id⇘𝒞⇙ r))
                      = setfunction (component x X) (setfunction (fmap (fobj (yoneda 𝒞) r) xa) (id⇘𝒞⇙ r))"
                unfolding Set_def apply auto by metis
              show "setfunction (fmap F xa) (setfunction (component x (cod⇘𝒞⇙ xa)) (id⇘𝒞⇙ cod⇘𝒞⇙ xa)) =
                    setfunction (component x (dom⇘𝒞⇙ xa)) xa"
                apply (auto simp add: xa_assms(2) [symmetric] xa_assms(3) [symmetric])
                apply (auto simp add: 2)
                unfolding yoneda_def apply simp
                unfolding contraHom_def apply simp
                using Category.left_id [OF assms(1) xa_assms(1)] xa_assms(3) by auto
            qed
        qed
    qed
  moreover have "∀y∈fobj F r. ?f (?g y) = y"
    apply auto
    unfolding nat_to_obj_def obj_to_nat_def apply simp
    using Functor.preserve_id [of F r] assms
    unfolding Presheaf_def FunCat_def opposite_def apply auto
    unfolding Set_def by simp
  ultimately
    show "∃f∈(fobj (yoneda 𝒞) r -[PSh 𝒞]→ F) → fobj F r. ∃g∈fobj F r → (fobj (yoneda 𝒞) r -[PSh 𝒞]→ F).
         (∀x∈fobj (yoneda 𝒞) r -[PSh 𝒞]→ F. g (f x) = x) ∧ (∀y∈fobj F r. f (g y) = y)"
      by auto
qed

end