(*
Author: Alexander Katovsky
*)

section "The Category of Sets"

theory SetCat
imports Functors Universe
begin

notation Elem (infixl ‹|∈|› 70)
notation HOLZF.subset (infixl ‹|⊆|› 71)
notation CartProd (infixl ‹|×|› 75)

definition 
  ZFfun :: "ZF → ZF → (ZF → ZF) → ZF" where
  "ZFfun d r f ≡ Opair (Opair d r) (Lambda d f)"

definition
  ZFfunDom :: "ZF → ZF" (‹|dom|_› [72] 72) where
  "ZFfunDom f ≡ Fst (Fst f)"

definition
  ZFfunCod :: "ZF → ZF" (‹|cod|_› [72] 72) where
  "ZFfunCod f ≡ Snd (Fst f)"

definition
  ZFfunApp :: "ZF → ZF → ZF" (infixl ‹|@|› 73) where
  "ZFfunApp f x ≡ app (Snd f) x"

definition 
  ZFfunComp :: "ZF → ZF → ZF" (infixl ‹|o|› 72) where
  "ZFfunComp f g ≡ ZFfun ( |dom| f) ( |cod| g) (λx. g |@| (f |@| x))"

definition 
  isZFfun :: "ZF → bool" where
  "isZFfun drf ≡ let f = Snd drf in
                 isOpair drf ∧ isOpair (Fst drf) ∧ isFun f ∧ (f |⊆| (Domain f) |×| (Range f))
                 ∧ (Domain f = |dom| drf) ∧ (Range f |⊆| |cod| drf)"

lemma isZFfunE[elim]: "[isZFfun f ;
  [isOpair f ; isOpair (Fst f) ; isFun (Snd f) ;
  ((Snd f) |⊆| (Domain (Snd f)) |×| (Range (Snd f))) ;
  (Domain (Snd f) = |dom| f) ∧ (Range (Snd f) |⊆| |cod| f)] ==> R] ==> R"
  by (auto simp add: isZFfun_def Let_def)

definition  
  SET' :: "(ZF, ZF) Category" where
  "SET' ≡ (
      Category.Obj = {x . True} ,
      Category.Mor = {f . isZFfun f} ,
      Category.Dom = ZFfunDom ,
      Category.Cod = ZFfunCod ,
      Category.Id = λx. ZFfun x x (λx . x) ,
      Category.Comp = ZFfunComp
  )"

definition "SET ≡ MakeCat SET'"

lemma ZFfunDom: "|dom| (ZFfun A B f) = A"
by (auto simp add: ZFfun_def ZFfunDom_def Fst)

lemma ZFfunCod: "|cod| (ZFfun A B f) = B"
by (auto simp add: ZFfun_def ZFfunCod_def Snd Fst)

lemma SETfun: 
  assumes "∀ x . x |∈| A ⟶ (f x) |∈| B"
  shows   "isZFfun (ZFfun A B f)"
proof(auto simp add: isZFfun_def ZFfun_def isOpair Fst Snd 
    ZFfunCod_def ZFfunDom_def isFun_Lambda domain_Lambda Let_def)
  {
    fix x
    have "x |∈| Range (Lambda A f) ==> x |∈| B"
      apply(insert isFun_Lambda[of A f])
      apply (drule fun_range_witness[of "Lambda A f" x], simp)
      by (auto simp add: domain_Lambda Lambda_app assms)
  }
  thus "subset (Range (Lambda A f)) B"
    by (auto simp add: subset_def)
  {
    fix x
    have "x |∈| (Lambda A f) ==> x |∈| A |×| Range (Lambda A f)" 
      by(auto simp add: CartProd Lambda_def Repl Range)
  }
  thus "(Lambda A f) |⊆| (A |×| Range (Lambda A f))"
    by (auto simp add: HOLZF.subset_def)
qed

lemma ZFCartProd: 
  assumes "x |∈| A |×| B"
  shows   "Fst x |∈| A ∧ Snd x |∈| B ∧ isOpair x"
proof-
  from CartProd obtain a b 
    where "a |∈| A" 
    and   "b |∈| B" 
    and   "x = Opair a b" using assms by auto
  thus ?thesis using assms by (auto simp add: Fst Snd isOpair_def)
qed

lemma ZFfunDomainOpair:
  assumes "isFun f"
  and     "x |∈| Domain f"
  shows   "Opair x (app f x) |∈| f"
