setoid construction

Category.thy

theory Category
imports Main
begin

no_notation Fun.comp (infixl "∘" 55)

lemma equiv_refl: "equiv A R ⟹ x ∈ A ⟹ (x,x) ∈ R"
by (rule equivE, simp, rule refl_onD, simp)

lemma equiv_sym: "equiv A R ⟹ (x,y) ∈ R ⟹ (y,x) ∈ R"
by (rule equivE, simp, rule symD, simp)

lemma equiv_trans: "equiv A R ⟹ (x,y) ∈ R ⟹ (y,z) ∈ R ⟹ (x,z) ∈ R"
by (rule equivE, simp, rule transD, simp)

lemma equiv_reflp: "equiv A {(x,y). eq x y} ⟹ x ∈ A ⟹ eq x x"
using equiv_refl by fastforce

lemma equiv_symp: "equiv A {(x,y). eq x y} ⟹ eq x y ⟹ eq y x"
using equiv_sym by fastforce

lemma equiv_transp: "equiv A {(x,y). eq x y} ⟹ eq x y ⟹ eq y z ⟹ eq x z"
by (meson equivE transpE transp_trans)

record 'a setoid =
  carrier :: "'a set"
  equal :: "'a ⇒ 'a ⇒ bool"

locale setoid =
  fixes A :: "('a,'b) setoid_scheme"
  assumes equal_equiv: "equiv (carrier A) {(x,y). equal A x y}"

declare [[coercion_enabled]]
declare [[coercion carrier]]

definition setoid_set where
  "setoid_set A = ⦇ carrier = A, equal = λx y. x = y ∧ x ∈ A ∧ y ∈ A ⦈"

lemma setoid_set_setoid: "setoid (setoid_set A)"
apply (unfold setoid_def setoid_set_def, auto, rule equivI)
apply (rule refl_onI, auto, rule symI, auto, rule transI, auto)
done

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

locale Category =
  fixes 𝒞 :: "('o,'a,'c) Category_scheme" (structure)

  assumes arr_setoid: "setoid (Arr 𝒞)"
  and dom_obj: "f ∈ Arr 𝒞 ⟹ Dom 𝒞 f ∈ Obj 𝒞"
  and cod_obj: "f ∈ Arr 𝒞 ⟹ Cod 𝒞 f ∈ Obj 𝒞"
  and id_exist: "A ∈ Obj 𝒞 ⟹ id A ∈ Arr 𝒞 ∧ Dom 𝒞 (id A) = A ∧ Cod 𝒞 (id A) = A"
  and comp_exist: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; Cod 𝒞 f = Dom 𝒞 g ⟧
    ⟹ g ∘ f ∈ Arr 𝒞 ∧ Dom 𝒞 (g ∘ f) = Dom 𝒞 f ∧ Cod 𝒞 (g ∘ f) = Cod 𝒞 g"
  and comp_equal: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; h ∈ Arr 𝒞; i ∈ Arr 𝒞; equal (Arr 𝒞) f g; equal (Arr 𝒞) h i;
    Dom 𝒞 f = Dom 𝒞 g; Cod 𝒞 f = Cod 𝒞 g; Dom 𝒞 h = Dom 𝒞 i; Cod 𝒞 h = Cod 𝒞 i; Cod 𝒞 h = Dom 𝒞 f ⟧
    ⟹ equal (Arr 𝒞) (f ∘ h) (g ∘ i)"

  and left_id: "f ∈ Arr 𝒞 ⟹ equal (Arr 𝒞) (id (Cod 𝒞 f) ∘ f) f"
  and right_id: "f ∈ Arr 𝒞 ⟹ equal (Arr 𝒞) f (f ∘ id (Dom 𝒞 f))"
  and assoc: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; h ∈ Arr 𝒞; Cod 𝒞 f = Dom 𝒞 g; Cod 𝒞 g = Dom 𝒞 h ⟧ ⟹ equal (Arr 𝒞) ((h ∘ g) ∘ f) (h ∘ (g ∘ f))"

abbreviation arr_equal (infixl "≈ı" 40) where
  "arr_equal 𝒞 f g ≡ (equal (Arr 𝒞) f g)"

lemma (in Category) arr_equiv: "equiv (Arr 𝒞) {(f,g). f ≈ g}"
using arr_setoid by (simp add: setoid_def)

lemma (in Category) arr_refl: "f ∈ Arr 𝒞 ⟹ f ≈ f"
by (rule equiv_reflp, rule arr_equiv, simp)

lemma (in Category) arr_sym: "f ≈ g ⟹ g ≈ f"
by (rule equiv_symp, rule arr_equiv, simp)

lemma (in Category) arr_trans: "⟦ f ≈ g; g ≈ h ⟧ ⟹ f ≈ h"
by (rule equiv_transp, rule arr_equiv, simp)

definition hom ("Hom[_][_,_]" 80) where
  "Hom[𝒞][A,B] ≡ ⦇ carrier = {f ∈ Arr 𝒞. Dom 𝒞 f = A ∧ Cod 𝒞 f = B}
    , equal = λf g. equal (Arr 𝒞) f g ∧ f ∈ Arr 𝒞 ∧ g ∈ Arr 𝒞 ∧ Dom 𝒞 f = A ∧ Cod 𝒞 f = B ∧ Dom 𝒞 g = A ∧ Cod 𝒞 g = B ⦈"

lemma hom_setoid: "Category 𝒞 ⟹ A ∈ Obj 𝒞 ⟹ B ∈ Obj 𝒞 ⟹ setoid (Hom[𝒞][A,B])"
apply (unfold setoid_def hom_def, simp, rule equivI)
apply (rule refl_onI, auto simp add: Category.arr_refl)
apply (rule symI, auto simp add: Category.arr_sym)
apply (rule transI, simp, rule Category.arr_trans, auto)
done

lemma CategoryI:
  fixes 𝒞 :: "('o,'a,'c) Category_scheme"
  assumes "setoid (Arr 𝒞)"
  and "⋀f. f ∈ Arr 𝒞 ⟹ Dom 𝒞 f ∈ Obj 𝒞" "⋀f. f ∈ Arr 𝒞 ⟹ Cod 𝒞 f ∈ Obj 𝒞"
  and "⋀A. A ∈ Obj 𝒞 ⟹ Id 𝒞 A ∈ Hom[𝒞][A,A]"
  and "⋀A B C f g. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B]; g ∈ Hom[𝒞][B,C] ⟧ ⟹ g ∘⇘𝒞⇙ f ∈ Hom[𝒞][A,C]"
  and "⋀A B C f g h i. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; f ∈ Hom[𝒞][B,C]; g ∈ Hom[𝒞][B,C]; h ∈ Hom[𝒞][A,B]; i ∈ Hom[𝒞][A,B]; f ≈⇘𝒞⇙ g; h ≈⇘𝒞⇙ i ⟧ ⟹ f ∘⇘𝒞⇙ h ≈⇘𝒞⇙ g ∘⇘𝒞⇙ i"
  and "⋀A B f. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B] ⟧ ⟹ Id 𝒞 B ∘⇘𝒞⇙ f ≈⇘𝒞⇙ f"
  and "⋀A B f. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B] ⟧ ⟹ f ≈⇘𝒞⇙ f ∘⇘𝒞⇙ Id 𝒞 A"
  and "⋀A B C D f g h. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; D ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B]; g ∈ Hom[𝒞][B,C]; h ∈ Hom[𝒞][C,D] ⟧ ⟹ ((h ∘⇘𝒞⇙ g) ∘⇘𝒞⇙ f) ≈⇘𝒞⇙ (h ∘⇘𝒞⇙ (g ∘⇘𝒞⇙ f))"
  shows "Category 𝒞"
proof (unfold Category_def, auto simp add: assms)
  { fix A assume "A ∈ Obj 𝒞" thus "id⇘𝒞⇙ A ∈ carrier (Arr 𝒞)" using assms(4) by (simp add: hom_def) }
  { fix A assume "A ∈ Obj 𝒞" thus "Dom 𝒞 (id⇘𝒞⇙ A) = A" using assms(4) by (simp add: hom_def) }
  { fix A assume "A ∈ Obj 𝒞" thus "Cod 𝒞 (id⇘𝒞⇙ A) = A" using assms(4) by (simp add: hom_def) }
next
  fix f g
  {
    assume 1: "f ∈ carrier (Arr 𝒞)" "g ∈ carrier (Arr 𝒞)" "Cod 𝒞 f = Dom 𝒞 g"
    have 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" "Dom 𝒞 g ∈ Obj 𝒞" "Cod 𝒞 g ∈ Obj 𝒞"
      using 1 assms(2) assms(3) by auto
    show "g ∘⇘𝒞⇙ f ∈ carrier (Arr 𝒞)"
      using assms(5) [of "Dom 𝒞 f" "Cod 𝒞 f" "Cod 𝒞 g" f g] by (simp add: hom_def 2 1)
  }
  {
    assume 1: "f ∈ carrier (Arr 𝒞)" "g ∈ carrier (Arr 𝒞)" "Cod 𝒞 f = Dom 𝒞 g"
    have 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" "Dom 𝒞 g ∈ Obj 𝒞" "Cod 𝒞 g ∈ Obj 𝒞"
      using 1 assms(2) assms(3) by auto
    show "Dom 𝒞 (g ∘⇘𝒞⇙ f) = Dom 𝒞 f"
      using assms(5) [of "Dom 𝒞 f" "Cod 𝒞 f" "Cod 𝒞 g" f g] by (simp add: hom_def 2 1)
  }
  {
    assume 1: "f ∈ carrier (Arr 𝒞)" "g ∈ carrier (Arr 𝒞)" "Cod 𝒞 f = Dom 𝒞 g"
    have 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" "Dom 𝒞 g ∈ Obj 𝒞" "Cod 𝒞 g ∈ Obj 𝒞"
      using 1 assms(2) assms(3) by auto
    show "Cod 𝒞 (g ∘⇘𝒞⇙ f) = Cod 𝒞 g"
      using assms(5) [of "Dom 𝒞 f" "Cod 𝒞 f" "Cod 𝒞 g" f g] by (simp add: hom_def 2 1)
  }
next
  fix f g h i
  assume 1: "f ∈ carrier (Arr 𝒞)" "g ∈ carrier (Arr 𝒞)" "h ∈ carrier (Arr 𝒞)" "i ∈ carrier (Arr 𝒞)" "f ≈⇘𝒞⇙ g" "h ≈⇘𝒞⇙ i"
            "Dom 𝒞 f = Dom 𝒞 g" "Cod 𝒞 f = Cod 𝒞 g" "Dom 𝒞 h = Dom 𝒞 i" "Cod 𝒞 h = Dom 𝒞 g" "Cod 𝒞 i = Dom 𝒞 g"
  have 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" "Dom 𝒞 g ∈ Obj 𝒞" "Cod 𝒞 g ∈ Obj 𝒞" "Dom 𝒞 h ∈ Obj 𝒞" "Cod 𝒞 h ∈ Obj 𝒞" "Dom 𝒞 i ∈ Obj 𝒞" "Cod 𝒞 i ∈ Obj 𝒞"
    using 1 assms(2) assms(3) by auto
  show "f ∘⇘𝒞⇙ h ≈⇘𝒞⇙ g ∘⇘𝒞⇙ i"
    by (rule assms(6) [of "Dom 𝒞 h" "Dom 𝒞 f" "Cod 𝒞 f" f g h i], auto simp add: 2 hom_def 1)
next
  fix f
  {
    assume 1: "f ∈ carrier (Arr 𝒞)"
    hence 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" using assms(2) assms(3) by auto
    show "id⇘𝒞⇙ Cod 𝒞 f ∘⇘𝒞⇙ f ≈⇘𝒞⇙ f" by (rule assms(7), auto simp add: hom_def 2 1)
  }
  {
    assume 1: "f ∈ carrier (Arr 𝒞)"
    hence 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" using assms(2) assms(3) by auto
    show "f ≈⇘𝒞⇙ f ∘⇘𝒞⇙ id⇘𝒞⇙ Dom 𝒞 f" by (rule assms(8), auto simp add: hom_def 2 1)
  }
next
  fix f g h
  assume 1: "f ∈ carrier (Arr 𝒞)" "g ∈ carrier (Arr 𝒞)" "h ∈ carrier (Arr 𝒞)" "Cod 𝒞 f = Dom 𝒞 g" "Cod 𝒞 g = Dom 𝒞 h"
  hence 2: "Dom 𝒞 f ∈ Obj 𝒞" "Cod 𝒞 f ∈ Obj 𝒞" "Dom 𝒞 g ∈ Obj 𝒞" "Cod 𝒞 g ∈ Obj 𝒞" "Dom 𝒞 h ∈ Obj 𝒞" "Cod 𝒞 h ∈ Obj 𝒞"
    using assms(2) assms(3) by auto
  show "h ∘⇘𝒞⇙ g ∘⇘𝒞⇙ f ≈⇘𝒞⇙ h ∘⇘𝒞⇙ (g ∘⇘𝒞⇙ f)"
    by (rule assms(9), auto simp add: hom_def 2 1)
qed

lemma CategoryE:
  "Category 𝒞 ⟹
    (setoid (Arr 𝒞) ⟹
     (⋀f. f ∈ Arr 𝒞 ⟹ Dom 𝒞 f ∈ Obj 𝒞) ⟹ (⋀f. f ∈ Arr 𝒞 ⟹ Cod 𝒞 f ∈ Obj 𝒞) ⟹
     (⋀A. A ∈ Obj 𝒞 ⟹ Id 𝒞 A ∈ Hom[𝒞][A,A]) ⟹
     (⋀A B C f g. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B]; g ∈ Hom[𝒞][B,C] ⟧ ⟹ g ∘⇘𝒞⇙ f ∈ Hom[𝒞][A,C]) ⟹
     (⋀A B C f g h i. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; f ∈ Hom[𝒞][B,C]; g ∈ Hom[𝒞][B,C]; h ∈ Hom[𝒞][A,B]; i ∈ Hom[𝒞][A,B]; f ≈⇘𝒞⇙ g; h ≈⇘𝒞⇙ i ⟧ ⟹ f ∘⇘𝒞⇙ h ≈⇘𝒞⇙ g ∘⇘𝒞⇙ i) ⟹
     thesis)
   ⟹ thesis"
by (unfold Category_def hom_def, auto)

lemma CategoryE_hom_refl: "⟦ Category 𝒞; f ∈ Hom[𝒞][A,B] ⟧ ⟹ f ≈⇘𝒞⇙ f"
by (simp add: hom_def Category.arr_refl)

lemma CategoryE_hom_sym: "⟦ Category 𝒞; f ≈⇘𝒞⇙ g ⟧ ⟹ g ≈⇘𝒞⇙ f"
by (simp add: hom_def Category.arr_sym)

lemma CategoryE_hom_trans: "⟦ Category 𝒞; f ≈⇘𝒞⇙ g; g ≈⇘𝒞⇙ h ⟧ ⟹ f ≈⇘𝒞⇙ h"
by (rule Category.arr_trans, auto simp add: hom_def)

lemma CategoryE_id_exist:
  assumes "Category 𝒞"
  shows "A ∈ Obj 𝒞 ⟹ Id 𝒞 A ∈ Hom[𝒞][A,A]"
by (metis CategoryE [OF assms])

lemma CategoryE_comp_exist:
  assumes "Category 𝒞"
  shows "⋀A B C f g. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B]; g ∈ Hom[𝒞][B,C] ⟧ ⟹ g ∘⇘𝒞⇙ f ∈ Hom[𝒞][A,C]"
by (metis CategoryE [OF assms])

lemma CategoryE_comp_equal:
  assumes "Category 𝒞"
  shows "⋀A B C f g h i. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; f ∈ Hom[𝒞][B,C]; g ∈ Hom[𝒞][B,C]; h ∈ Hom[𝒞][A,B]; i ∈ Hom[𝒞][A,B]; f ≈⇘𝒞⇙ g; h ≈⇘𝒞⇙ i ⟧ ⟹ f ∘⇘𝒞⇙ h ≈⇘𝒞⇙ g ∘⇘𝒞⇙ i"
by (rule CategoryE [OF assms], simp)

lemma CategoryE_left_id:
  assumes "Category 𝒞"
  shows "(⋀A B f. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B] ⟧ ⟹ Id 𝒞 B ∘⇘𝒞⇙ f ≈⇘𝒞⇙ f)"
using Category.left_id [OF assms] by (auto simp add: hom_def)

lemma CategoryE_right_id:
  assumes "Category 𝒞"
  shows "(⋀A B f. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B] ⟧ ⟹ f ≈⇘𝒞⇙ f ∘⇘𝒞⇙ Id 𝒞 A)"
using Category.right_id [OF assms] by (auto simp add: hom_def)

lemma CategoryE_assoc:
  assumes "Category 𝒞"
  shows "⋀A B C D f g h. ⟦ A ∈ Obj 𝒞; B ∈ Obj 𝒞; C ∈ Obj 𝒞; D ∈ Obj 𝒞; f ∈ Hom[𝒞][A,B]; g ∈ Hom[𝒞][B,C]; h ∈ Hom[𝒞][C,D] ⟧ ⟹ (h ∘⇘𝒞⇙ g) ∘⇘𝒞⇙ f ≈⇘𝒞⇙ h ∘⇘𝒞⇙ (g ∘⇘𝒞⇙ f)"
using Category.assoc [OF assms] by (simp add: hom_def)

definition opposite ("_ {^op}") 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})"
proof (rule CategoryI, auto simp add: opposite_def)
  show "setoid (Arr 𝒞)"
    using assms by (unfold Category_def, auto)
next
  fix f
  { assume a: "f ∈ carrier (Arr 𝒞)" show "Cod 𝒞 f ∈ Obj 𝒞" by (rule Category.cod_obj [OF assms a]) }
  { assume a: "f ∈ carrier (Arr 𝒞)" show "Dom 𝒞 f ∈ Obj 𝒞" by (rule Category.dom_obj [OF assms a]) }
next
  fix A
  assume a: "A ∈ Obj 𝒞"
  show "id⇘𝒞⇙ A ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,A]"
    by (simp add: hom_def Category.id_exist [OF assms a])
next
  fix A B C f g
  assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "C ∈ Obj 𝒞"
  and "f ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,B]"
  and "g ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][B,C]"
  thus "f ∘⇘𝒞⇙ g ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,C]"
    by (simp add: hom_def Category.comp_exist [OF assms])
next
  fix A B C A' B' C' f g h i
  assume "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "C ∈ Obj 𝒞"
  and "f ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][B,C]"
  and "g ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][B,C]"
  and "h ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,B]"
  and "i ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,B]"
  and "f ≈⇘𝒞⇙ g" "h ≈⇘𝒞⇙ i"
  thus"h ∘⇘𝒞⇙ f ≈⇘𝒞⇙ i ∘⇘𝒞⇙ g"
    using Category.comp_equal [of 𝒞 h i f g] by (simp add: hom_def assms)
next
  fix A B f
  assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "f ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,B]"
  hence 1: "f ∈ Hom[𝒞][B,A]" by (simp add: hom_def)
  show "f ∘⇘𝒞⇙ id⇘𝒞⇙ B ≈⇘𝒞⇙ f"
    by (rule CategoryE_hom_sym [OF assms], rule CategoryE_right_id [OF assms a(2) a(1) 1])
next
  fix A B f
  assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "f ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,B]"
  hence 1: "f ∈ Hom[𝒞][B,A]" by (simp add: hom_def)
  show "f ≈⇘𝒞⇙ id⇘𝒞⇙ A ∘⇘𝒞⇙ f"
    by (rule CategoryE_hom_sym [OF assms], rule CategoryE_left_id [OF assms a(2) a(1) 1])
next
  fix A B C D f g h
  assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "C ∈ Obj 𝒞" "D ∈ Obj 𝒞"
  and "f ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][A,B]"
  and "g ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][B,C]"
  and "h ∈ Hom[⦇Obj = Obj 𝒞, Arr = Arr 𝒞, Dom = Cod 𝒞, Cod = Dom 𝒞, Id = Category.Id 𝒞, comp = λf g. g ∘⇘𝒞⇙ f⦈][C,D]"
  hence 1: "f ∈ Hom[𝒞][B,A]" "g ∈ Hom[𝒞][C,B]" "h ∈ Hom[𝒞][D,C]" by (auto simp add: hom_def)
  show "f ∘⇘𝒞⇙ (g ∘⇘𝒞⇙ h) ≈⇘𝒞⇙ f ∘⇘𝒞⇙ g ∘⇘𝒞⇙ h"
    by (rule CategoryE_hom_sym [OF assms], rule CategoryE_assoc [OF assms a(4) a(3) a(2) a(1) 1(3) 1(2) 1(1)])
qed

record ('a,'b) setmap =
  setdom :: "'a setoid"
  setcod :: "'b setoid"
  setfunction :: "'a ⇒ 'b"

locale setmap =
  fixes f :: "('a,'b,'f) setmap_scheme"
  assumes mapping: "⋀x. x ∈ setdom f ⟹ setfunction f x ∈ setcod f"
  and dom_setoid: "setoid (setdom f)"
  and cod_setoid: "setoid (setcod f)"
  and preserve_equal: "⋀x y. equal (setdom f) x y ⟹ equal (setcod f) (setfunction f x) (setfunction f y)"

lemma setmap_cod_equiv: "setmap f ⟹ equiv (setcod f) {(x,y). equal (setcod f) x y}"
using setoid.equal_equiv [OF setmap.cod_setoid [of f]] by simp

lemma setmap_cod_refl: "setmap f ⟹ x ∈ setcod f ⟹ equal (setcod f) x x"
by (rule equiv_reflp, rule setmap_cod_equiv, auto)

lemma setmap_cod_sym: "setmap f ⟹ equal (setcod f) x y ⟹ equal (setcod f) y x"
by (rule equiv_symp, rule setmap_cod_equiv, auto)

lemma setmap_cod_trans: "setmap f ⟹ equal (setcod f) x y ⟹ equal (setcod f) y z ⟹ equal (setcod f) x z"
by (rule equiv_transp, rule setmap_cod_equiv, auto)

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

lemma setmap_eqI: "⟦ setdom f = setdom g; setcod f = setcod g; (⋀x. x ∈ setdom f ⟹ equal (setcod f) (setfunction f x) (setfunction g x)) ⟧ 
  ⟹ setmap_eq f g"
by (simp add: setmap_eq_def)

definition setmap_comp ("_ ∘[setmap] _" 80) where
  "g ∘[setmap] f ≡ ⦇ setdom = setdom f, setcod = setcod g, setfunction = (λx. setfunction g (setfunction f x)) ⦈"

lemma setmap_comp_setmap:
  assumes "setmap g" "setmap f" "setcod f = setdom g"
  shows "setmap (g ∘[setmap] f)"
apply (unfold setmap_comp_def setmap_def, auto)
using assms by (auto simp add: setmap_def)

definition idsetmap where
  "idsetmap A ≡ ⦇ setdom = A, setcod = A, setfunction = (λx. x) ⦈"

lemma id_setmap: "setoid A ⟹ setmap (idsetmap A)"
by (unfold idsetmap_def setmap_def, auto)

definition Setoid where
  "Setoid ≡ ⦇
    Obj = {A. setoid A},
    Arr = ⦇ carrier = {f. setmap f}, equal = (λf g. setmap f ∧ setmap g ∧ setmap_eq f g) ⦈,
    Dom = setdom,
    Cod = setcod,
    Id = idsetmap,
    comp = setmap_comp
  ⦈"

lemma Setoid_Category: "Category Setoid"
proof (rule CategoryI)
  show "setoid (Arr Setoid)"
    proof (unfold Setoid_def setoid_def, auto, rule equivI)
      show "refl_on (Collect setmap) {(x, y). setmap x ∧ setmap y ∧ setmap_eq x y}"
        apply (rule refl_onI, auto, unfold setmap_eq_def, auto)
        by (rule setmap_cod_refl, auto simp add: setmap_def)
      show "sym {(x, y). setmap x ∧ setmap y ∧ setmap_eq x y}"
        apply (rule symI, auto simp add: setmap_eq_def)
        by (rule setmap_cod_sym, auto simp add: setmap_def)
      show "transP (λx y. setmap x ∧ setmap y ∧ setmap_eq x y)"
        apply (rule transI, auto simp add: setmap_eq_def)
        by (rule setmap_cod_trans, auto simp add: setmap_def)
    qed
next
  fix f :: "('a,'a) setmap"
  assume "f ∈ carrier (Arr Setoid)" thus "Dom Setoid f ∈ Obj Setoid"
    apply (unfold Setoid_def, auto) by (metis setmap.dom_setoid)
next
  fix f :: "('a,'a) setmap"
  assume "f ∈ carrier (Arr Setoid)" thus "Cod Setoid f ∈ Obj Setoid"
    apply (unfold Setoid_def, auto) by (metis setmap.cod_setoid)
next
  fix A :: "'a setoid"
  assume "A ∈ Obj Setoid" thus "id⇘Setoid⇙ A ∈ Hom[Setoid][A,A]"
    by (unfold Setoid_def hom_def, simp, simp add: id_setmap, simp add: idsetmap_def)
next
  fix A B C :: "'a setoid" and f g
  assume "A ∈ Obj Setoid" "B ∈ Obj Setoid" "C ∈ Obj Setoid" "f ∈ Hom[Setoid][A,B]" "g ∈ Hom[Setoid][B,C]"
  thus "g ∘⇘Setoid⇙ f ∈ Hom[Setoid][A,C]"
    by (unfold Setoid_def hom_def, simp add: setmap_comp_setmap, unfold setmap_comp_def, auto)
next
  fix A B C :: "'a setoid" and f g h i
  assume a: "A ∈ Obj Setoid" "B ∈ Obj Setoid" "C ∈ Obj Setoid"
  and b: "f ∈ Hom[Setoid][B,C]" "g ∈ Hom[Setoid][B,C]" "h ∈ Hom[Setoid][A,B]" "i ∈ Hom[Setoid][A,B]"
  and c: "f ≈⇘Setoid⇙ g" "h ≈⇘Setoid⇙ i"
  have b2: "setmap f" "setmap g" "setmap h" "setmap i"
    using b by (auto simp add: Setoid_def hom_def)

  have h: "setmap_eq (f ∘[setmap] h) (g ∘[setmap] i)"
    apply (unfold setmap_eq_def, auto)
    using b(3) b(4) apply (simp add: setmap_comp_def hom_def Setoid_def)
    using b(1) b(2) apply (simp add: setmap_comp_def hom_def Setoid_def)
    apply (simp add: setmap_comp_def)
    apply (rule setmap_cod_trans, rule b2(1))
      apply (rule setmap.preserve_equal [of f], rule b2(1))
      using b c(2) apply (simp add: Setoid_def hom_def setmap_eq_def, fastforce)
      using b c(1) apply (simp add: Setoid_def hom_def setmap_eq_def setmap_def, fastforce)
    done
  show "f ∘⇘Setoid⇙ h ≈⇘Setoid⇙ g ∘⇘Setoid⇙ i"
    apply (unfold Setoid_def hom_def, auto)
    apply (rule setmap_comp_setmap, rule b2, rule b2) using b apply (simp add: hom_def Setoid_def)
    apply (rule setmap_comp_setmap, rule b2, rule b2) using b apply (simp add: hom_def Setoid_def)
    apply (rule h)
    done
next
  fix A B :: "'a setoid" and f
  assume "A ∈ Obj Setoid" "B ∈ Obj Setoid" "f ∈ Hom[Setoid][A,B]"
  thus "id⇘Setoid⇙ B ∘⇘Setoid⇙ f ≈⇘Setoid⇙ f"
    apply (unfold Setoid_def hom_def, simp)
    apply (rule, rule setmap_comp_setmap, rule id_setmap, simp, simp, simp add: idsetmap_def)
    apply (simp add: idsetmap_def setmap_eq_def setmap_comp_def, auto)
    apply (rule setmap_cod_refl, auto simp add: Setoid_def hom_def setmap_def)
    done
next
  fix A B :: "'a setoid" and f
  assume "A ∈ Obj Setoid" "B ∈ Obj Setoid" "f ∈ Hom[Setoid][A,B]"
  thus "f ≈⇘Setoid⇙ f ∘⇘Setoid⇙ id⇘Setoid⇙ A"
    apply (unfold Setoid_def hom_def, simp)
    apply (rule, rule setmap_comp_setmap, simp, rule id_setmap, simp, simp add: idsetmap_def)
    apply (simp add: idsetmap_def setmap_eq_def setmap_comp_def, auto)
    apply (rule setmap_cod_refl, auto simp add: Setoid_def hom_def setmap_def)
    done
next
  fix A B C D :: "'a setoid" and f g h
  assume "A ∈ Obj Setoid" "B ∈ Obj Setoid" "C ∈ Obj Setoid" "D ∈ Obj Setoid"
  and "f ∈ Hom[Setoid][A,B]" "g ∈ Hom[Setoid][B,C]" "h ∈ Hom[Setoid][C,D]"
  thus "h ∘⇘Setoid⇙ g ∘⇘Setoid⇙ f ≈⇘Setoid⇙ h ∘⇘Setoid⇙ (g ∘⇘Setoid⇙ f)"
    apply (unfold Setoid_def hom_def, auto)
    apply (auto simp add: setmap_comp_def setmap_def setmap_eq_def)
    apply (rule setmap_cod_refl, auto simp add: Setoid_def hom_def)
    done
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 fobj_mapping: "X ∈ Obj (domCat F) ⟹ fobj F X ∈ Obj (codCat F)"
  and fmap_mapping: "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: "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"
  and preserve_equal: "⟦ f ∈ Arr (domCat F); g ∈ Arr (domCat F); Dom (domCat F) f = Dom (domCat F) g; Cod (domCat F) f = Cod (domCat F) g; f ≈⇘domCat F⇙ g ⟧
    ⟹ fmap F f ≈⇘codCat F⇙ fmap F g"