proof-
  have "∃! y . Opair x y |∈| f" using assms by (auto simp add: unique_fun_value)
  thus "Opair x (app f x) |∈| f" by (auto simp add: app_def intro: theI')
qed
  
lemma ZFFunToLambda: 
  assumes 1: "isFun f"
  and     2: "f |⊆| (Domain f) |×| (Range f)"
  shows   "f = Lambda (Domain f) (λx. app f x)"
proof(subst Ext, rule allI, rule iffI)
  {
    fix x assume a: "x |∈| f" show "x |∈| Lambda (Domain f) (λx. app f x)" 
    proof(simp add: Lambda_def Repl, rule exI[of _ "(Fst x)"], rule conjI)
      have b:"isOpair x ∧ Fst x |∈| Domain f" using 2 a by (auto simp add: subset_def ZFCartProd)
      thus "Fst x |∈| Domain f" ..
      hence "Opair (Fst x) (app f (Fst x)) |∈| f" using 1 by (simp add: ZFfunDomainOpair)
      moreover have "Opair (Fst x) (Snd x) |∈| f" using a 2 by (auto simp add: FstSnd subset_def b)
      ultimately have "Snd x = (app f (Fst x))" using 1 by (auto simp add: isFun_def)
      hence "Opair (Fst x) (app f (Fst x)) = Opair (Fst x) (Snd x)" by simp
      also have "... = x"  using b by (simp add: FstSnd)
      finally show "x = Opair (Fst x) (app f (Fst x))" ..
    qed
  }
  moreover 
  {
    fix x assume a: "x |∈| Lambda (Domain f) (λx. app f x)" show "x |∈| f"
      proof-
        from Lambda_def obtain a where "a |∈| Domain f ∧ x = Opair a (app f a)" 
          using a by (auto simp add: Repl)
        thus ?thesis using a 1 by (auto simp add: ZFfunDomainOpair)
      qed
  }
qed   

lemma ZFfunApp: 
  assumes "x |∈| A"
  shows   "(ZFfun A B f) |@| x = f x"
proof-
  have "(ZFfun A B f) |@| x = app (Lambda A f) x" by (simp add: ZFfun_def ZFfunApp_def Snd)
  also have "... = f x" using assms by (simp add: Lambda_app)
  finally show ?thesis .
qed

lemma ZFfun: 
  assumes "isZFfun f" 
  shows   "f = ZFfun ( |dom| f) ( |cod| f) (λx. f |@| x)"
proof(auto simp add: ZFfun_def)
  have "isOpair f ∧ isOpair (Fst f)" using assms by (simp add: isZFfun_def[of f] Let_def)
  hence "f = Opair (Opair (Fst (Fst f)) (Snd (Fst f))) (Snd f)" by (simp add: FstSnd)
  hence "f = Opair (Opair ( |dom| f) ( |cod| f)) (Snd f)" using assms by (simp add: ZFfunDom_def ZFfunCod_def)
  moreover have "Snd f = Lambda ( |dom| f) (λx . f |@| x)" 
  proof-
    have "|dom| f = Domain (Snd f)" using assms by (simp add: isZFfun_def[of f] Let_def)
    moreover have "isFun (Snd f)" using assms by (simp add: isZFfun_def[of f] Let_def)
    moreover have "(λx . f |@| x) = (λx . app (Snd f) x)"  by(simp add: ZFfunApp_def)
    moreover have "(Snd f) |⊆| (Domain (Snd f)) |×| (Range (Snd f))" using assms
      by (auto simp add: isZFfun_def[of f] Let_def)
    ultimately show ?thesis apply simp by(rule ZFFunToLambda[of "Snd f"])
  qed
  ultimately show "f = Opair (Opair ( |dom| f) ( |cod| f)) (Lambda ( |dom| f) (λx . f |@| x))" by simp
qed

lemma ZFfun_ext: 
  assumes "∀ x . x |∈| A ⟶ f x = g x" 
  shows   "(ZFfun A B f) = (ZFfun A B g)"
proof-
  have "Lambda A f = Lambda A g" using assms by (auto simp add: Lambda_ext)
  thus ?thesis by (simp add: ZFfun_def)
qed

lemma ZFfunExt:
  assumes "|dom| f = |dom| g" and "|cod| f = |cod| g" and funf: "isZFfun f" and fung: "isZFfun g"
  and "∧ x . x |∈| ( |dom| f) ==> f |@| x = g |@| x"
  shows "f = g"
proof-
  have 1: "f = ZFfun ( |dom| f) ( |cod| f) (λx. f |@| x)" using funf by (rule ZFfun)
  have "g = ZFfun ( |dom| g) ( |cod| g) (λx. g |@| x)" using fung by (rule ZFfun)
  hence 2: "g = ZFfun ( |dom| f) ( |cod| f) (λx. g |@| x)" using assms by simp
  have "ZFfun ( |dom| f) ( |cod| f) (λx. f |@| x) = ZFfun ( |dom| f) ( |cod| f) (λx. g |@| x)" 
    using assms by (simp add: ZFfun_ext)
  thus ?thesis using 1 2 by simp
qed  

lemma ZFfunDomAppCod: 
  assumes "isZFfun f"
  and     "x |∈| |dom|f"
  shows   "f |@| x |∈| |cod|f"
proof(simp add: ZFfunApp_def)
  have "app (Snd f) x |∈| Range (Snd f)" using assms by (auto simp add: fun_value_in_range )
  thus "app (Snd f) x |∈| |cod|f" using assms by (auto simp add: HOLZF.subset_def)
qed

lemma ZFfunComp: 
  assumes "∀ x . x |∈| A ⟶ f x |∈| B"
  shows   "(ZFfun A B f) |o| (ZFfun B C g) = ZFfun A C (g o f)"
proof (simp add: ZFfunComp_def ZFfunDom ZFfunCod)
  {
    fix x assume a: "x |∈| A"
    have "ZFfun B C g |@| (ZFfun A B f |@| x) = (g o f) x" 
      proof-
        have "(ZFfun A B f |@| x) = f x" using a by (simp add: ZFfunApp)
        hence "ZFfun B C g |@| (ZFfun A B f |@| x) = g (f x)" using assms a by (simp add: ZFfunApp)
        thus ?thesis by simp
      qed
  }
  thus "ZFfun A C (λx. ZFfun B C g |@| (ZFfun A B f |@| x)) = ZFfun A C (g ∘ f)"
    by (simp add: ZFfun_ext)
qed

lemma ZFfunCompApp: 
  assumes a:"isZFfun f" and b:"isZFfun g" and c:"|dom|g = |cod|f"
  shows "f |o| g = ZFfun ( |dom| f) ( |cod| g) (λ x . g |@| (f |@| x))"
proof-
  have 1: "f = ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x)" using a by (rule ZFfun)
  have 2: "g = ZFfun ( |dom| g) ( |cod| g) (λ x . g |@| x)" using b by (rule ZFfun)
  have 3: "∀ x . x |∈| |dom|f ⟶ (λx. f |@| x) x |∈| |cod|f" using a by (simp add: ZFfunDomAppCod)
  hence 4: "∀ x . x |∈| |dom|f ⟶ (λx. g |@| (f |@| x)) x |∈| |cod|g" 
    using a b c by (simp add: ZFfunDomAppCod)
  have "f |o| g = ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x) |o|
    ZFfun ( |cod| f) ( |cod| g) (λ x . g |@| x)" using 1 2 c by simp
  hence "f |o| g = ZFfun ( |dom| f) ( |cod| g) (λ x . g |@| (f |@| x))"
    using 3 by (simp add: ZFfunComp comp_def)
  thus ?thesis using 4 by (simp add: SETfun)
qed  

lemma ZFfunCompAppZFfun: 
  assumes "isZFfun f" and "isZFfun g" and "|dom|g = |cod|f"
  shows   "isZFfun (f |o| g)"
proof-
  have "f |o| g = ZFfun ( |dom| f) ( |cod| g) (λ x . g |@| (f |@| x))" using assms
    by (simp add: ZFfunCompApp)
  moreover have "∀ x . x |∈| |dom|f ⟶ ((λ x . g |@| (f |@| x)) x) |∈| |cod|g" using assms
    by (simp add: ZFfunDomAppCod)
  ultimately show ?thesis by (simp add: SETfun)
qed

lemma ZFfunCompAssoc:
  assumes a: "isZFfun f" and b:"isZFfun h" and c:"|cod|g = |dom|h" 
  and d:"isZFfun g" and e:"|cod|f = |dom|g"
  shows "f |o| g |o| h = f |o| (g |o| h)"
proof-
  have 1: "f = ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x)" using a by (rule ZFfun)
  have 2: "g = ZFfun ( |dom| g) ( |cod| g) (λ x . g |@| x)" using d by (rule ZFfun)
  have 3: "h = ZFfun ( |dom| h) ( |cod| h) (λ x . h |@| x)" using b by (rule ZFfun)
  have 4: "∀ x . x |∈| |dom|f ⟶ (λx. f |@| x) x |∈| |cod|f" using a by (simp add: ZFfunDomAppCod)
  have "(f |o| g) |o| h = ZFfun ( |dom| f) ( |cod| h) (λ x . h |@| (g |@| (f |@| x)))"
  proof-
    have 5: "∀ x . x |∈| |dom|f ⟶ (λx. g |@| (f |@| x)) x |∈| |cod|g" 
      using 4 e d by (simp add: ZFfunDomAppCod)
    have "(f |o| g) |o| h = (ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x) |o|
      ZFfun ( |cod| f) ( |cod| g) (λ x . g |@| x)) |o|
      ZFfun ( |cod| g) ( |cod| h) (λ x . h |@| x)" 
      using 1 2 3 c e by (simp)
    thus ?thesis using 4 5 by (simp add: ZFfunComp comp_def)
  qed
  moreover have "f |o| (g |o| h) = ZFfun ( |dom| f) ( |cod| h) (λ x . h |@| (g |@| (f |@| x)))"
  proof-
    have 5: "∀ x . x |∈| |dom|g ⟶ (λx. g |@| x) x |∈| |cod|g" using d by (simp add: ZFfunDomAppCod)
    have "f |o| (g |o| h) = ZFfun ( |dom| f) ( |dom| g) (λ x . f |@| x) |o|
      (ZFfun ( |dom| g) ( |cod| g) (λ x . g |@| x) |o|
      ZFfun ( |cod| g) ( |cod| h) (λ x . h |@| x))" 
      using 1 2 3 c e by (simp)
    thus ?thesis using 4 e 5 by (simp add: ZFfunComp comp_def)
  qed
  ultimately show ?thesis by simp