abbreviation Functor_type ("Functor' _ : _ ⟶ _" 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]) ⟹
   (X ∈ Obj 𝒞 ⟹ fmap F (Id 𝒞 X) ≈⇘𝒟⇙ Id 𝒟 (fobj F X)) ⟹
   (f ∈ Hom[𝒞][A,B] ⟹ g ∈ Hom[𝒞][B,C] ⟹ fmap F (g ∘⇘𝒞⇙ f) ≈⇘𝒟⇙ fmap F g ∘⇘𝒟⇙ fmap F f) ⟹
   (A ∈ Obj 𝒞 ⟹ B ∈ Obj 𝒞 ⟹ f ∈ Hom[𝒞][A,B] ⟹ g ∈ Hom[𝒞][A,B] ⟹ f ≈⇘𝒞⇙ g ⟹ fmap F f ≈⇘𝒟⇙ fmap F g) ⟹
  thesis) ⟹ thesis"
by (auto simp add: Functor_def hom_def)

lemma FunctorE_cod_category: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ Category 𝒟" by (metis FunctorE)
lemma FunctorE_fobj: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ X ∈ Obj 𝒞 ⟹ fobj F X ∈ Obj 𝒟" by (metis FunctorE)
lemma FunctorE_fmap: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ f ∈ Hom[𝒞][A,B] ⟹ fmap F f ∈ Hom[𝒟][fobj F A,fobj F B]" by (metis FunctorE)
lemma FunctorE_preserver_id: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ X ∈ Obj 𝒞 ⟹ fmap F (Id 𝒞 X) ≈⇘𝒟⇙ Id 𝒟 (fobj F X)" by (metis FunctorE)
lemma FunctorE_preserver_comp: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ f ∈ Hom[𝒞][A,B] ⟹ g ∈ Hom[𝒞][B,C] ⟹ fmap F (g ∘⇘𝒞⇙ f) ≈⇘𝒟⇙ fmap F g ∘⇘𝒟⇙ fmap F f" by (metis FunctorE)
lemma FunctorE_preserver_equal: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ A ∈ Obj 𝒞 ⟹ B ∈ Obj 𝒞 ⟹ f ∈ Hom[𝒞][A,B] ⟹ g ∈ Hom[𝒞][A,B] ⟹ f ≈⇘𝒞⇙ g ⟹ fmap F f ≈⇘𝒟⇙ fmap F g" by (metis FunctorE)

lemma FunctorI:
  fixes F :: "('o,'a,'c,'o2,'a2,'d,'f) Functor_scheme"
  assumes "Category 𝒞" "Category 𝒟"
  and "domCat F = 𝒞" "codCat F = 𝒟"
  and "⋀X. X ∈ Obj 𝒞 ⟹ fobj F X ∈ Obj 𝒟"
  and "⋀A B f. f ∈ Hom[𝒞][A,B] ⟹ fmap F f ∈ Hom[𝒟][fobj F A,fobj F B]"
  and "⋀X. X ∈ Obj 𝒞 ⟹ fmap F (Id 𝒞 X) ≈⇘𝒟⇙ Id 𝒟 (fobj F X)"
  and "⋀A B C f g. A ∈ Obj 𝒞 ⟹ B ∈ Obj 𝒞 ⟹ C ∈ Obj 𝒞 ⟹ f ∈ Hom[𝒞][A,B] ⟹ g ∈ Hom[𝒞][B,C] ⟹ fmap F (g ∘⇘𝒞⇙ f) ≈⇘𝒟⇙ fmap F g ∘⇘𝒟⇙ fmap F f"
  and "⋀A B f g. A ∈ Obj 𝒞 ⟹ B ∈ Obj 𝒞 ⟹ f ∈ Hom[𝒞][A,B] ⟹ g ∈ Hom[𝒞][A,B] ⟹ f ≈⇘𝒞⇙ g ⟹ fmap F f ≈⇘𝒟⇙ fmap F g"
  shows "Functor' F : 𝒞 ⟶ 𝒟"
apply (unfold Functor_def, auto simp add: assms(3) assms(4))
apply (rule assms(1), rule assms(2), simp add: assms(5))
using assms(6) apply (simp add: hom_def)
using assms(6) apply (simp add: hom_def)
using assms(6) apply (simp add: hom_def)
apply (simp add: assms(7))
using assms(8) apply (simp add: hom_def)
apply (metis Category.cod_obj Category.dom_obj assms(1))
using assms(9) apply (simp add: hom_def)
apply (metis Category.cod_obj Category.dom_obj assms(1))
done

definition idFunctor where
  "idFunctor 𝒞 ≡ ⦇ domCat = 𝒞, codCat = 𝒞, fobj = λX. X, fmap = λf. f ⦈"

lemma id_Functor:
  assumes "Category 𝒞"
  shows "Functor' (idFunctor 𝒞) : 𝒞 ⟶ 𝒞"
apply (rule FunctorI, unfold idFunctor_def, auto, rule assms, rule assms)
apply (rule CategoryE_hom_refl [OF assms], rule CategoryE [OF assms], auto)
apply (rule CategoryE_hom_refl [OF assms])
apply (rule CategoryE_comp_exist [OF assms], auto simp add: hom_def)
done

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 η)"
  and cod_functor: "Functor (codFunctor η)"
  and component_mapping: "X ∈ Obj (domCat (domFunctor η))
    ⟹ component η X ∈ Hom[codCat (domFunctor η)][fobj (domFunctor η) X, fobj (codFunctor η) X]"
  and naturality: "f ∈ Arr (domCat (domFunctor η)) ⟹
    (component η (Cod (domCat (domFunctor η)) f) ∘⇘codCat (domFunctor η)⇙ fmap (domFunctor η) f) ≈⇘codCat (domFunctor η)⇙
    (fmap (codFunctor η) f ∘⇘codCat (domFunctor η)⇙ component η (Dom (domCat (domFunctor η)) f))"
 
abbreviation Nat_type ("Nat' _ : _ ⟶ _" [81] 90) where
  "Nat' η : F ⟶ G ≡ Nat η & Nat.domFunctor η = F & Nat.codFunctor η = G"

lemma NatI:
  fixes η :: "('o,'a,'c,'o2,'a2,'d,'f,'f2,'n) Nat_scheme"
  assumes "Functor' F : 𝒞 ⟶ 𝒟" "Functor' G : 𝒞 ⟶ 𝒟"
  and "domFunctor η = F" "codFunctor η = G"
  and "⋀X. X ∈ Obj 𝒞 ⟹ component η X ∈ Hom[𝒟][fobj F X, fobj G X]"
  and "⋀A B f. A ∈ Obj 𝒞 ⟹ B ∈ Obj 𝒞 ⟹ f ∈ Hom[𝒞][A,B] ⟹ (component η B ∘⇘𝒟⇙ fmap F f ≈⇘𝒟⇙ fmap G f ∘⇘𝒟⇙ component η A)"
  shows "Nat' η : F ⟶ G"
apply (unfold Nat_def, auto simp add: assms hom_def)
using assms(5) apply (simp add: hom_def)
using assms(5) apply (simp add: hom_def)
using assms(5) apply (simp add: hom_def)
using assms(6)
by (metis (mono_tags, lifting) Category.cod_obj Category.dom_obj Functor.dom_category assms(2) hom_def mem_Collect_eq setoid.select_convs(1))

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

lemma NatE_component: "⟦ Nat' η : F ⟶ G; A ∈ Obj (domCat F) ⟧ ⟹ component η A ∈ Hom[codCat F][fobj F A,fobj G A]"
by (metis NatE)

lemma NatE_naturality: "⟦ Nat' η : F ⟶ G; f ∈ Hom[domCat F][A,B] ⟧ ⟹ (component η B ∘⇘codCat F⇙ fmap F f) ≈⇘codCat F⇙ (fmap G f ∘⇘codCat F⇙ component η A)"
by (simp add: Nat_def hom_def, auto)

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

lemma id_Nat:
  assumes "Functor' F : 𝒞 ⟶ 𝒟"
  shows "Nat' (idNat F) : F ⟶ F"
apply (rule NatI, simp add: assms, simp add: assms, unfold idNat_def, auto)
apply (simp add: assms)
apply (rule CategoryE_id_exist [OF FunctorE_cod_category [OF assms]])
apply (rule FunctorE_fobj [OF assms], simp)
proof (simp add: assms)
  fix A B f
  assume "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "f ∈ Hom[𝒞][A,B]"
  show "id⇘𝒟⇙ fobj F B ∘⇘𝒟⇙ fmap F f ≈⇘𝒟⇙ fmap F f ∘⇘𝒟⇙ id⇘𝒟⇙ fobj F A"
    proof-
      have "id⇘𝒟⇙ fobj F B ∘⇘𝒟⇙ fmap F f ≈⇘𝒟⇙ fmap F f"
        apply (rule CategoryE_left_id [OF FunctorE_cod_category [OF assms]])
        apply (rule FunctorE_fobj [OF assms `A ∈ Obj 𝒞`])
        apply (rule FunctorE_fobj [OF assms `B ∈ Obj 𝒞`])
        apply (rule FunctorE_fmap [OF assms `f ∈ Hom[𝒞][A,B]`]) done
      moreover have "… ≈⇘𝒟⇙ fmap F f ∘⇘𝒟⇙ id⇘𝒟⇙ fobj F A"
        apply (rule CategoryE_right_id [OF FunctorE_cod_category [OF assms]])
        apply (rule FunctorE_fobj [OF assms `A ∈ Obj 𝒞`])
        apply (rule FunctorE_fobj [OF assms `B ∈ Obj 𝒞`])
        apply (rule FunctorE_fmap [OF assms `f ∈ Hom[𝒞][A,B]`]) done
      ultimately
        show ?thesis
          using CategoryE_hom_trans [OF FunctorE_cod_category [OF assms]] by blast
    qed
qed

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

lemma compNat_Nat:
  assumes "Nat' η : F ⟶ G" "Nat' ε : G ⟶ H"
  shows "Nat' (ε ∘[Nat] η) : F ⟶ H"
apply (rule NatI)
apply (rule NatE [OF assms(1)], simp)
apply (rule NatE [OF assms(2)], simp)
apply (unfold compNat_def, auto simp add: assms)
proof-
  def 𝒞 ≡ "domCat F"
  def 𝒟 ≡ "codCat F"

  have F: "Functor' F : 𝒞 ⟶ 𝒟" by (simp add: 𝒞_def 𝒟_def, rule NatE [OF assms(1)], simp)
  have G: "Functor' G : 𝒞 ⟶ 𝒟" by (simp add: 𝒞_def 𝒟_def, rule NatE [OF assms(1)], simp)
  have H: "Functor' H : 𝒞 ⟶ 𝒟" by (rule NatE [OF assms(2)], simp add: G)

  have 𝒞_cat: "Category 𝒞" by (unfold 𝒞_def, rule NatE [OF assms(1)], rule FunctorE, auto)
  have 𝒟_cat: "Category 𝒟" by (unfold 𝒟_def, rule NatE [OF assms(1)], rule FunctorE_cod_category, auto)

  {
    fix X
    assume "X ∈ Obj (domCat G)" thus "component ε X ∘⇘codCat G⇙ component η X ∈ Hom[codCat G][fobj F X,fobj H X]"
      proof (simp add: G)
        assume a: "X ∈ Obj 𝒞"
        show "component ε X ∘⇘𝒟⇙ component η X ∈ Hom[𝒟][fobj F X,fobj H X]"
          apply (rule CategoryE_comp_exist [OF 𝒟_cat FunctorE_fobj [OF F a] FunctorE_fobj [OF G a] FunctorE_fobj [OF H a]])
          using NatE_component [OF assms(1)] apply (simp add: F a)
          using NatE_component [OF assms(2)] apply (simp add: G a)
          done
      qed
  }
  {
    fix A B f
    assume "A ∈ Obj (domCat G)" "B ∈ Obj (domCat G)" "f ∈ Hom[domCat G][A,B]"
    thus "component ε B ∘⇘codCat G⇙ component η B ∘⇘codCat G⇙ fmap F f ≈⇘codCat G⇙
          fmap H f ∘⇘codCat G⇙ (component ε A ∘⇘codCat G⇙ component η A)"
      proof (simp add: G)
        assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "f ∈ Hom[𝒞][A,B]"
        have Ff: "fmap F f ∈ Hom[𝒟][fobj F A, fobj F B]"
          by (rule FunctorE_fmap [OF F], rule a(3))
        have Gf: "fmap G f ∈ Hom[𝒟][fobj G A, fobj G B]"
          by (rule FunctorE_fmap [OF G], rule a(3))
        have Hf: "fmap H f ∈ Hom[𝒟][fobj H A, fobj H B]"
          by (rule FunctorE_fmap [OF H], rule a(3))
        have εX: "⋀X. X ∈ Obj 𝒞 ⟹ component ε X ∈ Hom[𝒟][fobj G X, fobj H X]"
          using NatE_component [OF assms(2)] by (simp add: G a(2))
        have ηX: "⋀X. X ∈ Obj 𝒞 ⟹ component η X ∈ Hom[𝒟][fobj F X, fobj G X]"
          using NatE_component [OF assms(1)] by (simp add: F a(2))

        have 1: "(component ε B ∘⇘𝒟⇙ component η B) ∘⇘𝒟⇙ fmap F f ≈⇘𝒟⇙ component ε B ∘⇘𝒟⇙ (component η B ∘⇘𝒟⇙ fmap F f)"
          apply (rule CategoryE_assoc [OF 𝒟_cat _ _ _ _ Ff ηX εX])
          apply (auto simp add: a FunctorE_fobj F G H) done
        have 2: "… ≈⇘𝒟⇙ component ε B ∘⇘𝒟⇙ (fmap G f ∘⇘𝒟⇙ component η A)"
          apply (rule CategoryE_comp_equal [OF 𝒟_cat _ _ _ εX εX], rule FunctorE_fobj [OF F], rule a(1))
          apply (auto simp add: FunctorE_fobj G H a)
          apply (rule CategoryE_comp_exist [OF 𝒟_cat FunctorE_fobj [OF F a(1)] FunctorE_fobj [OF F a(2)] FunctorE_fobj [OF G a(2)]])
          apply (auto simp add: Ff ηX [OF a(2)])
          apply (rule CategoryE_comp_exist [OF 𝒟_cat FunctorE_fobj [OF F a(1)] FunctorE_fobj [OF G a(1)] FunctorE_fobj [OF G a(2)]])
          apply (auto simp add: Gf ηX [OF a(1)])
          apply (rule CategoryE_hom_refl [OF 𝒟_cat], rule εX [OF a(2)])
          using NatE_naturality [OF assms(1)] apply (simp add: F a(3))
          done
        have 3: "… ≈⇘𝒟⇙ (component ε B ∘⇘𝒟⇙ fmap G f) ∘⇘𝒟⇙ component η A"
          apply (rule CategoryE_hom_sym [OF 𝒟_cat CategoryE_assoc [OF 𝒟_cat _ _ _ _ ηX Gf εX]])
          apply (auto simp add: FunctorE_fobj F G H a) done
        have 4: "… ≈⇘𝒟⇙ (fmap H f ∘⇘𝒟⇙ component ε A) ∘⇘𝒟⇙ component η A"
          apply (rule CategoryE_comp_equal [OF 𝒟_cat _ _ _ _ _ ηX ηX], auto simp add: FunctorE_fobj F G a)
          apply (rule FunctorE_fobj [OF H a(2)])
          apply (rule CategoryE_comp_exist [OF 𝒟_cat _ _ _ Gf], auto simp add: FunctorE_fobj F G H a εX)
          apply (rule CategoryE_comp_exist [OF 𝒟_cat _ _ _ εX Hf], auto simp add: FunctorE_fobj G H a)
          using NatE_naturality [OF assms(2)] apply (simp add: G a(3))
          apply (rule CategoryE_hom_refl [OF 𝒟_cat], rule ηX [OF a(1)])
          done
        have 5: "… ≈⇘𝒟⇙ fmap H f ∘⇘𝒟⇙ (component ε A ∘⇘𝒟⇙ component η A)"
          apply (rule CategoryE_assoc [OF 𝒟_cat _ _ _ _ ηX εX Hf])
          apply (auto simp add: FunctorE_fobj F G H a) done

        show "(component ε B ∘⇘𝒟⇙ component η B) ∘⇘𝒟⇙ fmap F f ≈⇘𝒟⇙ fmap H f ∘⇘𝒟⇙ (component ε A ∘⇘𝒟⇙ component η A)"
          by (rule CategoryE_hom_trans [OF 𝒟_cat CategoryE_hom_trans [OF 𝒟_cat 1 2] CategoryE_hom_trans [OF 𝒟_cat 3 CategoryE_hom_trans [OF 𝒟_cat 4 5]]])
      qed
  }
qed

definition Nat_equal where
  "Nat_equal η ε ≡ (domFunctor η = domFunctor ε ∧ codFunctor η = codFunctor ε ∧
    (∀X. X ∈ Obj (domCat (domFunctor η)) ⟶ component η X ≈⇘codCat (domFunctor η)⇙ component ε X))"

lemma Nat_equalI:
  assumes "Nat' η : F ⟶ G" "Nat' ε : F ⟶ G"
  and "⋀X. X ∈ Obj (domCat F) ⟹ component η X ≈⇘codCat F⇙ component ε X"
  shows "Nat_equal η ε"
by (unfold Nat_equal_def, auto simp add: assms)

lemma Nat_equalE_equal:
  "Nat_equal η ε ⟹ X ∈ Obj (domCat (domFunctor η)) ⟹ component η X ≈⇘codCat (domFunctor η)⇙ component ε X"
using assms by (unfold Nat_equal_def, auto)

definition FunCat ("Cat[_,_]") where
  "Cat[𝒞,𝒟] ≡ ⦇
    Obj = {F. Functor' F : 𝒞 ⟶ 𝒟},
    Arr = ⦇ carrier = {η. ∃F. ∃G. (Nat' η : F ⟶ G) ∧ (Functor' F : 𝒞 ⟶ 𝒟) ∧ (Functor' G : 𝒞 ⟶ 𝒟)},
            equal = λη ε. ∃F. ∃G. (Nat_equal η ε) ∧ (Nat' η : F ⟶ G) ∧ (Nat' ε : F ⟶ G) ∧ (Functor' F : 𝒞 ⟶ 𝒟) ∧ (Functor' G : 𝒞 ⟶ 𝒟) ⦈,
    Dom = domFunctor,
    Cod = codFunctor,
    Id = idNat,
    comp = compNat
  ⦈"

lemma FunCat_Category:
  assumes "Category 𝒞" "Category 𝒟"
  shows "Category Cat[𝒞,𝒟]"
proof (rule CategoryI)
  show "setoid (Arr Cat[𝒞,𝒟])"
    proof (unfold setoid_def, rule equivI)
      show "refl_on (carrier (Arr Cat[𝒞,𝒟])) {(x, y). x ≈⇘Cat[𝒞,𝒟]⇙ y}"
        apply (unfold FunCat_def, auto, rule refl_onI, auto)
        apply (unfold Nat_equal_def, auto)
        apply (rule CategoryE_hom_refl, metis assms(2))
        apply (rule NatE_component, auto)
        done
      show "sym {(x, y). x ≈⇘Cat[𝒞,𝒟]⇙ y}"
        apply (rule symI, simp add: FunCat_def, auto)
        apply (rule Nat_equalI, simp, simp)
        apply (rule CategoryE_hom_sym, metis assms(2), rule Nat_equalE_equal, auto)
        done
      show "transP op ≈⇘Cat[𝒞,𝒟]⇙"
        apply (simp add: transp_trans [symmetric], rule transpI)
        apply (unfold FunCat_def, simp, unfold Nat_equal_def, auto)
        apply (rule CategoryE_hom_trans, metis assms(2), auto)
        done
    qed
next
  fix f assume "f ∈ carrier (Arr Cat[𝒞,𝒟])"
  thus "Dom Cat[𝒞,𝒟] f ∈ Obj Cat[𝒞,𝒟]" by (unfold FunCat_def, simp)
next
  fix f assume "f ∈ carrier (Arr Cat[𝒞,𝒟])"
  thus "Cod Cat[𝒞,𝒟] f ∈ Obj Cat[𝒞,𝒟]" by (unfold FunCat_def, auto)
next
  fix A assume "A ∈ Obj Cat[𝒞,𝒟]"
  thus "id⇘Cat[𝒞,𝒟]⇙ A ∈ Hom[Cat[𝒞,𝒟]][A,A]" by (unfold FunCat_def hom_def, auto, auto simp add: id_Nat)
next
  fix A B C f g
  assume "A ∈ Obj Cat[𝒞,𝒟]" "B ∈ Obj Cat[𝒞,𝒟]" "C ∈ Obj Cat[𝒞,𝒟]"
  and "f ∈ Hom[Cat[𝒞,𝒟]][A,B]" "g ∈ Hom[Cat[𝒞,𝒟]][B,C]"
  thus "g ∘⇘Cat[𝒞,𝒟]⇙ f ∈ Hom[Cat[𝒞,𝒟]][A,C]" by (simp add: hom_def FunCat_def compNat_Nat)
next
  fix A B C f g h i
  assume a: "A ∈ Obj Cat[𝒞,𝒟]" "B ∈ Obj Cat[𝒞,𝒟]" "C ∈ Obj Cat[𝒞,𝒟]"
  and b: "f ∈ Hom[Cat[𝒞,𝒟]][B,C]" "g ∈ Hom[Cat[𝒞,𝒟]][B,C]" "h ∈ Hom[Cat[𝒞,𝒟]][A,B]" "i ∈ Hom[Cat[𝒞,𝒟]][A,B]"
  and c: "f ≈⇘Cat[𝒞,𝒟]⇙ g" "h ≈⇘Cat[𝒞,𝒟]⇙ i"

  have a2: "Functor' A : 𝒞 ⟶ 𝒟" "Functor' B : 𝒞 ⟶ 𝒟" "Functor' C : 𝒞 ⟶ 𝒟"
    using a(1) apply (simp add: FunCat_def)
    using a(2) apply (simp add: FunCat_def)
    using a(3) apply (simp add: FunCat_def) done
  have b2: "Nat' f : B ⟶ C" "Nat' g : B ⟶ C" "Nat' h : A ⟶ B" "Nat' i : A ⟶ B"
    using b(1) apply (simp add: FunCat_def hom_def)
    using b(2) apply (simp add: FunCat_def hom_def)
    using b(3) apply (simp add: FunCat_def hom_def)
    using b(4) apply (simp add: FunCat_def hom_def) done
  have h: "⋀A B C f g h i. ⟦ Functor' A : 𝒞 ⟶ 𝒟; Functor' B : 𝒞 ⟶ 𝒟; Functor' C : 𝒞 ⟶ 𝒟; Nat' f : B ⟶ C; Nat' g : B ⟶ C; Nat' h : A ⟶ B; Nat' i : A ⟶ B; Nat_equal f g; Nat_equal h i ⟧ ⟹ Nat_equal (f ∘[Nat] h) (g ∘[Nat] i)"
    apply (rule Nat_equalI)
    apply (rule compNat_Nat, simp, simp)
    apply (rule compNat_Nat, simp, simp)
    apply (unfold compNat_def, simp)
    apply (rule CategoryE_comp_equal [OF assms(2)])
    prefer 4 using NatE_component apply (rule, simp, simp, fastforce)
    prefer 2 apply (rule FunctorE_fobj, simp, simp)
    prefer 2 apply (rule FunctorE_fobj, simp, simp)
    prefer 2 using NatE_component apply (rule, simp, simp, fastforce)
    prefer 2 using NatE_component apply (rule, simp, simp, fastforce)
    apply (rule FunctorE_fobj, simp, simp)
    using NatE_component apply (rule, simp, simp, fastforce)
    apply (unfold Nat_equal_def, auto)
    done
  show "f ∘⇘Cat[𝒞,𝒟]⇙ h ≈⇘Cat[𝒞,𝒟]⇙ g ∘⇘Cat[𝒞,𝒟]⇙ i"
    apply (unfold FunCat_def, auto)
    apply (rule h, auto simp add: a2 b2)
    using c(1) apply (simp add: FunCat_def)
    using c(2) apply (simp add: FunCat_def)
    using compNat_Nat [OF b2(3) b2(1)] apply simp
    using compNat_Nat [OF b2(4) b2(2)] apply simp
    apply (auto simp add: compNat_def a2 b2)
    done
next
  fix A B f
  assume a: "A ∈ Obj Cat[𝒞,𝒟]" "B ∈ Obj Cat[𝒞,𝒟]" "f ∈ Hom[Cat[𝒞,𝒟]][A,B]"
  show "id⇘Cat[𝒞,𝒟]⇙ B ∘⇘Cat[𝒞,𝒟]⇙ f ≈⇘Cat[𝒞,𝒟]⇙ f"
    apply (simp add: FunCat_def hom_def, auto)
    defer
    using compNat_Nat [of f A B "idNat B" B] a apply (simp add: hom_def FunCat_def id_Nat)
    using a(3) apply (simp add: hom_def FunCat_def)
    using a(3) apply (simp add: compNat_def FunCat_def hom_def)
    using a(3) apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    using a apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    using a apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    using a apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    using a apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    using a apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    using a apply (simp add: compNat_def FunCat_def hom_def idNat_def)
    apply (rule Nat_equalI)
      apply (rule compNat_Nat) using a(3) apply (simp add: FunCat_def hom_def)
      apply (rule id_Nat) using a(2) apply (simp add: FunCat_def)
      using a(3) apply (simp add: FunCat_def hom_def)
      apply (simp add: compNat_def idNat_def)
      using a(1) a(2)
      proof (simp add: FunCat_def)
        fix X
        assume a2: "X ∈ Obj 𝒞" "Functor' A : 𝒞 ⟶ 𝒟" "Functor' B : 𝒞 ⟶ 𝒟"
        show "id⇘𝒟⇙ fobj B X ∘⇘𝒟⇙ component f X ≈⇘𝒟⇙ component f X"
          apply (rule CategoryE_left_id [OF FunctorE_cod_category [OF a2(2)]])
          apply (auto simp add: FunctorE_fobj a2)
          using a(3) apply (simp add: FunCat_def hom_def)
          apply (rule FunctorE_fobj [OF a2(2) a2(1)])
          using NatE_component [of f A B X] a a2(1) by (simp add: FunCat_def hom_def)
      qed
next
  fix A B f
  assume a: "A ∈ Obj Cat[𝒞,𝒟]" "B ∈ Obj Cat[𝒞,𝒟]" "f ∈ Hom[Cat[𝒞,𝒟]][A,B]"
  have a2: "Functor' A : 𝒞 ⟶ 𝒟" "Functor' B : 𝒞 ⟶ 𝒟" "Nat' f : A ⟶ B"
    using a(1) apply (simp add: FunCat_def)
    using a(2) apply (simp add: FunCat_def)
    using a(3) apply (simp add: FunCat_def hom_def) done
  show "f ≈⇘Cat[𝒞,𝒟]⇙ f ∘⇘Cat[𝒞,𝒟]⇙ id⇘Cat[𝒞,𝒟]⇙ A"
    apply (simp add: FunCat_def hom_def, auto)
    defer
    apply (simp add: a2(3))
    using compNat_Nat [of "idNat A" A A f B] a apply (simp add: hom_def FunCat_def id_Nat)
    apply (simp add: compNat_def idNat_def a2(3))
    apply (simp add: compNat_def idNat_def a2(3))
    apply (simp add: a2)+
    apply (rule Nat_equalI, rule a2)
      apply (rule compNat_Nat, rule id_Nat, rule a2, rule a2)
      apply (simp add: a2 compNat_def idNat_def)
      apply (rule CategoryE_right_id [OF assms(2)])
      apply (simp add: FunctorE_fobj [OF a2(1)], rule FunctorE_fobj [OF a2(2)], simp)
      using NatE_component [OF a2(3)] apply (simp add: a2)
      done
next
  fix A B C D f g h
  assume a: "A ∈ Obj Cat[𝒞,𝒟]" "B ∈ Obj Cat[𝒞,𝒟]" "C ∈ Obj Cat[𝒞,𝒟]" "D ∈ Obj Cat[𝒞,𝒟]"
  and b: "f ∈ Hom[Cat[𝒞,𝒟]][A,B]" "g ∈ Hom[Cat[𝒞,𝒟]][B,C]" "h ∈ Hom[Cat[𝒞,𝒟]][C,D]"

  have a2: "Functor' A : 𝒞 ⟶ 𝒟" "Functor' B : 𝒞 ⟶ 𝒟" "Functor' C : 𝒞 ⟶ 𝒟" "Functor' D : 𝒞 ⟶ 𝒟"
    using a(1) apply (simp add: FunCat_def)
    using a(2) apply (simp add: FunCat_def)
    using a(3) apply (simp add: FunCat_def)
    using a(4) apply (simp add: FunCat_def) done

  have b2: "Nat' f : A ⟶ B" "Nat' g : B ⟶ C" "Nat' h : C ⟶ D"
    using b(1) apply (simp add: FunCat_def hom_def)
    using b(2) apply (simp add: FunCat_def hom_def)
    using b(3) apply (simp add: FunCat_def hom_def) done

  have h: "Nat_equal ((h ∘[Nat] g) ∘[Nat] f) (h ∘[Nat] (g ∘[Nat] f))"
    apply (rule Nat_equalI)
    apply (rule compNat_Nat, rule b2, rule compNat_Nat, rule b2, rule b2)
    apply (rule compNat_Nat, rule compNat_Nat, rule b2, rule b2, rule b2)
    apply (simp add: compNat_def a2 b2)
    apply (rule CategoryE_assoc [OF assms(2)])
    apply (rule FunctorE_fobj [OF a2(1)], simp)
    apply (rule FunctorE_fobj [OF a2(2)], simp)
    apply (rule FunctorE_fobj [OF a2(3)], simp)
    apply (rule FunctorE_fobj [OF a2(4)], simp)
    using NatE_component [OF b2(1)] apply (fastforce simp add: a2)
    using NatE_component [OF b2(2)] apply (fastforce simp add: a2)
    using NatE_component [OF b2(3)] apply (fastforce simp add: a2)
    done

  show "h ∘⇘Cat[𝒞,𝒟]⇙ g ∘⇘Cat[𝒞,𝒟]⇙ f ≈⇘Cat[𝒞,𝒟]⇙ h ∘⇘Cat[𝒞,𝒟]⇙ (g ∘⇘Cat[𝒞,𝒟]⇙ f)"
    apply (simp add: FunCat_def, auto)
    apply (rule h)
    apply (metis compNat_Nat b2)
    apply (metis compNat_Nat b2)
    apply (auto simp add: compNat_def b2 a2)
    done
qed

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

lemma Presheaf_Category: "Category 𝒞 ⟹ Category (PSh 𝒞)"
by (simp add: Presheaf_def, rule FunCat_Category, simp add: opposite_Category, rule Setoid_Category)

definition contraHom ("Hom{_}[-,_]") where
  "Hom{𝒞}[-,C] ≡ ⦇
    domCat = 𝒞 {^op},
    codCat = Setoid,
    fobj = λX. Hom[𝒞][X,C],
    fmap = λf. ⦇ setdom = Hom[𝒞][Cod 𝒞 f,C], setcod = Hom[𝒞][Dom 𝒞 f,C], setfunction = λu. (u ∘⇘𝒞⇙ f) ⦈
  ⦈"

lemma contraHom_fobj_setoid:
  assumes "Category 𝒞" "C ∈ Obj 𝒞" "X ∈ Obj 𝒞"
  shows "setoid (fobj Hom{𝒞}[-,C] X)"
by (simp add: contraHom_def, rule hom_setoid [OF assms(1) assms(3) assms(2)])

lemma contraHom_fmap_setmap:
  assumes "Category 𝒞" "C ∈ Obj 𝒞" "f ∈ Hom[𝒞][A,B]"
  shows "setmap (fmap Hom{𝒞}[-,C] f)"
apply (auto simp add: contraHom_def setmap_def)
defer apply (rule hom_setoid [OF assms(1)], rule Category.cod_obj [OF assms(1)]) using assms(3) apply (simp add: hom_def, simp add: assms)
apply (rule hom_setoid [OF assms(1)], rule Category.dom_obj [OF assms(1)]) using assms(3) apply (simp add: hom_def, simp add: assms)
apply (simp add: hom_def, auto)
apply (rule CategoryE_comp_equal [OF assms(1), of A B _ _ _ f f])
  using assms(3) apply (auto simp add: hom_def)
  apply (metis Category.dom_obj [OF assms(1)])
  apply (metis Category.cod_obj [OF assms(1)])
  apply (metis Category.cod_obj [OF assms(1)])
  apply (rule CategoryE_hom_refl [OF assms(1) assms(3)])
  apply (metis Category.comp_exist [OF assms(1)])+
done

lemma contraHom_Functor:
  assumes "Category 𝒞" "C ∈ Obj 𝒞"
  shows "Functor' Hom{𝒞}[-,C] : 𝒞 {^op} ⟶ Setoid"
apply (rule FunctorI, rule opposite_Category, rule assms, rule Setoid_Category)
apply (simp add: contraHom_def, simp add: contraHom_def)
apply (simp add: contraHom_def Setoid_def setoid_set_setoid)
proof-
  fix A B f
  assume "f ∈ Hom[𝒞 {^op}][A,B]"
  hence f: "f ∈ Hom[𝒞][B,A]" by (simp add: hom_def opposite_def)
  show "fmap Hom{𝒞}[-,C] f ∈ Hom[Setoid][fobj Hom{𝒞}[-,C] A,fobj Hom{𝒞}[-,C] B]"
    apply (auto simp add: Setoid_def hom_def)
      apply (rule contraHom_fmap_setmap [OF assms f])
      apply (simp add: contraHom_def) using f apply (simp add: hom_def)
      apply (simp add: contraHom_def) using f apply (simp add: hom_def)
    done
next
  fix X
  assume "X ∈ Obj (𝒞 {^op})"
  hence X: "X ∈ Obj 𝒞" by (simp add: opposite_def)
  hence idX: "id⇘𝒞⇙ X ∈ Hom[𝒞][X,X]" by (rule CategoryE_id_exist [OF assms(1)])
  show "fmap Hom{𝒞}[-,C] (id⇘𝒞 {^op}⇙ X) ≈⇘Setoid⇙ id⇘Setoid⇙ fobj Hom{𝒞}[-,C] X"
    apply (simp add: Setoid_def, auto)
    apply (rule contraHom_fmap_setmap [OF assms])
    apply (simp add: opposite_def, rule CategoryE_id_exist [OF assms(1) X])
    apply (rule id_setmap, rule contraHom_fobj_setoid [OF assms X])
    apply (rule setmap_eqI)
      apply (simp add: contraHom_def idsetmap_def opposite_def)
      using CategoryE_id_exist [OF assms(1) X] apply (simp add: hom_def)
      apply (simp add: contraHom_def idsetmap_def opposite_def)
      using CategoryE_id_exist [OF assms(1) X] apply (simp add: hom_def)
      apply (simp add: contraHom_def opposite_def idsetmap_def)
      apply (simp add: hom_def)
      using CategoryE_id_exist [OF assms(1) X] apply (simp add: hom_def)
      using CategoryE_hom_sym [OF assms(1) CategoryE_right_id [OF assms(1) X assms(2)]] apply (simp add: hom_def)
      using CategoryE_comp_exist [OF assms(1) X X assms(2) CategoryE_id_exist [OF assms(1) X]] apply (simp add: hom_def)
    done
next
  fix X
  assume "X ∈ Obj (𝒞 {^op})" thus "setoid (Hom[𝒞][X,C])"
    using hom_setoid [OF assms(1) _ assms(2)] by (simp add: opposite_def)
next
  fix A B Ca f g
  assume a: "A ∈ Obj (𝒞 {^op})" "B ∈ Obj (𝒞 {^op})" "Ca ∈ Obj (𝒞 {^op})"
  and b: "f ∈ carrier (Hom[𝒞 {^op}][A,B])" "g ∈ carrier (Hom[𝒞 {^op}][B,Ca])"

  have a2: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "Ca ∈ Obj 𝒞" using a by (auto simp add: opposite_def)
  have b2: "f ∈ carrier (Hom[𝒞][B,A])" "g ∈ carrier (Hom[𝒞][Ca,B])" using b by (auto simp add: opposite_def hom_def)
  show "fmap Hom{𝒞}[-,C] (g ∘⇘𝒞 {^op}⇙ f) ≈⇘Setoid⇙ fmap Hom{𝒞}[-,C] g ∘⇘Setoid⇙ fmap Hom{𝒞}[-,C] f"
    apply (simp add: Setoid_def, auto)
    apply (rule contraHom_fmap_setmap [OF assms])
    apply (simp add: opposite_def, rule CategoryE_comp_exist [OF assms(1) a2(3) a2(2) a2(1) b2(2) b2(1)])
    apply (rule setmap_comp_setmap)
    apply (rule contraHom_fmap_setmap [OF assms]) using b2 apply (simp add: hom_def)
    apply (rule contraHom_fmap_setmap [OF assms]) using b2 apply (simp add: hom_def)
    apply (simp add: contraHom_def) using b2 apply (simp add: hom_def)
    apply (rule setmap_eqI)
      apply (simp add: setmap_comp_def contraHom_def opposite_def)
      using CategoryE_comp_exist [OF assms(1) a2(3) a2(2) a2(1) b2(2) b2(1)] b2(1) apply (simp add: hom_def)
      apply (simp add: setmap_comp_def contraHom_def opposite_def)
      using CategoryE_comp_exist [OF assms(1) a2(3) a2(2) a2(1) b2(2) b2(1)] b2(2) apply (simp add: hom_def)
      apply (simp add: setmap_comp_def contraHom_def opposite_def)
      using CategoryE_comp_exist [OF assms(1), of _ _ _ "f ∘⇘𝒞⇙ g"] b2 apply (simp add: hom_def)
      using CategoryE_comp_exist [OF assms(1) a2(3) a2(2) a2(1) b2(2) b2(1)] b2 apply (simp add: hom_def)
      by (simp add: Category.arr_sym Category.assoc Category.comp_exist assms(1))
next
  fix A B f g
  assume a: "f ∈ Hom[𝒞 {^op}][A,B]" "g ∈ Hom[𝒞 {^op}][A,B]" "f ≈⇘𝒞 {^op}⇙ g"
  have a2: "f ∈ Hom[𝒞][B,A]" "g ∈ Hom[𝒞][B,A]" "f ≈⇘𝒞⇙ g"
    using a by (auto simp add: hom_def opposite_def)
  show "fmap Hom{𝒞}[-,C] f ≈⇘Setoid⇙ fmap Hom{𝒞}[-,C] g"
    apply (simp add: Setoid_def, auto)
    apply (rule contraHom_fmap_setmap [OF assms a2(1)])
    apply (rule contraHom_fmap_setmap [OF assms a2(2)])
    apply (rule setmap_eqI)
      using a2 apply (simp add: contraHom_def hom_def)
      using a2 apply (simp add: contraHom_def hom_def)
      using a2 apply (simp add: contraHom_def hom_def)
      by (smt Category.Category.select_convs(2) Category.arr_refl Category.comp_equal Category.comp_exist a2(3) assms(1))
qed

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

lemma contraHomNat_component_setmap:
  assumes "Category 𝒞" "f ∈ Hom[𝒞][A,B]" "x ∈ Obj 𝒞" "A ∈ Obj 𝒞" "B ∈ Obj 𝒞"
  shows "setmap (component HomNat{𝒞}[-,f] x)"
apply (simp add: contraHomNat_def setmap_def, auto)
apply (simp add: contraHom_def, rule CategoryE_comp_exist [OF assms(1) assms(3), of "Dom 𝒞 f"])
apply (rule Category.dom_obj [OF assms(1)]) using assms(2) apply (simp add: hom_def)
apply (rule Category.cod_obj [OF assms(1)]) using assms(2) apply (simp add: hom_def)
apply simp using assms(2) apply (simp add: hom_def)
apply (rule contraHom_fobj_setoid [OF assms(1) _ assms(3)]) using assms(2) assms(4) apply (simp add: hom_def)
apply (rule contraHom_fobj_setoid [OF assms(1) _ assms(3)]) using assms(2) assms(5) apply (simp add: hom_def)
apply (simp add: contraHom_def hom_def)
by (smt Category.comp_equal Category.comp_exist CategoryE_hom_refl CollectD assms(1) assms(2) hom_def setoid.select_convs(1))

lemma contraHomNat_Nat:
  assumes "Category 𝒞" "f ∈ Hom[𝒞][A,B]" "A ∈ Obj 𝒞" "B ∈ Obj 𝒞"
  shows "Nat' HomNat{𝒞}[-,f] : Hom{𝒞}[-,A] ⟶ Hom{𝒞}[-,B]"
apply (rule NatI)
apply (rule contraHom_Functor [OF assms(1)], rule assms(3))
apply (rule contraHom_Functor [OF assms(1)], rule assms(4))
apply (simp add: contraHomNat_def) using assms(2) apply (simp add: hom_def)
apply (simp add: contraHomNat_def) using assms(2) apply (simp add: hom_def)
apply (simp add: opposite_def hom_def Setoid_def)
using assms(2) apply (simp add: contraHomNat_component_setmap [OF assms(1) _ _ assms(3) assms(4)] hom_def)
apply (simp add: contraHomNat_def opposite_def hom_def Setoid_def setmap_def)

apply (simp add: Setoid_def opposite_def hom_def, auto)
  apply (rule setmap_comp_setmap, rule contraHomNat_component_setmap [OF assms(1) assms(2) _ assms(3) assms(4)], simp)
  apply (rule contraHom_fmap_setmap [OF assms(1)])
  using assms(2) apply (simp add: hom_def, simp add: assms)
  using assms(2) apply (simp add: hom_def)
  using assms(2) apply (simp add: contraHom_def contraHomNat_def hom_def)
  apply (rule setmap_comp_setmap, rule contraHom_fmap_setmap [OF assms(1)])
  using assms(2) apply (simp add: hom_def assms)
  using assms(2) apply (simp add: hom_def)
  apply (rule contraHomNat_component_setmap [OF assms(1) assms(2) _ assms(3) assms(4)])
  using assms(2) apply (simp add: hom_def assms)
  using assms(2) apply (simp add: contraHom_def contraHomNat_def hom_def)
  apply (rule setmap_eqI)
    apply (simp add: setmap_comp_def contraHom_def contraHomNat_def)
    using assms(2) apply (simp add: setmap_comp_def contraHom_def contraHomNat_def hom_def)
    using assms(2) apply (simp add: setmap_comp_def contraHom_def contraHomNat_def hom_def)
    apply (simp add: setmap_comp_def contraHomNat_def contraHom_def hom_def)
    by (smt Category.arr_sym Category.assoc Category.comp_exist CollectD assms(1) assms(2) hom_def setoid.select_convs(1))

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

lemma yoneda_functor:
  assumes "Category 𝒞"
  shows "Functor' (yoneda 𝒞) : 𝒞 ⟶ PSh(𝒞)"
apply (rule FunctorI, rule assms)
apply (rule Presheaf_Category [OF assms], simp add: yoneda_def)
apply (simp add: yoneda_def, simp add: yoneda_def Presheaf_def)
apply (simp add: yoneda_def FunCat_def, rule contraHom_Functor [OF assms], simp)
proof (unfold Presheaf_def)
  fix A B f
  assume f: "f ∈ Hom[𝒞][A,B]"
  have AB: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞"
    using f by (auto simp add: hom_def Category.dom_obj [OF assms] Category.cod_obj [OF assms])
  show "fmap (yoneda 𝒞) f ∈ Hom[Cat[𝒞 {^op},Setoid]][fobj (yoneda 𝒞) A,fobj (yoneda 𝒞) B]"
    using f apply (simp add: hom_def)
    apply (simp add: yoneda_def FunCat_def hom_def)
    apply (simp add: contraHomNat_Nat [OF assms f AB])
    apply (simp add: contraHom_Functor [OF assms AB(1)] contraHom_Functor [OF assms AB(2)])
    done
next
  fix X
  assume X: "X ∈ Obj 𝒞"
  show "fmap (yoneda 𝒞) (id⇘𝒞⇙ X) ≈⇘Cat[𝒞 {^op},Setoid]⇙ id⇘Cat[𝒞 {^op},Setoid]⇙ fobj (yoneda 𝒞) X"
    apply (simp add: yoneda_def FunCat_def id_Nat [OF contraHom_Functor [OF assms]])
    apply (simp add: contraHomNat_Nat [OF assms CategoryE_id_exist [OF assms X] X X])
    apply (simp add: id_Nat [OF contraHom_Functor [OF assms X]])
    apply (simp add: contraHom_Functor [OF assms X])
    apply (rule Nat_equalI)
    apply (rule contraHomNat_Nat [OF assms CategoryE_id_exist [OF assms X] X X])
    apply (simp add: id_Nat [OF contraHom_Functor [OF assms X]] Category.id_exist [OF assms X])
    apply (simp add: contraHom_def opposite_def idNat_def Setoid_def, auto)
    apply (simp add: contraHomNat_component_setmap [OF assms CategoryE_id_exist [OF assms X] _ X X])
    apply (simp add: id_setmap [OF hom_setoid [OF assms _ X]])
    apply (rule setmap_eqI)
      apply (simp add: contraHomNat_def idsetmap_def contraHom_def)
      apply (simp add: Category.id_exist [OF assms X])
      apply (simp add: contraHomNat_def idsetmap_def contraHom_def)
      apply (simp add: Category.id_exist [OF assms X])
      apply (simp add: contraHomNat_def contraHom_def idsetmap_def)
      by (simp add: Category.comp_exist Category.id_exist CategoryE_left_id X assms hom_def)
next
  fix A B C f g
  assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "C ∈ Obj 𝒞" "f ∈ Hom[𝒞][A,B]" "g ∈ Hom[𝒞][B,C]"
  hence gf: "g ∘⇘𝒞⇙ f ∈ Hom[𝒞][A,C]"
    using CategoryE_comp_exist [OF assms a] by (simp add: hom_def)

  show "fmap (yoneda 𝒞) (g ∘⇘𝒞⇙ f) ≈⇘Cat[𝒞 {^op},Setoid]⇙ fmap (yoneda 𝒞) g ∘⇘Cat[𝒞 {^op},Setoid]⇙ fmap (yoneda 𝒞) f"
    apply (simp add: yoneda_def FunCat_def)
    apply (simp add: contraHomNat_Nat [OF assms gf a(1) a(3)])
    apply rule defer
    apply (simp add: contraHom_Functor [OF assms a(1)])
    apply (simp add: contraHom_Functor [OF assms a(3)])
    apply (rule compNat_Nat)
    apply (simp add: contraHomNat_Nat [OF assms a(4) a(1) a(2)])
    apply (simp add: contraHomNat_Nat [OF assms a(5) a(2) a(3)])
    apply (rule Nat_equalI)
      apply (rule contraHomNat_Nat [OF assms gf a(1) a(3)])
      apply (rule compNat_Nat)
      apply (simp add: contraHomNat_Nat [OF assms a(4) a(1) a(2)])
      apply (simp add: contraHomNat_Nat [OF assms a(5) a(2) a(3)])
      apply (auto simp add: contraHom_def Setoid_def opposite_def)
      apply (rule contraHomNat_component_setmap [OF assms gf _ a(1) a(3)], simp)
      apply (simp add: compNat_def contraHomNat_def contraHom_def Setoid_def)
      apply (rule setmap_comp_setmap)
      using contraHomNat_component_setmap [OF assms a(5) _ a(2) a(3)] apply (simp add: contraHomNat_def contraHom_def)
      using contraHomNat_component_setmap [OF assms a(4) _ a(1) a(2)] apply (simp add: contraHomNat_def contraHom_def)
      using a apply (simp add: contraHomNat_def contraHom_def hom_def)
      apply (rule setmap_eqI)
        apply (simp add: compNat_def contraHomNat_def contraHom_def Setoid_def setmap_comp_def)
        using a gf apply (simp add: hom_def)
        apply (simp add: compNat_def contraHomNat_def contraHom_def Setoid_def setmap_comp_def)
        using a gf apply (simp add: hom_def)
        apply (simp add: compNat_def contraHomNat_def contraHom_def Setoid_def setmap_comp_def)
        by (smt Category.assoc Category.comp_exist a(4) a(5) assms hom_def mem_Collect_eq setoid.select_convs(1) setoid.select_convs(2))
next
  fix A B f g
  assume a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "f ∈ Hom[𝒞][A,B]" "g ∈ Hom[𝒞][A,B]" "f ≈⇘𝒞⇙ g"
  show "fmap (yoneda 𝒞) f ≈⇘Cat[𝒞 {^op},Setoid]⇙ fmap (yoneda 𝒞) g"
    apply (simp add: yoneda_def FunCat_def)
    apply (simp add: contraHomNat_Nat [OF assms a(3) a(1) a(2)] contraHomNat_Nat [OF assms a(4) a(1) a(2)])
    apply (simp add: contraHom_Functor [OF assms a(1)] contraHom_Functor [OF assms a(2)])
    apply (rule Nat_equalI)
    apply (simp add: contraHomNat_Nat [OF assms a(3) a(1) a(2)], simp add: contraHomNat_Nat [OF assms a(4) a(1) a(2)])
    apply (simp add: contraHom_def Setoid_def opposite_def, auto)
      apply (rule contraHomNat_component_setmap [OF assms a(3) _ a(1) a(2)], simp)
      apply (rule contraHomNat_component_setmap [OF assms a(4) _ a(1) a(2)], simp)
      apply (rule setmap_eqI)
        apply (simp add: contraHomNat_def) using a apply (simp add: hom_def)
        apply (simp add: contraHomNat_def) using a apply (simp add: hom_def)
        apply (simp add: contraHomNat_def contraHom_def)
        by (smt Category.comp_exist CategoryE_comp_equal CategoryE_hom_refl a(1) a(2) a(3) a(4) a(5) assms hom_def mem_Collect_eq setoid.select_convs(1) setoid.select_convs(2))
qed

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

lemma obj_to_nat_build_component_setmap:
  assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "C ∈ Obj 𝒞" "x ∈ fobj F C" "X ∈ Obj (𝒞 {^op})"
  shows "setmap (component (obj_to_nat_build 𝒞 F C x) X)"
proof (simp add: obj_to_nat_build_def)
  have F_Functor: "Functor' F : 𝒞 {^op} ⟶ Setoid"
    using assms(2) by (simp add: Presheaf_def FunCat_def)
  have Xop: "X ∈ Obj (𝒞 {^op})" by (rule assms)
  hence X: "X ∈ Obj 𝒞" by (simp add: opposite_def)

  show "setmap ⦇setdom = fobj (fobj (yoneda 𝒞) C) X, setcod = fobj F X, setfunction = λu. setfunction (fmap F u) x⦈"
    proof (simp add: setmap_def, auto)
      fix xa
      assume "xa ∈ carrier (fobj (fobj (yoneda 𝒞) C) X)"
      hence xa: "xa ∈ Hom[𝒞][X,C]" by (simp add: yoneda_def contraHom_def)
      have Fxa: "fmap F xa ∈ Hom[Setoid][fobj F C,fobj F X]"
        apply (rule FunctorE_fmap [OF F_Functor])
        using xa apply (simp add: hom_def opposite_def) done
      show "setfunction (fmap F xa) x ∈ carrier (fobj F X)"
        using Fxa assms(4) by (simp add: hom_def Setoid_def setmap_def, auto)
    next
      show "setoid (fobj (fobj (yoneda 𝒞) C) X)"
        by (simp add: yoneda_def contraHom_def, rule hom_setoid [OF assms(1) X assms(3)])
    next
      show "setoid (fobj F X)"
        using FunctorE_fobj [OF F_Functor Xop] by (simp add: Setoid_def)
    next
      fix xa y
      assume "equal (fobj (fobj (yoneda 𝒞) C) X) xa y"
      hence a: "xa ∈ Hom[𝒞][X,C]" "y ∈ Hom[𝒞][X,C]" "xa ≈⇘𝒞⇙ y"
        by (auto simp add: yoneda_def contraHom_def hom_def)
      hence aop: "xa ∈ Hom[𝒞 {^op}][C,X]" "y ∈ Hom[𝒞 {^op}][C,X]" "xa ≈⇘𝒞 {^op}⇙ y"
        by (auto simp add: opposite_def hom_def)
      have h: "fmap F xa ≈⇘Setoid⇙ fmap F y"
        using FunctorE_preserver_equal [OF F_Functor _ Xop aop] by (simp add: assms opposite_def)
      have h2: "setdom (fmap F xa) = fobj F C" "setcod (fmap F xa) = fobj F X" "setdom (fmap F y) = fobj F C"
        using FunctorE_fmap [OF F_Functor aop(1)] FunctorE_fmap [OF F_Functor aop(2)]
        by (auto simp add: hom_def Setoid_def)
      show "equal (fobj F X) (setfunction (fmap F xa) x) (setfunction (fmap F y) x)"
        using h apply (simp add: Setoid_def setmap_eq_def)
        using assms(4) by (fastforce simp add: h2)
    qed
qed


lemma obj_to_nat_build_Nat:
  assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "C ∈ Obj 𝒞" "x ∈ fobj F C"
  shows "Nat' (obj_to_nat_build 𝒞 F C x) : (fobj (yoneda 𝒞) C) ⟶ F"
apply (rule NatI)
apply (simp add: yoneda_def, rule contraHom_Functor [OF assms(1) assms(3)])
using assms(2) apply (simp add: Presheaf_def FunCat_def)
apply (simp add: obj_to_nat_build_def, simp add: obj_to_nat_build_def)
proof-
  fix X
  assume Xop: "X ∈ Obj (𝒞 {^op})"
  show "component (obj_to_nat_build 𝒞 F C x) X ∈ Hom[Setoid][fobj (fobj (yoneda 𝒞) C) X,fobj F X]"
    apply (simp add: opposite_def obj_to_nat_build_def hom_def Setoid_def)
    using obj_to_nat_build_component_setmap [OF assms Xop] by (simp add: obj_to_nat_build_def)
next
  have F_Functor: "Functor' F : 𝒞 {^op} ⟶ Setoid"
    using assms(2) by (simp add: Presheaf_def FunCat_def)

  fix A B f
  assume aop: "A ∈ Obj (𝒞 {^op})" "B ∈ Obj (𝒞 {^op})" "f ∈ carrier (Hom[𝒞 {^op}][A,B])"
  hence a: "A ∈ Obj 𝒞" "B ∈ Obj 𝒞" "f ∈ carrier (Hom[𝒞][B,A])" by (auto simp add: hom_def opposite_def)
  show "component (obj_to_nat_build 𝒞 F C x) B ∘⇘Setoid⇙ fmap (fobj (yoneda 𝒞) C) f ≈⇘Setoid⇙
        fmap F f ∘⇘Setoid⇙ component (obj_to_nat_build 𝒞 F C x) A"
    apply (simp add: Setoid_def, auto)
    apply (rule setmap_comp_setmap, simp add: obj_to_nat_build_def)
    using obj_to_nat_build_component_setmap [OF assms] apply (simp add: obj_to_nat_build_def aop)
    apply (simp add: yoneda_def, rule contraHom_fmap_setmap [OF assms(1) assms(3) a(3)])
    apply (simp add: yoneda_def obj_to_nat_build_def contraHom_def) using a(3) apply (simp add: hom_def)
    apply (rule setmap_comp_setmap)
    using FunctorE_fmap [OF F_Functor aop(3)] apply (simp add: hom_def Setoid_def)
    apply (simp add: obj_to_nat_build_def) using obj_to_nat_build_component_setmap [OF assms] apply (simp add: obj_to_nat_build_def aop)
    apply (simp add: obj_to_nat_build_def)
    using FunctorE_fmap [OF F_Functor aop(3)] apply (simp add: hom_def Setoid_def)
    apply (rule setmap_eqI)
      apply (simp add: setmap_comp_def yoneda_def obj_to_nat_build_def contraHom_def) using a(3) apply (simp add: hom_def)
      apply (simp add: setmap_comp_def yoneda_def obj_to_nat_build_def contraHom_def)
      using FunctorE_fmap [OF F_Functor aop(3)] apply (simp add: hom_def Setoid_def)
      apply (simp add: setmap_comp_def obj_to_nat_build_def yoneda_def contraHom_def)
      proof-
        fix xa
        assume "xa ∈ Hom[𝒞][Cod 𝒞 f,C]"
        hence b: "xa ∈ Hom[𝒞][A,C]" using a by (simp add: hom_def)
        hence bop: "xa ∈ Hom[𝒞 {^op}][C,A]" using a by (simp add: hom_def opposite_def)
        have h: "fmap F (xa ∘⇘𝒞⇙ f) ≈⇘Setoid⇙ fmap F f ∘⇘Setoid⇙ fmap F xa"
          using FunctorE_preserver_comp [OF F_Functor bop aop(3)] by (simp add: opposite_def)
        have Fxaf: "fmap F (xa ∘⇘𝒞⇙ f) ∈ Hom[Setoid][fobj F C, fobj F B]"
          using FunctorE_fmap [OF F_Functor, of "xa ∘⇘𝒞⇙ f" C B] apply (rule)
          using CategoryE_comp_exist [OF assms(1) a(2) a(1) assms(3) a(3) b] by (simp add: hom_def opposite_def, simp)
        have p: "setdom (fmap F (xa ∘⇘𝒞⇙ f)) = fobj F C" "setcod (fmap F (xa ∘⇘𝒞⇙ f)) = fobj F B"
          using Fxaf by (auto simp add: hom_def Setoid_def)
        have q1: "equal (fobj F B) (setfunction (fmap F (xa ∘⇘𝒞⇙ f)) x) (setfunction (fmap F f ∘⇘Setoid⇙ fmap F xa) x)"
          using h apply (simp add: Setoid_def setmap_eq_def)
          using assms(4) apply (auto simp add: p)
          done
        have q2: "setfunction (fmap F f ∘⇘Setoid⇙ fmap F xa) x = setfunction (fmap F f) (setfunction (fmap F xa) x)"
          by (simp add: Setoid_def setmap_comp_def)
        show "equal (fobj F B) (setfunction (fmap F (xa ∘⇘𝒞⇙ f)) x) (setfunction (fmap F f) (setfunction (fmap F xa) x))"
          using q1 by (simp add: q2)
      qed
qed

definition obj_to_nat where
  "obj_to_nat 𝒞 F C ≡ ⦇
    setdom = fobj F C,
    setcod = Hom[PSh(𝒞)][fobj (yoneda 𝒞) C, F],
    setfunction = obj_to_nat_build 𝒞 F C
  ⦈"

lemma obj_to_nat_setmap:
  assumes "Category 𝒞" "F ∈ Obj (PSh 𝒞)" "C ∈ Obj 𝒞"
  shows "setmap (obj_to_nat 𝒞 F C)"
apply (auto simp add: setmap_def)
apply (simp add: obj_to_nat_def hom_def Presheaf_def FunCat_def)
  apply (simp add: obj_to_nat_build_Nat [OF assms] yoneda_def contraHom_Functor [OF assms(1) assms(3)])
  using assms(2) apply (simp add: Presheaf_def FunCat_def)
apply (simp add: obj_to_nat_def)
  using FunctorE_fobj [of F "𝒞 {^op}" Setoid C] assms(2) assms(3) apply (simp add: Presheaf_def FunCat_def opposite_def Setoid_def)
apply (simp add: obj_to_nat_def)
  apply (rule hom_setoid, simp add: Presheaf_def FunCat_Category [OF opposite_Category [OF assms(1)] Setoid_Category])
  apply (simp add: Presheaf_def FunCat_def yoneda_def contraHom_Functor [OF assms(1) assms(3)], rule assms(2))
proof (simp add: obj_to_nat_def)
  have F_Functor: "Functor' F : 𝒞 {^op} ⟶ Setoid"
    using assms(2) by (simp add: Presheaf_def FunCat_def)

  fix x y
  assume a: "equal (fobj F C) x y"
  have 1: "setoid (fobj F C)"
    using FunctorE_fobj [OF F_Functor, of C] by (simp add: opposite_def assms(3) Setoid_def)
  have 2: "x ∈ fobj F C" "y ∈ fobj F C"
    using equiv_type [OF setoid.equal_equiv [OF 1]] a by auto
  have 3: "⋀X. X ∈ Obj 𝒞 ⟹ component (obj_to_nat_build 𝒞 F C x) X ∈ Hom[Setoid][fobj (fobj (yoneda 𝒞) C) X, fobj F X]"
    using NatE_component [OF obj_to_nat_build_Nat [OF assms 2(1)]] by (simp add: yoneda_def contraHom_def opposite_def)

  show "equal (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) (obj_to_nat_build 𝒞 F C x) (obj_to_nat_build 𝒞 F C y)"
    apply (simp add: hom_def Presheaf_def FunCat_def)
    apply (simp add: obj_to_nat_build_Nat [OF assms 2(1)] obj_to_nat_build_Nat [OF assms 2(2)])
    apply (simp add: yoneda_def contraHom_Functor [OF assms(1) assms(3)] F_Functor)
    apply (rule Nat_equalI)
      apply (rule obj_to_nat_build_Nat [OF assms 2(1)], rule obj_to_nat_build_Nat [OF assms 2(2)])
      apply (simp add: yoneda_def contraHom_def opposite_def)
      apply (simp add: Setoid_def, auto)
      using NatE_component [OF obj_to_nat_build_Nat [OF assms 2(1)]] apply (simp add: yoneda_def contraHom_def opposite_def hom_def Setoid_def)
      using NatE_component [OF obj_to_nat_build_Nat [OF assms 2(2)]] apply (simp add: yoneda_def contraHom_def opposite_def hom_def Setoid_def)
      apply (rule setmap_eqI)
        apply (simp add: obj_to_nat_build_def, simp add: obj_to_nat_build_def)
        apply (simp add: obj_to_nat_build_def yoneda_def contraHom_def)
        proof-
          fix X xa
          assume b: "X ∈ Obj 𝒞" "xa ∈ Hom[𝒞][X,C]"
          have 4: "fmap F xa ∈ Hom[Setoid][fobj F C, fobj F X]"
            apply (rule FunctorE_fmap [OF F_Functor]) using b(2) by (simp add: hom_def opposite_def)
          show "equal (fobj F X) (setfunction (fmap F xa) x) (setfunction (fmap F xa) y)"
            using setmap.preserve_equal [of "fmap F xa"] 4 by (simp add: hom_def Setoid_def a)
        qed
qed

definition nat_to_obj where
  "nat_to_obj 𝒞 F C ≡ ⦇
    setdom = Hom[PSh(𝒞)][fobj (yoneda 𝒞) C, F],
    setcod = fobj F C,
    setfunction = λα. setfunction (component α C) (Id 𝒞 C)
  ⦈"

lemma nat_to_obj_setmap:
  assumes "Category 𝒞" "F ∈ Obj (PSh 𝒞)" "C ∈ Obj 𝒞"
  shows "setmap (nat_to_obj 𝒞 F C)"
proof (auto simp add: setmap_def, simp add: nat_to_obj_def)
  fix x
  assume "x ∈ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]"
  hence 1: "Nat' x : fobj (yoneda 𝒞) C ⟶ F"
    by (simp add: hom_def Presheaf_def FunCat_def)
  have 2: "component x C ∈ Hom[Setoid][Hom[𝒞][C,C], fobj F C]"
    using NatE_component [OF 1, of C] by (simp add: yoneda_def contraHom_def opposite_def assms(3))
  have 3: "setmap (component x C)" "id⇘𝒞⇙ C ∈ setdom (component x C)" "setcod (component x C) = fobj F C"
    using 2 apply (simp add: hom_def Setoid_def)
    using 2 apply (simp add: hom_def Setoid_def Category.id_exist [OF assms(1) assms(3)])
    using 2 apply (simp add: hom_def Setoid_def)
    done
  show "setfunction (component x C) (id⇘𝒞⇙ C) ∈ fobj F C"
    using 3(1) apply (simp add: setmap_def)
    using 3(2) 3(3) apply simp
    done
next
  show "setoid (setdom (nat_to_obj 𝒞 F C))"
    apply (simp add: nat_to_obj_def, rule hom_setoid)
    apply (simp add: Presheaf_def, rule FunCat_Category [OF opposite_Category [OF assms(1)] Setoid_Category])
    apply (simp add: yoneda_def Presheaf_def FunCat_def, rule contraHom_Functor [OF assms(1) assms(3)], rule assms(2))
    done
next
  show "setoid (setcod (nat_to_obj 𝒞 F C))"
    apply (simp add: nat_to_obj_def)
    using assms(2) apply (simp add: Presheaf_def FunCat_def)
    using FunctorE_fobj [of F "𝒞 {^op}" Setoid C] assms(3) by (simp add: opposite_def Setoid_def)
next
  fix x y
  assume 1: "equal (setdom (nat_to_obj 𝒞 F C)) x y"
  have 2: "x ≈⇘Cat[𝒞 {^op},Setoid]⇙ y" "Nat' x : fobj (yoneda 𝒞) C ⟶ F" "Nat' y : fobj (yoneda 𝒞) C ⟶ F"
    using 1 apply (simp add: nat_to_obj_def hom_def Presheaf_def)
    using 1 apply (simp add: nat_to_obj_def hom_def Presheaf_def FunCat_def)
    using 1 apply (simp add: nat_to_obj_def hom_def Presheaf_def FunCat_def)
    done
  have "Nat_equal x y"
    using 2(1) by (simp add: FunCat_def)
  hence 3: "component x C ≈⇘Setoid⇙ component y C"
    apply (simp add: Nat_equal_def)
    using 2(2) apply (simp add: yoneda_def contraHom_def opposite_def, simp add: assms(3))
    done
  have "⋀xa. xa ∈ setdom (component x C) ⟹ equal (setcod (component x C)) (setfunction (component x C) xa) (setfunction (component y C) xa)"
    using 3 by (simp add: Setoid_def setmap_eq_def, auto)
  hence 4: "⋀xa. xa ∈ Hom[𝒞][C,C] ⟹ equal (fobj F C) (setfunction (component x C) xa) (setfunction (component y C) xa)"
    using NatE_component [OF 2(2)] apply (simp add: yoneda_def contraHom_def opposite_def)
    using assms(3) apply (simp add: hom_def Setoid_def)
    done
  show "equal (setcod (nat_to_obj 𝒞 F C)) (setfunction (nat_to_obj 𝒞 F C) x) (setfunction (nat_to_obj 𝒞 F C) y)"
    by (simp add: nat_to_obj_def, rule 4, rule CategoryE_id_exist [OF assms(1) assms(3)])
qed

definition IsoWith where
  "IsoWith A B f g ≡ (equal (Hom[Setoid][A,A]) (g ∘[setmap] f) (id⇘Setoid⇙ A))
                   ∧ (equal (Hom[Setoid][B,B]) (f ∘[setmap] g) (id⇘Setoid⇙ B))"

lemma YonedaLemma:
  assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "C ∈ Obj 𝒞"
  shows "IsoWith (Hom[PSh(𝒞)][fobj (yoneda 𝒞) C, F]) (fobj F C) (nat_to_obj 𝒞 F C) (obj_to_nat 𝒞 F C)"
proof (unfold IsoWith_def, auto)
  have F_Functor: "Functor' F : 𝒞 {^op} ⟶ Setoid"
    using assms(2) by (simp add: Presheaf_def FunCat_def)

  have q1: "setmap_eq ((obj_to_nat 𝒞 F C) ∘[setmap] (nat_to_obj 𝒞 F C)) (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])"
    apply (rule setmap_eqI)
    apply (simp add: setmap_comp_def nat_to_obj_def obj_to_nat_def Setoid_def idsetmap_def)
    apply (simp add: setmap_comp_def nat_to_obj_def obj_to_nat_def Setoid_def idsetmap_def)
    proof-
      fix x
      assume "x ∈ setdom (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C)"
      hence x: "x ∈ Hom[PSh(𝒞)][fobj (yoneda 𝒞) C, F]"
        by (simp add: setmap_comp_def nat_to_obj_def)
      hence x_Nat: "Nat' x : fobj (yoneda 𝒞) C ⟶ F" by (simp add: hom_def Presheaf_def FunCat_def)

      have h1: "setcod (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) = Hom[PSh(𝒞)][fobj (yoneda 𝒞) C, F]"
        by (simp add: setmap_comp_def obj_to_nat_def)
      have h2: "⋀f g. equal (Hom[PSh(𝒞)][fobj (yoneda 𝒞) C, F]) f g = ((f ≈⇘PSh 𝒞⇙ g) ∧ (f ∈ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) ∧ (g ∈ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]))"
        by (simp add: hom_def, auto)
      show "equal (setcod (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C))
          (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)
          (setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x)"
        proof (simp add: h1 h2, auto)
          have ha1: "⋀f g. (f ≈⇘PSh 𝒞⇙ g) = (Nat_equal f g
            ∧ (Nat' f : domFunctor f ⟶ codFunctor f) ∧ (Nat' g : domFunctor f ⟶ codFunctor f)
            ∧ (Functor' (domFunctor f) : 𝒞 {^op} ⟶ Setoid) ∧ (Functor' (codFunctor f) : 𝒞 {^op} ⟶ Setoid))"
            by (simp add: Presheaf_def FunCat_def)

          have onno_Nat: "Nat' setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x : fobj (yoneda 𝒞) C ⟶ F"
            apply (simp add: setmap_comp_def obj_to_nat_def)
            apply (rule obj_to_nat_build_Nat [OF assms])
            using nat_to_obj_setmap [OF assms] apply (simp add: setmap_def nat_to_obj_def x) done
          have idx_Nat: "Nat' setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x : fobj (yoneda 𝒞) C ⟶ F"
            apply (simp add: Setoid_def idsetmap_def)
            using x by (simp add: hom_def Presheaf_def FunCat_def)
          have 1: "domCat (fobj (yoneda 𝒞) C) = (𝒞 {^op})" "codCat (fobj (yoneda 𝒞) C) = Setoid"
            by (auto simp add: yoneda_def contraHom_def)
          have 2: "setfunction (nat_to_obj 𝒞 F C) x ∈ carrier (fobj F C)"
            using nat_to_obj_setmap [OF assms] by (simp add: setmap_def nat_to_obj_def x)

          {
            show "setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x ≈⇘PSh 𝒞⇙ setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x"
              proof (simp add: ha1, auto)
                have 3: "⋀X. X ∈ Obj 𝒞 ⟹ setdom (component x X) = Hom[𝒞][X,C] ∧ fobj F X = setcod (component x X) ∧ setmap (component x X)"
                  using NatE_component [OF x_Nat] by (simp add: yoneda_def contraHom_def opposite_def hom_def Setoid_def)
  
                show "Nat_equal
                  (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)
                  (setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x)"
                  apply (rule Nat_equalI, rule onno_Nat, rule idx_Nat)
                  apply (simp add: 1 opposite_def Setoid_def, auto)
                  apply (simp add: setmap_comp_def obj_to_nat_def)
                  apply (rule obj_to_nat_build_component_setmap [OF assms 2], simp add: opposite_def)
                  apply (simp add: idsetmap_def)
                  using NatE_component [OF x_Nat] apply (simp add: yoneda_def contraHom_def opposite_def hom_def Setoid_def)
                  apply (rule setmap_eqI)
                    apply (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def idsetmap_def yoneda_def contraHom_def 3)
                    apply (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def idsetmap_def yoneda_def contraHom_def 3)
                    apply (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def idsetmap_def yoneda_def contraHom_def nat_to_obj_def)
                    proof-
                      fix X xa
                      assume a: "X ∈ Obj 𝒞" "xa ∈ Hom[𝒞][X,C]"
                      hence aop: "X ∈ Obj (𝒞 {^op})" "xa ∈ Hom[𝒞 {^op}][C,X]" by (auto simp add: hom_def opposite_def)
  
                      have 4: "setdom (fmap F xa ∘[setmap] component x C) = Hom[𝒞][C,C]" "setcod (fmap F xa ∘[setmap] component x C) = fobj F X"
                        apply (simp add: setmap_comp_def)
                        using NatE_component [OF x_Nat, of C] apply (simp add: yoneda_def contraHom_def opposite_def assms hom_def Setoid_def)
                        apply (simp add: setmap_comp_def)
                        using FunctorE_fmap [OF F_Functor aop(2)] apply (simp add: hom_def Setoid_def) done
                      have 5: "id⇘𝒞⇙ C ∈ Hom[𝒞][C,C]" by (rule CategoryE_id_exist [OF assms(1) assms(3)])
  
                      have 51: "fmap F xa ∘⇘Setoid⇙ component x C ≈⇘Setoid⇙ component x X ∘⇘Setoid⇙ fmap (fobj (yoneda 𝒞) C) xa"
                        using NatE_naturality [OF x_Nat, of xa C X]
                        apply (simp add: yoneda_def contraHom_def aop(2))
                        apply (simp add: CategoryE_hom_sym [OF Setoid_Category]) done
                      hence 6: "⋀k. k ∈ Hom[𝒞][C,C] ⟹ equal (fobj F X) (setfunction (fmap F xa ∘⇘Setoid⇙ component x C) k) (setfunction (component x X ∘⇘Setoid⇙ fmap (fobj (yoneda 𝒞) C) xa) k)"
                        by (simp add: Setoid_def setmap_eq_def, metis 4)
                      have 7: "equal (fobj F X) (setfunction (component x X) xa) (setfunction (component x X) (id⇘𝒞⇙ C ∘⇘𝒞⇙ xa))"
                        proof-
                          have h1: "xa ≈⇘𝒞⇙ id⇘𝒞⇙ C ∘⇘𝒞⇙ xa" by (rule CategoryE_hom_sym [OF assms(1)], rule CategoryE_left_id [OF assms(1) a(1) assms(3) a(2)])
                          have h2: "setmap (component x X)" using 3 [OF a(1)] by simp
                          have h3: "setdom (component x X) = Hom[𝒞][X,C]" using 3 [OF a(1)] by simp
                          have h4: "setcod (component x X) = fobj F X" using 3 [OF a(1)] by simp
                          show ?thesis
                            using setmap.preserve_equal [OF h2] apply (simp add: h3 h4 hom_def)
                            using h1 a(2) CategoryE_id_exist [OF assms(1) assms(3)]
                            by (simp add: Category.comp_exist assms(1) hom_def)
                        qed
  
                      show "equal (fobj F X) (setfunction (fmap F xa) (setfunction (component x C) (id⇘𝒞⇙ C))) (setfunction (component x X) xa)"
                        using 6 [OF 5] apply (simp add: Setoid_def setmap_comp_def yoneda_def contraHom_def)
                        using 7
                        by (metis (mono_tags, lifting) "4"(2) Category.Category.select_convs(2) Category.Category.select_convs(6) Setoid_def 51setmap_cod_sym setmap_cod_trans setoid.select_convs(2))
                    qed
              next
                show "Nat (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)" by (simp add: onno_Nat)
              next
                show "Nat (setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x)" by (simp add: Setoid_def idsetmap_def x_Nat)
              next
                show "domFunctor (setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x) = domFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)"
                  apply (simp add: Setoid_def idsetmap_def setmap_comp_def obj_to_nat_def obj_to_nat_build_def) using x by (simp add: hom_def Presheaf_def FunCat_def)
              next
                show "codFunctor (setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x) = codFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)"
                  apply (simp add: Setoid_def idsetmap_def setmap_comp_def obj_to_nat_def obj_to_nat_build_def) using x by (simp add: hom_def Presheaf_def FunCat_def)
              next
                show "Functor (domFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x))"
                  by (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def yoneda_def contraHom_Functor [OF assms(1) assms(3)])
              next
                show "domCat (domFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)) = (𝒞 {^op})"
                  by (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def yoneda_def contraHom_Functor [OF assms(1) assms(3)])
              next
                show "codCat (domFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)) = Setoid"
                  by (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def yoneda_def contraHom_Functor [OF assms(1) assms(3)])
              next
                show "Functor (codFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x))"
                  by (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def F_Functor)
              next
                show "domCat (codFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)) = (𝒞 {^op})"
                  by (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def F_Functor)
              next
                show "codCat (codFunctor (setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x)) = Setoid"
                  by (simp add: setmap_comp_def obj_to_nat_def obj_to_nat_build_def F_Functor)
              qed
          }
          {
            show "setfunction (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) x ∈ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]"
              apply (simp add: hom_def Presheaf_def FunCat_def onno_Nat)
              by (simp add: yoneda_def contraHom_Functor [OF assms(1) assms(3)] F_Functor)
          }
          {
            have q: "⋀x. Nat' x : (fobj (yoneda 𝒞) C) ⟶ F ⟹ x ∈ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]"
              by (simp add: hom_def Presheaf_def FunCat_def yoneda_def contraHom_Functor [OF assms(1) assms(3)] F_Functor)
            show "setfunction (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x ∈ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]" 
              by (simp add: q idx_Nat)
          }
        qed
    qed

  have q2: "setmap_eq ((nat_to_obj 𝒞 F C) ∘[setmap] (obj_to_nat 𝒞 F C)) (id⇘Setoid⇙ fobj F C)"
    apply (rule setmap_eqI)
    apply (simp add: setmap_comp_def obj_to_nat_def Setoid_def idsetmap_def)
    apply (simp add: setmap_comp_def Setoid_def idsetmap_def nat_to_obj_def)
    apply (simp add: setmap_comp_def obj_to_nat_def nat_to_obj_def obj_to_nat_build_def Setoid_def idsetmap_def)
    proof-
      fix x
      assume x: "x ∈ carrier (fobj F C)"
      have 1: "fmap F (id⇘𝒞⇙ C) ≈⇘Setoid⇙ id⇘Setoid⇙ fobj F C"
        using FunctorE_preserver_id [OF F_Functor, of C] by (simp add: opposite_def assms(3))
      have 2: "equal (fobj F C) (setfunction (fmap F (id⇘𝒞⇙ C)) x) (setfunction (idsetmap (fobj F C)) x)"
        using 1 apply (simp add: Setoid_def setmap_eq_def)
        by (simp add: idsetmap_def, metis x)
      show "equal (fobj F C) (setfunction (fmap F (id⇘𝒞⇙ C)) x) x"
        using 2 by (simp add: idsetmap_def)
    qed

  {
    show "equal (Hom[Setoid][Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F],Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]])
            ((obj_to_nat 𝒞 F C) ∘[setmap] (nat_to_obj 𝒞 F C))
            (id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])"
      proof-
        have 1: "⋀a b f g. (equal (Hom[Setoid][a,b]) f g) =
          (equal (Arr Setoid) f g ∧ f ∈ carrier (Arr Setoid) ∧ g ∈ carrier (Arr Setoid) ∧ Dom Setoid f = a ∧ Cod Setoid f = b ∧ Dom Setoid g = a ∧ Cod Setoid g = b)"
          by (simp add: hom_def)
        show ?thesis
          apply (simp add: 1, auto)
          defer defer
          apply (simp add: Setoid_def, rule id_setmap, rule hom_setoid, rule Presheaf_Category [OF assms(1)])
          apply (simp add: yoneda_def Presheaf_def FunCat_def contraHom_Functor [OF assms(1) assms(3)])
          apply (simp add: assms(2))
          apply (simp add: Setoid_def setmap_comp_def nat_to_obj_def)
          apply (simp add: Setoid_def setmap_comp_def obj_to_nat_def)
          apply (simp add: Setoid_def setmap_comp_def nat_to_obj_def idsetmap_def)
          apply (simp add: Setoid_def setmap_comp_def nat_to_obj_def idsetmap_def)
          proof-
            show "(obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) ≈⇘Setoid⇙ id⇘Setoid⇙ Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]"
              proof (auto simp add: Setoid_def)
                show "setmap (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C)"
                  apply (simp add: setmap_comp_def nat_to_obj_def obj_to_nat_def)
                  proof (simp add: setmap_def, auto)
                    fix x
                    assume x: "x ∈ carrier (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])"
                    hence x_Nat: "Nat' x : fobj (yoneda 𝒞) C ⟶ F" by (simp add: hom_def Presheaf_def FunCat_def)
                    have 1: "component x C ∈ Hom[Setoid][fobj (fobj (yoneda 𝒞) C) C, fobj F C]"
                      using NatE_component [OF x_Nat, of C] by (simp add: yoneda_def contraHom_def opposite_def assms(3))
                    have "⋀xa. xa ∈ (fobj (fobj (yoneda 𝒞) C) C) ⟹ setfunction (component x C) xa ∈ fobj F C"
                      using 1 by (simp add: hom_def Setoid_def setmap_def, auto)
                    hence 2: "⋀xa. xa ∈ Hom[𝒞][C,C] ⟹ setfunction (component x C) xa ∈ fobj F C"
                      by (simp add: yoneda_def contraHom_def)
                    have 3: "setfunction (component x C) (id⇘𝒞⇙ C) ∈ fobj F C"
                      by (rule 2, rule CategoryE_id_exist [OF assms(1) assms(3)])
  
                    show "obj_to_nat_build 𝒞 F C (setfunction (component x C) (id⇘𝒞⇙ C)) ∈ carrier (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])"
                      apply (simp add: hom_def Presheaf_def FunCat_def obj_to_nat_build_Nat [OF assms 3])
                      apply (simp add: yoneda_def contraHom_Functor [OF assms(1) assms(3)] F_Functor)
                      done
              next
                show "setoid (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])"
                  apply (rule hom_setoid, rule Presheaf_Category [OF assms(1)])
                  apply (simp add: Presheaf_def FunCat_def yoneda_def contraHom_Functor [OF assms(1) assms(3)], rule assms(2))
                  done
              next
                fix x y
                assume a: "equal (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]) x y"
                from a have x: "x ∈ carrier (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])" by (simp add: hom_def)
                from a have y: "y ∈ carrier (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])" by (simp add: hom_def)
                from x have x_Nat: "Nat' x : fobj (yoneda 𝒞) C ⟶ F" by (simp add: hom_def Presheaf_def FunCat_def)
                from y have y_Nat: "Nat' y : fobj (yoneda 𝒞) C ⟶ F" by (simp add: hom_def Presheaf_def FunCat_def)
                have x1: "component x C ∈ Hom[Setoid][fobj (fobj (yoneda 𝒞) C) C, fobj F C]"
                  using NatE_component [OF x_Nat, of C] by (simp add: yoneda_def contraHom_def opposite_def assms(3))
                have "⋀xa. xa ∈ (fobj (fobj (yoneda 𝒞) C) C) ⟹ setfunction (component x C) xa ∈ fobj F C"
                  using x1 by (simp add: hom_def Setoid_def setmap_def, auto)
                hence x2: "⋀xa. xa ∈ Hom[𝒞][C,C] ⟹ setfunction (component x C) xa ∈ fobj F C"
                  by (simp add: yoneda_def contraHom_def)
                have x3: "setfunction (component x C) (id⇘𝒞⇙ C) ∈ fobj F C"
                  by (rule x2, rule CategoryE_id_exist [OF assms(1) assms(3)])
                have y1: "component y C ∈ Hom[Setoid][fobj (fobj (yoneda 𝒞) C) C, fobj F C]"
                  using NatE_component [OF y_Nat, of C] by (simp add: yoneda_def contraHom_def opposite_def assms(3))
                have "⋀xa. xa ∈ (fobj (fobj (yoneda 𝒞) C) C) ⟹ setfunction (component y C) xa ∈ fobj F C"
                  using y1 by (simp add: hom_def Setoid_def setmap_def, auto)
                hence y2: "⋀xa. xa ∈ Hom[𝒞][C,C] ⟹ setfunction (component y C) xa ∈ fobj F C"
                  by (simp add: yoneda_def contraHom_def)
                have y3: "setfunction (component y C) (id⇘𝒞⇙ C) ∈ fobj F C"
                  by (rule y2, rule CategoryE_id_exist [OF assms(1) assms(3)])
  
                show "equal (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F])
                  (obj_to_nat_build 𝒞 F C (setfunction (component x C) (id⇘𝒞⇙ C)))
                  (obj_to_nat_build 𝒞 F C (setfunction (component y C) (id⇘𝒞⇙ C)))"
                  apply (simp add: hom_def Presheaf_def FunCat_def)
                  apply (simp add: obj_to_nat_build_Nat [OF assms x3] obj_to_nat_build_Nat [OF assms y3])
                  apply (simp add: F_Functor yoneda_def contraHom_Functor [OF assms(1) assms(3)])
                  apply (rule Nat_equalI)
                    apply (simp add: obj_to_nat_build_Nat [OF assms x3], simp add: obj_to_nat_build_Nat [OF assms y3])
                    apply (simp add: yoneda_def contraHom_def opposite_def)
                    apply (auto simp add: Setoid_def)
                      using obj_to_nat_build_component_setmap [OF assms x3] apply (simp add: opposite_def)
                      using obj_to_nat_build_component_setmap [OF assms y3] apply (simp add: opposite_def)
                      apply (rule setmap_eqI)
                        apply (simp add: obj_to_nat_build_def)
                        apply (simp add: obj_to_nat_build_def)
                        apply (simp add: obj_to_nat_build_def yoneda_def)
                        proof-
                          fix X xa
                          assume b: "X ∈ Obj 𝒞" "xa ∈ fobj Hom{𝒞}[-,C] X"
                          hence xa: "xa ∈ Hom[𝒞][X,C]" by (simp add: contraHom_def)
                          have "Nat_equal x y"
                            using a by (simp add: hom_def Presheaf_def FunCat_def)
                          hence "component x C ≈⇘Setoid⇙ component y C"
                            apply (simp add: Nat_equal_def)
                            using x_Nat apply (simp add: yoneda_def contraHom_def opposite_def)
                            using assms(3) by (metis (mono_tags, lifting))
                          hence "⋀xa. xa ∈ setdom (component x C) ⟹ equal (setcod (component x C)) (setfunction (component x C) xa) (setfunction (component y C) xa)"
                            by (simp add: Setoid_def setmap_eq_def, auto)
                          hence q1: "⋀xa. xa ∈ Hom[𝒞][C,C] ⟹ equal (fobj F C) (setfunction (component x C) xa) (setfunction (component y C) xa)"
                            using x1 by (simp add: hom_def Setoid_def yoneda_def contraHom_def)
                          have q2: "equal (fobj F C) (setfunction (component x C) (id⇘𝒞⇙ C)) (setfunction (component y C) (id⇘𝒞⇙ C))"
                            by (rule q1, rule CategoryE_id_exist [OF assms(1) assms(3)])
  
                          have Fxa: "fmap F xa ∈ Hom[Setoid][fobj F C, fobj F X]"
                            using FunctorE_fmap [OF F_Functor, of xa] xa by (simp add: hom_def opposite_def)
                          hence Fxa_setmap: "setmap (fmap F xa)"
                            by (simp add: hom_def Setoid_def)
  
                          show "equal (fobj F X)
                            (setfunction (fmap F xa) (setfunction (component x C) (id⇘𝒞⇙ C)))
                            (setfunction (fmap F xa) (setfunction (component y C) (id⇘𝒞⇙ C)))"
                            using setmap.preserve_equal [OF Fxa_setmap, of "setfunction (component x C) (id⇘𝒞⇙ C)" "setfunction (component y C) (id⇘𝒞⇙ C)"]
                            using Fxa by (simp add: hom_def Setoid_def q2)
                        qed
                qed
            next
              show "setmap (idsetmap (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]))"
                apply (rule id_setmap, rule hom_setoid [OF Presheaf_Category [OF assms(1)] _ assms(2)])
                apply (simp add: Presheaf_def FunCat_def yoneda_def contraHom_Functor [OF assms(1) assms(3)])
                done
            next
              show "setmap_eq (obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) (idsetmap (Hom[PSh 𝒞][fobj (yoneda 𝒞) C,F]))"
                using q1 by (simp add: Setoid_def)
            qed
        next
          show "(obj_to_nat 𝒞 F C ∘[setmap] nat_to_obj 𝒞 F C) ∈ Arr Setoid"
            apply (simp add: Setoid_def, rule setmap_comp_setmap)
            apply (rule obj_to_nat_setmap [OF assms], rule nat_to_obj_setmap [OF assms])
            apply (simp add: nat_to_obj_def obj_to_nat_def)
            done
        qed
    qed
  }
  {
    have 1: "setmap (nat_to_obj 𝒞 F C ∘[setmap] obj_to_nat 𝒞 F C)"
      apply (rule setmap_comp_setmap [OF nat_to_obj_setmap [OF assms] obj_to_nat_setmap [OF assms]])
      apply (simp add: obj_to_nat_def nat_to_obj_def) done
    have 2: "setmap (idsetmap (fobj F C))"
      apply (rule id_setmap) using FunctorE_fobj [OF F_Functor, of C] assms(3) by (simp add: opposite_def Setoid_def)
    show "equal (Hom[Setoid][fobj F C,fobj F C]) (nat_to_obj 𝒞 F C ∘[setmap] obj_to_nat 𝒞 F C) (id⇘Setoid⇙ fobj F C)"
      apply (simp add: hom_def Setoid_def, simp add: 1 2, auto)
      using q2 apply (simp add: Setoid_def)
      apply (simp add: setmap_comp_def obj_to_nat_def)
      apply (simp add: setmap_comp_def nat_to_obj_def)
      apply (simp add: idsetmap_def, simp add: idsetmap_def)
      done
  }
qed