qed
  
lemma ZFfunCompAppDomCod: 
  assumes "isZFfun f" and "isZFfun g" and "|dom|g = |cod|f"
  shows   "|dom| (f |o| g) = |dom| f ∧ |cod| (f |o| g) = |cod| g"
proof-
  have "f |o| g = ZFfun ( |dom| f) ( |cod| g) (λ x . g |@| (f |@| x))" using assms
    by (simp add: ZFfunCompApp)
  thus ?thesis by (simp add: ZFfunDom ZFfunCod)
qed

lemma ZFfunIdLeft: 
  assumes a: "isZFfun f" shows "(ZFfun ( |dom|f) ( |dom|f) (λx. x)) |o| f = f"
proof-
  let ?g = "(ZFfun ( |dom|f) ( |dom|f) (λx. x))"
  have "ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x) = ?g |o| f" using a 
    by (simp add: ZFfun_ext ZFfunApp ZFfunCompApp SETfun ZFfunCod ZFfunDom)
  moreover have "f = ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x)" using a by (rule ZFfun)
  ultimately show ?thesis by simp
qed

lemma ZFfunIdRight:
  assumes a: "isZFfun f" shows "f |o| (ZFfun ( |cod|f) ( |cod|f) (λx. x)) = f"
proof-
  let ?g = "(ZFfun ( |cod|f) ( |cod|f) (λx. x))"
  have 1: "∀ x . x |∈| |dom|f ⟶ (λx. f |@| x) x |∈| |cod|f" using a by (simp add: ZFfunDomAppCod)
  have "ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x) = f |o| ?g" using a 1
    by (simp add: ZFfun_ext ZFfunApp ZFfunCompApp SETfun ZFfunCod ZFfunDom)
  moreover have "f = ZFfun ( |dom| f) ( |cod| f) (λ x . f |@| x)" using a by (rule ZFfun)
  ultimately show ?thesis by simp
qed

lemma SETCategory: "Category(SET)"
proof-
  have "Category_axioms SET'"  
    by (auto simp add: Category_axioms_def SET'_def ZFfunCompAppDomCod 
      ZFfunCompAppZFfun ZFfunCompAssoc ZFfunIdLeft ZFfunIdRight ZFfunDom ZFfunCod SETfun MapsTo_def CompDefined_def)
  thus ?thesis by (auto simp add: SET_def MakeCat)
qed

lemma SETobj: "X ∈ Obj (SET)"
by (simp add: SET_def SET'_def MakeCat_def)

lemma SETcod: "isZFfun (ZFfun A B f) ==> cod ZFfun A B f = B"
by(simp add: SET_def MakeCat_def SET'_def ZFfunCod)

lemma SETmor: "(isZFfun f) = (f ∈ mor)"
by(simp add: SET_def MakeCat_def SET'_def)

lemma SETdom: "isZFfun (ZFfun A B f) ==> dom ZFfun A B f = A"
by(simp add: SET_def MakeCat_def SET'_def ZFfunDom)

lemma SETId: assumes "x |∈| X" shows "(Id SET X) |@| x = x"
proof-
  have "X ∈ Obj SET" by (simp add: SET_def SET'_def MakeCat_def)
  hence "isZFfun(Id SET X)" by (simp add: SETCategory Category.CatIdInMor SETmor)
  moreover have "(Id SET X) = ZFfun X X (λx. x)" using assms by (simp add: SET_def SET'_def MakeCat_def)
  ultimately show ?thesis using assms by (simp add: ZFfunApp)
qed

lemma SETCompE[elim]: "[f ≈> g ; [isZFfun f ; isZFfun g ; |cod| f = |dom| g] ==> R] ==> R"
by (auto simp add: SET_def SET'_def MakeCat_def)

lemma SETmapsTo: "f maps X to Y ==> isZFfun f ∧ |dom| f = X ∧ |cod| f = Y"
by(auto simp add: MapsTo_def SET_def SET'_def MakeCat_def)

lemma SETComp: assumes "f ≈> g" shows "f ;; g = f |o| g"
proof-
  have a: "f ≈> _SET' g" using assms by (simp add: SET_def)
  have "f ;; g = f ;; _SET' g" by (simp add: SET_def)
  also have "... = f ;;_' g" using a  by (simp  add: MakeCatComp2)
  finally show ?thesis by (simp add: SET'_def)
qed

lemma SETCompAt:
  assumes "f ≈> g" and "x |∈| |dom| f" shows "(f ;; g) |@| x = g |@| (f |@| x)"
proof-
  have "f ;; g = f |o| g" using assms by (simp add: SETComp)
  also have "... = ZFfun ( |dom| f) ( |cod| g) (λ x . g |@| (f |@| x))" using assms by (auto simp add: ZFfunCompApp)
  finally show ?thesis using assms by (simp add: ZFfunApp)
qed

lemma SETZFfun: 
  assumes "f maps X to Y" shows "f = ZFfun X Y (λx . f |@| x)"
proof-
  have "isZFfun f"  using assms by (auto simp add: SETmor)
  hence "f = ZFfun ( |dom| f) ( |cod| f) (λx. f |@| x)" by (simp add: ZFfun)
  moreover have "|dom| f = X" and "|cod| f = Y" using assms by (auto simp add: SET_def SET'_def MakeCat_def)
  ultimately show ?thesis by (simp)
qed  

lemma SETfunDomAppCod:
  assumes "f maps X to Y" and "x |∈| X"
  shows "f |@| x |∈| Y"
proof-
  have 1: "isZFfun f" and "|dom| f = X" and 2: "|cod| f = Y" using assms by (auto simp add: SETmapsTo)
  hence "x |∈| |dom| f" using assms by simp
  hence "f |@| x |∈| |cod| f" using 1 by (simp add: ZFfunDomAppCod)  
  thus ?thesis using 2 by simp
qed

(*Locally Small Category has an injective map from the morphisms to ZF*)
record ('o,'m) LSCategory = "('o,'m) Category" +
  mor2ZF :: "'m → ZF" (‹m2zı_› [70] 70)

definition 
  ZF2mor (‹z2mı_› [70] 70) where
  "ZF2mor C f ≡ THE m . m ∈ mor ∧ m2z m = f"

definition
  "HOMCollection C X Y ≡ {m2z f | f . f maps X to Y}"

definition
  HomSet (‹Homı _ _› [65, 65] 65)  where
  "HomSet C X Y ≡ implode (HOMCollection C X Y)"

locale LSCategory = Category +
  assumes mor2ZFInj: "[x ∈ mor ; y ∈ mor ; m2z x = m2z y] ==> x = y"
  and HOMSetIsSet: "[X ∈ obj ; Y ∈ obj] ==> HOMCollection C X Y ∈ range explode"
  and m2zExt: "mor2ZF C ∈ extensional (Mor C)"

lemma [elim]: "[LSCategory C ;
  [Category C ; [x ∈ mor ; y ∈ mor ; m2z x = m2z y] ==> x = y;
  [X ∈ obj ; Y ∈ obj] ==> HOMCollection C X Y ∈ range explode] ==> R] ==> R"
by(simp add: LSCategory_def LSCategory_axioms_def)

definition
  HomFtorMap :: "('o,'m,'a) LSCategory_scheme → 'o → 'm → ZF" (‹Homı[_,_]› [65,65] 65) where
  "HomFtorMap C X g ≡ ZFfun (Hom X (dom g)) (Hom X (cod g)) (λ f . m2z ((z2m f) ;; g))"

definition 
  HomFtor' :: "('o,'m,'a) LSCategory_scheme → 'o →
      ('o,ZF,'m,ZF,(mor2ZF :: 'm → ZF, … :: 'a),unit) Functor" (‹HomPı[_,←-]› [65] 65) where
  "HomFtor' C X ≡ (
        CatDom = C,
        CatCod = SET ,
        MapM = λ g . Hom[X,g]
  )"

definition HomFtor (‹Homı[_,←-]› [65] 65) where "HomFtor C X ≡ MakeFtor (HomFtor' C X)"

lemma [simp]: "LSCategory C ==> Category C"
  by (simp add: LSCategory_def)

lemma (in LSCategory) m2zz2m: 
  assumes "f maps X to Y" shows "(m2z f) |∈| (Hom X Y)"
proof-
  have "X ∈ Obj C" and "Y ∈ Obj C" using assms by (simp add: MapsToObj)+
  hence "HOMCollection C X Y ∈ range explode" using assms by (simp add: HOMSetIsSet)
  moreover have "(m2z f) ∈ HOMCollection C X Y" using assms by (auto simp add: HOMCollection_def)
  ultimately have "(m2z f) |∈| implode (HOMCollection C X Y)" by (simp add: Elem_implode)
  thus ?thesis by (simp add: HomSet_def) 
qed

lemma (in LSCategory) m2zz2mInv: 
  assumes "f ∈ mor"
  shows "z2m (m2z f) = f"
proof-
  have 1: "f ∈ mor ∧ m2z f = m2z f" using assms by simp
  moreover have "∃! m . m ∈ mor ∧ m2z m = (m2z f)" 
  proof(rule ex_ex1I)
    show "∃ m . m ∈ mor ∧ m2z m = (m2z f)" 
      by(rule exI[of _ f], insert 1, simp)
    {
      fix m y assume "m ∈ mor ∧ m2z m = (m2z f)" and "y ∈ mor ∧ m2z y = (m2z f)"
      thus "m = y" by(simp add: mor2ZFInj)
    }
  qed
  ultimately show ?thesis by(simp add: ZF2mor_def the1_equality)
qed

lemma (in LSCategory) z2mm2z: 
  assumes "X ∈ obj" and "Y ∈ obj" and "f |∈| (Hom X Y)"
  shows "z2m f maps X to Y ∧ m2z (z2m f) = f"
proof-
  have 1: "∃ m . m maps X to Y ∧ m2z m = f"
  proof-
    have "HOMCollection C X Y ∈ range explode" using assms by (simp add: HOMSetIsSet)
    moreover have "f |∈| implode (HOMCollection C X Y)" using assms(3) by (simp add: HomSet_def)
    ultimately have "f ∈ HOMCollection C X Y" by (simp add: HOLZF.Elem_implode)
    thus ?thesis by (auto simp add: HOMCollection_def)
  qed
  have 2: "∃! m . m ∈ mor ∧ m2z m = f" 
  proof(rule ex_ex1I)
    show "∃ m . m ∈ mor ∧ m2z m = f"
    proof-
      from 1 obtain m where "m ∈ mor ∧ m2z m = f" by auto
      thus ?thesis by auto
    qed
    {
      fix m y assume "m ∈ mor ∧ m2z m = f" and "y ∈ mor ∧ m2z y = f"
      thus "m = y" by(simp add: mor2ZFInj)
    }
  qed
  thus ?thesis
  proof-
    from 1 obtain a where 3: "a maps X to Y ∧ m2z a = f" by auto
    have 4: "a ∈ mor" using 3 by auto
    have "z2m f = a" 
      apply (auto simp add: 3 ZF2mor_def[of _ f])
      apply (rule the1_equality[of "λ m . m ∈ mor ∧ m2z m = f" a])
      apply (auto simp add: 2 3 4)
      done
    thus ?thesis by (simp add: 3)
  qed
qed

lemma  HomFtorMapLemma1: 
  assumes a: "LSCategory C" and b: "X ∈ obj" and c: "f ∈ mor" and d: "x |∈| (Hom X (dom f))"
  shows "(m2z ((z2m x) ;; f)) |∈| (Hom X (cod f))"
proof-
  have 1: "dom f ∈ obj" and 2: "cod f ∈ obj" using a c by (simp add: Category.Simps)+
  have "z2m x maps X to (dom f)"  using a b d 1 by (auto simp add: LSCategory.z2mm2z)
  hence "(z2m x) ;; f maps X to (cod f)" using a c by (auto intro: Category.Ccompt)
  hence "(m2z ((z2m x) ;; f)) |∈| (Hom X (cod f))" using a b d 2 
    by (auto simp add: LSCategory.m2zz2m)
  thus ?thesis using c by (simp add: Category.Simps)
qed

lemma HomFtorInMor':
  assumes "LSCategory C" and "X ∈ obj" and "f ∈ mor"
  shows "Hom[X,f] ∈ mor_'" 
proof(simp add: HomFtorMap_def)
  {
    fix x assume "x |∈| (Hom X dom f)" 
    hence "m2z ((z2m x) ;; f) |∈| (Hom X cod f)" using assms by (blast intro: HomFtorMapLemma1)
  }
  hence "∀ x . x |∈| (Hom X dom f) ⟶ (m2z ((z2m x) ;; f)) |∈| (Hom X cod f)" by (simp)
  hence "isZFfun (ZFfun (Hom X dom f) (Hom X cod f) (λ x . m2z ((z2m x) ;; f)))"
    by (simp add: SETfun)
  thus "ZFfun (Hom X dom f) (Hom X cod f) (λ x . m2z ((z2m x) ;; f)) ∈ mor_'"
    by (simp add: SET'_def)
qed

lemma HomFtorMor':
  assumes "LSCategory C" and "X ∈ obj" and "f ∈ mor"
  shows   "Hom[X,f] maps_' Hom X (dom f) to Hom X (cod f)"  
proof-
  have "Hom[X,f] ∈ mor_'" using assms by (simp add: HomFtorInMor')
  moreover have "dom_' (Hom[X,f]) = Hom X (dom f)"
    by(simp add: HomFtorMap_def SET'_def ZFfunDom)
  moreover have "cod_' (Hom[X,f]) = Hom X (cod f)"
    by(simp add: HomFtorMap_def SET'_def ZFfunCod)
  ultimately show ?thesis by (auto simp add: SET_def)
qed

lemma HomFtorMapsTo:
  "[LSCategory C ; X ∈ obj ; f ∈ mor ] ==> Hom[X,f] maps Hom X (dom f) to Hom X (cod f)"
by (simp add: HomFtorMor' SET_def MakeCatMapsTo)

lemma HomFtorMor:
  assumes "LSCategory C" and "X ∈ obj" and "f ∈ mor" 
  shows "Hom[X,f] ∈ Mor SET" and "dom (Hom[X,f]) = Hom X (dom f)" 
  and "cod (Hom[X,f]) = Hom X (cod f)"
proof-
  have "Hom[X,f] maps Hom X (dom f) to Hom X (cod f)" using assms by (simp add: HomFtorMapsTo)
  thus "Hom[X,f] ∈ Mor SET" and "dom (Hom[X,f]) = Hom X (dom f)" and "cod (Hom[X,f]) = Hom X (cod f)"
    by auto
qed

lemma HomFtorCompDef':
  assumes "LSCategory C" and "X ∈ obj" and "f ≈> g" 
  shows   "(Hom[X,f]) ≈>_' (Hom[X,g])"
proof(rule CompDefinedI)
  have a: "f ∈ mor" and b: "g ∈ mor" using assms(3) by auto 
  thus "Hom[X,f] ∈ mor_'" and "Hom[X,g] ∈ mor_'" using assms by (simp add:HomFtorInMor')+
  have "(Hom[X,f]) maps_' Hom X dom f to Hom X cod f"
    and "(Hom[X,g]) maps_' Hom X dom g to Hom X cod g" using assms a b by (simp add: HomFtorMor')+
  hence "cod_' (Hom[X,f]) = Hom X (cod f)" 
    and "dom_' (Hom[X,g]) = Hom X (dom g)" by auto
  moreover have "(cod f) = (dom g)" using assms(3) by auto
  ultimately show "cod_' (Hom[X,f]) = dom_' (Hom[X,g])" by simp
qed

lemma HomFtorDist': 
  assumes a: "LSCategory C" and b: "X ∈ obj" and c: "f ≈> g"
  shows   "(Hom[X,f]) ;;_' (Hom[X,g]) = Hom[X,f ;; g]"
proof-
  let ?A = "(Hom X dom f)"
  let ?B = "(Hom X dom g)"
  let ?C = "(Hom X cod g)"
  let ?f = "(λh. m2z ((z2m h) ;; f))"
  let ?g = "(λf. m2z ((z2m f) ;; g))"
  have 1: "cod f = dom g" using c by auto
  have 2: "dom (f ;; g) = dom f" and 3: "cod (f ;; g) = cod g" using assms 
    by (auto simp add: Category.MapsToMorDomCod)
  have "(Hom[X,f]) ;;_' (Hom[X,g]) = (ZFfun ?A (Hom X cod f) ?f) |o| (ZFfun ?B ?C ?g)" 
    by (simp add: HomFtorMap_def SET'_def)
  also have "... = (ZFfun ?A ?B ?f) |o| (ZFfun ?B ?C ?g)" using 1 by simp
  also have "... = ZFfun ?A ?C (?g o ?f)" 
  proof(rule ZFfunComp, rule allI, rule impI)
    {
      fix h assume aa: "h |∈| ?A" show "?f h |∈| ?B"
      proof-
        have "f ∈ mor" using assms by auto
        hence "?f h |∈| (Hom X cod f)" using assms aa by (simp add: HomFtorMapLemma1)
        thus ?thesis using 1 by simp
      qed
    }
  qed
  also have "... = ZFfun ?A ?C (λh. m2z ((z2m h) ;; (f ;; g)))"
  proof(rule ZFfun_ext, rule allI, rule impI, simp add: comp_def)
    {
      fix h assume aa: "h |∈| ?A" 
      show "m2z ((z2m (m2z((z2m h) ;; f))) ;; g) = m2z ((z2m h) ;; (f ;; g))"
      proof-
        have bb: "(z2m h) ≈> f" 
        proof(rule CompDefinedI)
          show "f ∈ mor" using c by auto
          hence "dom f ∈ obj" using a by (simp add: Category.Cdom)
          hence "(z2m h) maps X to dom f" using assms aa by (simp add: LSCategory.z2mm2z)
          thus "(z2m h) ∈ mor" and "cod (z2m h) = dom f" by auto
        qed
        hence "(z2m h) ;; f ∈ mor" using a by (simp add: Category.MapsToMorDomCod)
        hence "z2m (m2z ((z2m h) ;; f)) = (z2m h) ;; f" using a by (simp add: LSCategory.m2zz2mInv)
        hence "m2z ((z2m (m2z((z2m h) ;; f))) ;; g) = m2z (((z2m h) ;; f) ;; g)" by simp
        also have "... = m2z ((z2m h) ;; (f ;; g))" using bb c a by (simp add: Category.Cassoc)
        finally show ?thesis .
      qed
    }
  qed
  also have "... = ZFfun (Hom X dom (f ;; g)) (Hom X cod (f ;; g)) (λh. m2z ((z2m h) ;; (f ;; g)))"
    using 2 3 by simp
  also have "... = Hom[X,f ;; g]" by (simp add:  HomFtorMap_def)
  finally show ?thesis by (auto simp add: SET_def)
qed

lemma HomFtorDist:
  assumes "LSCategory C" and "X ∈ obj" and "f ≈> g"
  shows   "(Hom[X,f]) ;; (Hom[X,g]) = Hom[X,f ;; g]"
proof-
  have "(Hom[X,f]) ;;_' (Hom[X,g]) = Hom[X,f ;; g]" using assms by (simp add: HomFtorDist')
  moreover have "(Hom[X,f]) ≈>_' (Hom[X,g])" using assms by (simp add: HomFtorCompDef')
  ultimately show ?thesis by (simp add: MakeCatComp SET_def)
qed

lemma HomFtorId':
  assumes a: "LSCategory C" and b: "X ∈ obj" and c: "Y ∈ obj"
  shows   "Hom[X,id Y] = id_' (Hom X Y)"
proof-
  have "(id Y) maps Y to Y" using a c by (simp add: Category.Simps)
  hence 1: "(dom (id Y)) = Y" and 2: "(cod (id Y)) = Y" by auto
  have "Hom[X,id Y] = ZFfun (Hom X (dom (id Y))) (Hom X (cod (id Y))) (λ f . m2z ((z2m f) ;; (id Y)))"
    by (simp add: HomFtorMap_def)
  also have "... = ZFfun (Hom X Y) (Hom X Y) (λ f . m2z ((z2m f) ;; (id Y)))" using 1 2 by simp
  also have "... = ZFfun (Hom X Y) (Hom X Y) (λ f . f)" 
  proof(rule ZFfun_ext, rule allI, rule impI)
    {
      fix h assume aa: "h |∈| (Hom X Y)" show "m2z ((z2m h) ;; (id Y)) = h"
      proof-
        have "(z2m h) maps X to Y" and bb: "m2z (z2m h) = h" 
          using assms aa by (simp add: LSCategory.z2mm2z)+
        hence "(z2m h) ;; (id Y) = (z2m h)" using a by (auto simp add: Category.Simps)
        hence "m2z ((z2m h) ;; (id Y)) = m2z (z2m h)" by simp
        also have "... = h" using bb .
        finally show ?thesis .
      qed
    }
  qed
  finally show ?thesis by (simp add: SET'_def)
qed

lemma HomFtorId: 
  assumes "LSCategory C" and "X ∈ obj" and "Y ∈ obj"
  shows   "Hom[X,id Y] = id (Hom X Y)"
proof-
  have "Hom[X,id Y] = id_' (Hom X Y)" using assms by (simp add: HomFtorId')
  moreover have "(Hom X Y) ∈ obj_'" by (simp add: SET'_def)
  ultimately show ?thesis by (simp add: MakeCatId SET_def)
qed

lemma HomFtorObj':
  assumes a: "LSCategory C"
  and     b: "PreFunctor (HomP[X,←-])"  and c: "X ∈ obj" and d: "Y ∈ obj"
  shows   "(HomP[X,←-]) @@ Y = Hom X Y" 
proof-
  let ?F = "(HomFtor' C X)"
  have "?F ## (id _?F Y) = Hom[X,id Y]" by (simp add: HomFtor'_def)
  also have "... = id _?F (Hom X Y)" using assms by (simp add: HomFtorId HomFtor'_def)
  finally have "?F ## (id _?F Y) = id _?F (Hom X Y)" by simp
  moreover have "Hom X Y ∈ obj _?F" using assms 
    by (simp add: HomFtorId HomFtor'_def SET_def SET'_def MakeCatObj)
  moreover have "Y ∈ obj _?F" using d by (simp add: HomFtor'_def)
  ultimately show ?thesis using b by(simp add: PreFunctor.FmToFo[of ?F Y "Hom X Y"])
qed

lemma HomFtorFtor': 
  assumes a: "LSCategory C"
  and     b: "X ∈ obj"
  shows   "FunctorM (HomP[X,←-])"
proof(intro_locales)
  show PF: "PreFunctor (HomP[X,←-])"
  proof(auto simp add: HomFtor'_def PreFunctor_def SETCategory a HomFtorDist b)
    {
      fix Z assume aa: "Z ∈ obj" 
      show "∃ Y ∈ obj . Hom[X,id Z] = id Y"
      proof(rule_tac x="Hom X Z" in Set.rev_bexI)
        show "Hom X Z ∈ obj" by (simp add: SET_def SET'_def MakeCatObj) 
        show "Hom[X,id Z] = id (Hom X Z)" using assms aa by(simp add:HomFtorId)
      qed
    }
  qed
  {
    fix f Z Y assume aa: "f maps Z to Y" 
    have "(HomP[X,←-]) ## f maps ((HomP[X,←-]) @@ Z) to ((HomP[X,←-]) @@ Y)" 
    proof-
      have bb: "Z ∈ obj" and cc: "Y ∈ obj" using aa a by (simp add: Category.MapsToObj)+
      have dd: "dom f = Z" and ee: "cod f = Y" and ff: "f ∈ mor" using aa by auto
      have "(HomP[X,←-]) ## f = Hom[X,f]" by (simp add: HomFtor'_def)
      moreover have "(HomP[X,←-]) @@ Z = Hom X Z" 
        and "(HomP[X,←-]) @@ Y = Hom X Y" using assms bb cc PF by (simp add: HomFtorObj')+
      moreover have "Hom[X,f] maps (Hom X (dom f)) to (Hom X (cod f))" 
        using assms ff by (simp add: HomFtorMapsTo)
      ultimately show ?thesis using dd ee by simp
    qed
  }
  thus "FunctorM_axioms (HomP[X,←-])" using PF by (auto simp add: FunctorM_axioms_def HomFtor'_def)
qed

lemma HomFtorFtor: 
  assumes a: "LSCategory C"
  and     b: "X ∈ obj"
  shows   "Functor (Hom[X,←-])"
proof-
  have "FunctorM (HomP[X,←-])" using assms by (rule HomFtorFtor')
  thus ?thesis by (simp add: HomFtor_def MakeFtor)
qed 

lemma HomFtorObj:
  assumes "LSCategory C"
  and     "X ∈ obj" and "Y ∈ obj"
  shows   "(Hom[X,←-]) @@ Y = Hom X Y"
proof-
  have "FunctorM (HomP[X,←-])" using assms by (simp add: HomFtorFtor')
  hence 1: "PreFunctor (HomP[X,←-])" by (simp add: FunctorM_def)
  moreover have "CatDom (HomP[X,←-]) = C" by (simp add: HomFtor'_def)
  ultimately have "(Hom[X,←-]) @@ Y = (HomP[X,←-]) @@ Y" using assms by (simp add: MakeFtorObj HomFtor_def)
  thus ?thesis using assms 1 by (simp add: HomFtorObj')
qed

definition
  HomFtorMapContra :: "('o,'m,'a) LSCategory_scheme → 'm → 'o → ZF" (‹HomCı[_,_]› [65,65] 65) where
  "HomFtorMapContra C g X ≡ ZFfun (Hom (cod g) X) (Hom (dom g) X) (λ f . m2z (g ;; (z2m f)))"

definition 
  HomFtorContra' :: "('o,'m,'a) LSCategory_scheme → 'o →
      ('o,ZF,'m,ZF,(mor2ZF :: 'm → ZF, … :: 'a),unit) Functor" (‹HomPı[←-,_]› [65] 65) where
  "HomFtorContra' C X ≡ (
        CatDom = (Op C),
        CatCod = SET ,
        MapM = λ g . HomC[g,X]
  )"

definition HomFtorContra (‹Homı[←-,_]› [65] 65) where "HomFtorContra C X ≡ MakeFtor(HomFtorContra' C X)"

lemma HomContraAt: "x |∈| (Hom (cod f) X) ==> (HomC[f,X]) |@| x = m2z (f ;; (z2m x))"
  by (simp add: HomFtorMapContra_def ZFfunApp)

lemma mor2ZF_Op: "mor2ZF (Op C) = mor2ZF C"  
apply (cases C)
apply (simp add: OppositeCategory_def)
done

lemma mor_Op: "mor _C = mor" by (simp add: OppositeCategory_def)
lemma obj_Op: "obj _C = obj" by (simp add: OppositeCategory_def)

lemma ZF2mor_Op: "ZF2mor (Op C) f = ZF2mor C f"
by (simp add: ZF2mor_def mor2ZF_Op mor_Op)

lemma mapsTo_Op: "f maps _C Y to X = f maps X to Y"
by (auto simp add: OppositeCategory_def mor_Op MapsTo_def)

lemma HOMCollection_Op: "HOMCollection (Op C) X Y = HOMCollection C Y X"
by (simp add: HOMCollection_def mapsTo_Op mor2ZF_Op)

lemma Hom_Op: "Hom _C X Y = Hom Y X"
by (simp add: HomSet_def HOMCollection_Op)

lemma HomFtorContra': "HomP[←-,X] = HomP _C[X,←-]"
apply (simp add:  HomFtorContra'_def 
                      HomFtor'_def HomFtorMapContra_def HomFtorMap_def mor2ZF_Op ZF2mor_Op Hom_Op)
by (simp add: OppositeCategory_def)

lemma HomFtorContra: "Hom[←-,X] = Hom _C[X,←-]"
by (auto simp add: HomFtorContra' HomFtorContra_def HomFtor_def)

lemma HomFtorContraDom: "CatDom (Hom[←-,X]) = Op C"
by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)

lemma HomFtorContraCod: "CatCod (Hom[←-,X]) = SET"
by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)

lemma LSCategory_Op: assumes "LSCategory C" shows "LSCategory (Op C)"
proof(auto simp only: LSCategory_def)
  show "Category (Op C)" using assms by (simp add: OpCatCat)
  show "LSCategory_axioms (Op C)" using assms
    by (simp add: LSCategory_axioms_def mor_Op obj_Op mor2ZF_Op HOMCollection_Op 
                     LSCategory.mor2ZFInj LSCategory.HOMSetIsSet LSCategory.m2zExt)
qed

lemma HomFtorContraFtor:
  assumes "LSCategory C"
  and     "X ∈ obj"
  shows   "Ftor (Hom[←-,X]) : (Op C) ⟶ SET"
proof(auto simp only: functor_abbrev_def)
  show "Functor (Hom[←-,X])"
  proof-
    have "Hom[←-,X] = Hom _C[X,←-]" by (simp add: HomFtorContra)
    moreover have "LSCategory (Op C)" using assms by (simp add: LSCategory_Op)
    moreover have "X ∈ obj _C" using assms by (simp add: OppositeCategory_def)
    ultimately show ?thesis using assms by (simp add: HomFtorFtor)
  qed
  show "CatDom (Hom[←-,X]) = Op C" by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
  show "CatCod (Hom[←-,X]) = SET" by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
qed

lemma HomFtorOpObj:
  assumes "LSCategory C"
  and     "X ∈ obj" and "Y ∈ obj"
  shows   "(Hom[←-,X]) @@ Y = Hom Y X"
proof-
  have 1: "X ∈ Obj (Op C)" and 2: "Y ∈ Obj (Op C)" using assms by (simp add: OppositeCategory_def)+
  have "(Hom[←-,X]) @@ Y = (Hom _C[X,←-]) @@ Y" by (simp add: HomFtorContra)
  also have "... = (Hom _C X Y)" using assms(1) 1 2 by (simp add: LSCategory_Op HomFtorObj)
  also have "... = (Hom Y X)" by (simp add: Hom_Op)
  finally show ?thesis .
qed
  

lemma HomCHomOp: "HomC[g,X] = Hom _C[X,g]"
apply (simp add:  HomFtorContra'_def 
                      HomFtor'_def HomFtorMapContra_def HomFtorMap_def mor2ZF_Op ZF2mor_Op Hom_Op)
by (simp add: OppositeCategory_def)

lemma HomFtorContraMapsTo:
  assumes "LSCategory C" and "X ∈ obj" and "f ∈ mor" 
  shows "HomC[f,X] maps Hom (cod f) X to Hom (dom f) X"
proof-
  have "LSCategory (Op C)" using assms by(simp add: LSCategory_Op)
  moreover have "X ∈ Obj (Op C)" using assms by (simp add: OppositeCategory_def)
  moreover have "f ∈ Mor (Op C)" using assms by (simp add: OppositeCategory_def)
  ultimately have "Hom _C[X,f] maps Hom _C X (dom _C f) to Hom _C X (cod _C f)" using assms
    by (simp add: HomFtorMapsTo)
  moreover have "HomC[f,X] = Hom _C[X,f]" by (simp add: HomCHomOp)
  moreover have "Hom _C X (dom _C f) = Hom (cod f) X" 
  proof-
    have "Hom _C X (dom _C f) = Hom (dom _C f) X" by (simp add: Hom_Op)
    thus ?thesis by (simp add:  OppositeCategory_def)
  qed
  moreover have "Hom _C X (cod _C f) = Hom (dom f) X"
  proof-
    have "Hom _C X (cod _C f) = Hom (cod _C f) X" by (simp add: Hom_Op)
    thus ?thesis by (simp add:  OppositeCategory_def)
  qed
  ultimately show ?thesis by simp
qed

lemma HomFtorContraMor:
  assumes "LSCategory C" and "X ∈ obj" and "f ∈ mor" 
  shows "HomC[f,X] ∈ Mor SET" and "dom (HomC[f,X]) = Hom (cod f) X" 
  and "cod (HomC[f,X]) = Hom (dom f) X"
proof-
  have "HomC[f,X] maps Hom (cod f) X to Hom (dom f) X" using assms by (simp add: HomFtorContraMapsTo)
  thus "HomC[f,X] ∈ Mor SET" and "dom (HomC[f,X]) = Hom (cod f) X" 
  and "cod (HomC[f,X]) = Hom (dom f) X"
    by auto
qed

lemma HomContraMor:
  assumes "LSCategory C" and "f ∈ Mor C" 
  shows "(Hom[←-,X]) ## f = HomC[f,X]"
by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def assms OppositeCategory_def) 



(*This is used in the proof of the naturality of the Yoneda trans*)
lemma HomCHom:
  assumes "LSCategory C" and "f ∈ Mor C" and "g ∈ Mor C"
  shows "(HomC[g,dom f]) ;; (Hom[dom g,f]) = (Hom[cod g,f]) ;; (HomC[g,cod f])"
proof-
  have ObjDf: "dom f ∈ obj" and ObjDg: "dom g ∈ obj" using assms by (simp add: Category.Cdom)+
  have ObjCg: "cod g ∈ obj" and ObjCf: "cod f ∈ obj" using assms by (simp add: Category.Ccod)+
  have "(HomC[g,dom f]) ;; (Hom[dom g,f]) = (HomC[g,dom f]) |o| (Hom[dom g,f])" 
  proof-
    have "(HomC[g,dom f]) ≈> (Hom[dom g,f])" 
    proof(rule CompDefinedI)
      show "Hom[dom g,f] ∈ Mor SET" using assms ObjDg by (simp add: HomFtorMor)
      show "HomC[g,dom f] ∈ Mor SET" using assms ObjDf by (simp add: HomFtorContraMor)
      show "cod (HomC[g,dom f]) = dom (Hom[dom g,f])" using assms ObjDg ObjDf
        by (simp add: HomFtorMor HomFtorContraMor)
    qed
    thus ?thesis by(simp add: SET_def SET'_def MakeCatComp2)
  qed
  also have "... = ZFfun (Hom (cod g) (dom f)) (Hom (dom g) (cod f))
              ((λ h . m2z ((z2m h) ;; f)) o (λ h . m2z (g ;; (z2m h))))" 
  proof(simp add: HomFtorMapContra_def HomFtorMap_def, rule ZFfunComp, rule allI, rule impI)
    {
      fix x assume aa: "x |∈| (Hom (cod g) (dom f))"
      show "(m2z (g ;; (z2m x))) |∈| (Hom (dom g) (dom f))"
      proof(rule LSCategory.m2zz2m, simp_all add: assms(1) ObjDg ObjDf)
        have "g maps (dom g) to (cod g)" using assms by auto
        moreover have "(z2m x) maps (cod g) to (dom f)" using aa ObjCg ObjDf assms(1) 
          by (simp add: LSCategory.z2mm2z)
        ultimately show "g ;; (z2m x) maps (dom g) to (dom f)" using assms(1)
          by (simp add: Category.Ccompt)
      qed
    }
  qed
  also have "... = ZFfun (Hom (cod g) (dom f)) (Hom (dom g) (cod f))
              ((λ h . m2z (g ;; (z2m h))) o (λ h . m2z ((z2m h) ;; f)))" 
  proof(rule ZFfun_ext, rule allI, rule impI)
    {
      fix h assume aa: "h |∈| (Hom (cod g) (dom f))"
      show "((λ h . m2z ((z2m h) ;; f)) o (λ h . m2z (g ;; (z2m h)))) h =
        ((λ h . m2z (g ;; (z2m h))) o (λ h . m2z ((z2m h) ;; f))) h"
      proof-
        have MapsTo1: "(z2m h) maps (cod g) to (dom f)" using assms(1) ObjCg ObjDf aa by (simp add: LSCategory.z2mm2z)
        have CompDef1: "(z2m h) ≈> f"
        proof(rule CompDefinedI)
          show "f ∈ mor" using assms by simp
          show "(z2m h) ∈ mor" and "cod (z2m h) = dom f" using MapsTo1 by auto
        qed
        have CompDef2: "g ≈> (z2m h)"
        proof(rule CompDefinedI)
          show "g ∈ mor" using assms by simp
          thus "(z2m h) ∈ mor" and "cod g = dom (z2m h)" using MapsTo1 by auto
        qed
        have c1: "(z2m h) ;; f ∈ Mor C" using assms CompDef1 by (simp add: Category.MapsToMorDomCod)
        have c2: "g ;; (z2m h) ∈ Mor C" using assms CompDef2 by (simp add: Category.MapsToMorDomCod)
        have "g ;; (z2m (m2z ((z2m h) ;; f))) = g ;; ((z2m h) ;; f)" using assms(1) c1
          by (simp add: LSCategory.m2zz2mInv)
        also have "... = (g ;; (z2m h)) ;; f" using CompDef1 CompDef2 assms by (simp add: Category.Cassoc)
        also have "... = (z2m (m2z (g ;; (z2m h)))) ;; f" using assms(1) c2
          by (simp add: LSCategory.m2zz2mInv)
        finally have "g ;; (z2m (m2z ((z2m h) ;; f))) = (z2m (m2z (g ;; (z2m h)))) ;; f" .
        thus ?thesis by simp
      qed
    }
  qed
  also have "... = (Hom[cod g,f]) |o| (HomC[g,cod f])"
  proof(simp add: HomFtorMapContra_def HomFtorMap_def, rule ZFfunComp[THEN sym], rule allI, rule impI)
    {
      fix x assume aa: "x |∈| (Hom cod g dom f)"
      show "m2z ((z2m x) ;; f) |∈| (Hom cod g cod f)" 
      proof(rule LSCategory.m2zz2m, simp_all add: assms(1) ObjCg ObjCf)
        have "f maps (dom f) to (cod f)" using assms by auto
        moreover have "(z2m x) maps (cod g) to (dom f)" using aa ObjCg ObjDf assms(1) 
          by (simp add: LSCategory.z2mm2z)
        ultimately show "(z2m x) ;; f maps cod g to cod f" using assms(1)
          by (simp add: Category.Ccompt)
      qed
    }
  qed
  also have "... = (Hom[cod g,f]) ;; (HomC[g,cod f])"
  proof-
    have "(Hom[cod g,f]) ≈> (HomC[g,cod f])"
    proof(rule CompDefinedI)
      show "Hom[cod g,f] ∈ Mor SET" using assms ObjCg by (simp add: HomFtorMor)
      show "HomC[g,cod f] ∈ Mor SET" using assms ObjCf by (simp add: HomFtorContraMor)
      show "cod (Hom[cod g,f]) = dom (HomC[g,cod f])" using assms ObjCg ObjCf
        by (simp add: HomFtorMor HomFtorContraMor)
    qed
    thus ?thesis by(simp add: SET_def SET'_def MakeCatComp2)
  qed
  finally show ?thesis .
qed

end