Theory SetCat

(*
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⇘SET⇙ ZFfun A B f = B"
by(simp add: SET_def MakeCat_def SET'_def ZFfunCod)

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

lemma SETdom: "isZFfun (ZFfun A B f) ⟹ dom⇘SET⇙ 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 ≈>⇘SET⇙ 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⇘SET⇙ 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 ≈>⇘SET⇙ g" shows "f ;;⇘SET⇙ g = f |o| g"
proof-
  have a: "f ≈>⇘MakeCat SET'⇙ g" using assms by (simp add: SET_def)
  have "f ;;⇘SET⇙ g = f ;;⇘MakeCat SET'⇙ g" by (simp add: SET_def)
  also have "... = f ;;⇘SET'⇙ g" using a  by (simp  add: MakeCatComp2)
  finally show ?thesis by (simp add: SET'_def)
qed

lemma SETCompAt:
  assumes "f ≈>⇘SET ⇙g" and "x |∈|  |dom| f" shows "(f ;;⇘SET ⇙g) |@| x = g |@| (f |@| x)"
proof-
  have "f ;;⇘SET⇙ 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⇘SET⇙ 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⇘SET ⇙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⇘C⇙ ∧ m2z⇘C⇙ m = f"

definition
  "HOMCollection C X Y ≡ {m2z⇘C⇙ f | f . f maps⇘C⇙ 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⇘C⇙ ; y ∈ mor⇘C⇙ ; m2z⇘C⇙ x = m2z⇘C⇙ y⟧ ⟹  x = y;
  ⟦X ∈ obj⇘C⇙ ; Y ∈ obj⇘C⇙⟧ ⟹ 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⇘C⇙ X (dom⇘C⇙ g)) (Hom⇘C⇙ X (cod⇘C⇙ g)) (λ f . m2z⇘C⇙ ((z2m⇘C⇙ f) ;;⇘C⇙ 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⇘C⇙[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⇘C⇙" and c: "f ∈ mor⇘C⇙" and d: "x |∈| (Hom⇘C⇙ X (dom⇘C⇙ f))"
  shows "(m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f)) |∈| (Hom⇘C⇙ X (cod⇘C⇙ f))"
proof-
  have 1: "dom⇘C⇙ f ∈ obj⇘C⇙" and 2: "cod⇘C⇙ f ∈ obj⇘C⇙" using a c by (simp add: Category.Simps)+
  have "z2m⇘C⇙ x maps⇘C⇙ X to (dom⇘C⇙ f)"  using a b d 1 by (auto simp add: LSCategory.z2mm2z)
  hence "(z2m⇘C⇙ x) ;;⇘C⇙ f maps⇘C⇙ X to (cod⇘C⇙ f)" using a c by (auto intro: Category.Ccompt)
  hence "(m2z⇘C⇙ ((z2m⇘C⇙ x) ;;⇘C⇙ f)) |∈| (Hom⇘C⇙ X (cod⇘C⇙ 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⇘C⇙" and "f ∈ mor⇘C⇙"
  shows "Hom⇘C⇙[X,f] ∈ mor⇘SET'⇙" 
proof(simp add: HomFtorMap_def)
  {
    fix x assume "x |∈| (Hom⇘C⇙ X dom⇘C⇙ f)" 
    hence "m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f) |∈| (Hom⇘C⇙ X cod⇘C⇙ f)" using assms by (blast intro: HomFtorMapLemma1)
  }
  hence "∀ x . x |∈| (Hom⇘C⇙ X dom⇘C⇙ f) ⟶ (m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f)) |∈| (Hom⇘C⇙ X cod⇘C⇙ f)" by (simp)
  hence "isZFfun (ZFfun (Hom⇘C⇙ X dom⇘C⇙ f) (Hom⇘C⇙ X cod⇘C⇙ f) (λ x . m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f)))"
    by (simp add: SETfun)
  thus "ZFfun (Hom⇘C⇙ X dom⇘C⇙ f) (Hom⇘C⇙ X cod⇘C⇙ f) (λ x . m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f)) ∈ mor⇘SET'⇙"
    by (simp add: SET'_def)
qed

lemma HomFtorMor':
  assumes "LSCategory C" and "X ∈ obj⇘C⇙" and "f ∈ mor⇘C⇙"
  shows   "Hom⇘C⇙[X,f] maps⇘SET'⇙ Hom⇘C ⇙X (dom⇘C⇙ f) to Hom⇘C ⇙X (cod⇘C⇙ f)"  
proof-
  have "Hom⇘C⇙[X,f] ∈ mor⇘SET'⇙" using assms by (simp add: HomFtorInMor')
  moreover have "dom⇘SET'⇙ (Hom⇘C⇙[X,f]) = Hom⇘C ⇙X (dom⇘C⇙ f)"
    by(simp add: HomFtorMap_def SET'_def ZFfunDom)
  moreover have "cod⇘SET'⇙ (Hom⇘C⇙[X,f]) = Hom⇘C ⇙X (cod⇘C⇙ 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⇘C ⇙; f ∈ mor⇘C ⇙⟧ ⟹ Hom⇘C⇙[X,f] maps⇘SET⇙ Hom⇘C ⇙X (dom⇘C⇙ f) to Hom⇘C ⇙X (cod⇘C⇙ f)"
by (simp add: HomFtorMor' SET_def MakeCatMapsTo)

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

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

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

lemma HomFtorDist:
  assumes "LSCategory C" and "X ∈ obj⇘C⇙" and "f ≈>⇘C⇙ g"
  shows   "(Hom⇘C⇙[X,f]) ;;⇘SET⇙ (Hom⇘C⇙[X,g]) = Hom⇘C⇙[X,f ;;⇘C⇙ g]"
proof-
  have "(Hom⇘C⇙[X,f]) ;;⇘SET'⇙ (Hom⇘C⇙[X,g]) = Hom⇘C⇙[X,f ;;⇘C⇙ g]" using assms by (simp add: HomFtorDist')
  moreover have "(Hom⇘C⇙[X,f]) ≈>⇘SET'⇙ (Hom⇘C⇙[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⇘C⇙" and c: "Y ∈ obj⇘C⇙"
  shows   "Hom⇘C⇙[X,id⇘C⇙ Y] = id⇘SET'⇙ (Hom⇘C ⇙X Y)"
proof-
  have "(id⇘C⇙ Y) maps⇘C⇙ Y to Y" using a c by (simp add: Category.Simps)
  hence 1: "(dom⇘C⇙ (id⇘C⇙ Y)) = Y" and 2: "(cod⇘C⇙ (id⇘C⇙ Y)) = Y" by auto
  have "Hom⇘C⇙[X,id⇘C⇙ Y] = ZFfun (Hom⇘C ⇙X (dom⇘C⇙ (id⇘C⇙ Y))) (Hom⇘C ⇙X (cod⇘C⇙ (id⇘C⇙ Y))) (λ f . m2z⇘C⇙ ((z2m⇘C⇙ f) ;;⇘C⇙ (id⇘C⇙ Y)))"
    by (simp add: HomFtorMap_def)
  also have "... = ZFfun (Hom⇘C ⇙X Y) (Hom⇘C ⇙X Y) (λ f . m2z⇘C⇙ ((z2m⇘C⇙ f) ;;⇘C⇙ (id⇘C⇙ Y)))" using 1 2 by simp
  also have "... = ZFfun (Hom⇘C ⇙X Y) (Hom⇘C ⇙X Y) (λ f . f)" 
  proof(rule ZFfun_ext, rule allI, rule impI)
    {
      fix h assume aa: "h |∈| (Hom⇘C⇙ X Y)" show "m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ (id⇘C⇙ Y)) = h"
      proof-
        have "(z2m⇘C⇙ h) maps⇘C⇙ X to Y" and bb: "m2z⇘C⇙ (z2m⇘C⇙ h) = h" 
          using assms aa by (simp add: LSCategory.z2mm2z)+
        hence "(z2m⇘C⇙ h) ;;⇘C⇙ (id⇘C⇙ Y) = (z2m⇘C⇙ h)" using a by (auto simp add: Category.Simps)
        hence "m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ (id⇘C⇙ Y)) = m2z⇘C⇙ (z2m⇘C⇙ 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⇘C⇙" and "Y ∈ obj⇘C⇙"
  shows   "Hom⇘C⇙[X,id⇘C⇙ Y] = id⇘SET⇙ (Hom⇘C ⇙X Y)"
proof-
  have "Hom⇘C⇙[X,id⇘C⇙ Y] = id⇘SET'⇙ (Hom⇘C ⇙X Y)" using assms by (simp add: HomFtorId')
  moreover have "(Hom⇘C ⇙X Y) ∈ obj⇘SET'⇙" 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⇘C⇙[X,─])"  and c: "X ∈ obj⇘C⇙" and d: "Y ∈ obj⇘C⇙"
  shows   "(HomP⇘C⇙[X,─]) @@ Y = Hom⇘C ⇙X Y" 
proof-
  let ?F = "(HomFtor' C X)"
  have "?F ## (id⇘CatDom ?F⇙ Y) = Hom⇘C⇙[X,id⇘C⇙ Y]" by (simp add: HomFtor'_def)
  also have "... = id⇘CatCod ?F⇙ (Hom⇘C ⇙X Y)" using assms by (simp add: HomFtorId HomFtor'_def)
  finally have "?F ## (id⇘CatDom ?F⇙ Y) = id⇘CatCod ?F⇙ (Hom⇘C ⇙X Y)" by simp
  moreover have "Hom⇘C ⇙X Y ∈ obj⇘CatCod ?F⇙" using assms 
    by (simp add: HomFtorId HomFtor'_def SET_def SET'_def MakeCatObj)
  moreover have "Y ∈ obj⇘CatDom ?F⇙" using d by (simp add: HomFtor'_def)
  ultimately show ?thesis using b by(simp add: PreFunctor.FmToFo[of ?F Y "Hom⇘C ⇙X Y"])
qed

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

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

lemma HomFtorObj:
  assumes "LSCategory C"
  and     "X ∈ obj⇘C⇙" and "Y ∈ obj⇘C⇙"
  shows   "(Hom⇘C⇙[X,─]) @@ Y = Hom⇘C ⇙X Y"
proof-
  have "FunctorM (HomP⇘C⇙[X,─])" using assms by (simp add: HomFtorFtor')
  hence 1: "PreFunctor (HomP⇘C⇙[X,─])" by (simp add: FunctorM_def)
  moreover have "CatDom (HomP⇘C⇙[X,─]) = C" by (simp add: HomFtor'_def)
  ultimately have "(Hom⇘C⇙[X,─]) @@ Y = (HomP⇘C⇙[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⇘C⇙ (cod⇘C⇙ g) X) (Hom⇘C⇙ (dom⇘C⇙ g) X) (λ f . m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ 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⇘C⇙[g,X]
  ⦈"

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

lemma HomContraAt: "x |∈| (Hom⇘C ⇙(cod⇘C⇙ f) X) ⟹ (HomC⇘C⇙[f,X]) |@| x = m2z⇘C⇙ (f ;;⇘C⇙ (z2m⇘C⇙ 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⇘Op C⇙ = mor⇘C⇙" by (simp add: OppositeCategory_def)
lemma obj_Op: "obj⇘Op C⇙ = obj⇘C⇙" 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⇘Op C⇙ Y to X = f maps⇘C⇙ 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⇘Op C⇙ X Y = Hom⇘C⇙ Y X"
by (simp add: HomSet_def HOMCollection_Op)

lemma HomFtorContra': "HomP⇘C⇙[─,X] = HomP⇘Op 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⇘C⇙[─,X] = Hom⇘Op C⇙[X,─]"
by (auto simp add: HomFtorContra' HomFtorContra_def HomFtor_def)

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

lemma HomFtorContraCod: "CatCod (Hom⇘C⇙[─,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⇘C⇙"
  shows   "Ftor (Hom⇘C⇙[─,X]) : (Op C) ⟶ SET"
proof(auto simp only: functor_abbrev_def)
  show "Functor (Hom⇘C⇙[─,X])"
  proof-
    have "Hom⇘C⇙[─,X] = Hom⇘Op C⇙[X,─]" by (simp add: HomFtorContra)
    moreover have "LSCategory (Op C)" using assms by (simp add: LSCategory_Op)
    moreover have "X ∈ obj⇘Op C⇙" using assms by (simp add: OppositeCategory_def)
    ultimately show ?thesis using assms by (simp add: HomFtorFtor)
  qed
  show "CatDom (Hom⇘C⇙[─,X]) = Op C" by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
  show "CatCod (Hom⇘C⇙[─,X]) = SET" by(simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
qed

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

lemma HomCHomOp: "HomC⇘C⇙[g,X] = Hom⇘Op 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⇘C⇙" and "f ∈ mor⇘C⇙" 
  shows "HomC⇘C⇙[f,X] maps⇘SET⇙ Hom⇘C ⇙(cod⇘C⇙ f) X  to Hom⇘C ⇙(dom⇘C⇙ 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⇘Op C⇙[X,f] maps⇘SET⇙ Hom⇘Op C ⇙X (dom⇘Op C⇙ f) to Hom⇘Op C ⇙X (cod⇘Op C⇙ f)" using assms
    by (simp add: HomFtorMapsTo)
  moreover have "HomC⇘C⇙[f,X] = Hom⇘Op C⇙[X,f]" by (simp add: HomCHomOp)
  moreover have "Hom⇘Op C ⇙X (dom⇘Op C⇙ f) = Hom⇘C ⇙(cod⇘C⇙ f) X" 
  proof-
    have "Hom⇘Op C ⇙X (dom⇘Op C⇙ f) = Hom⇘C⇙ (dom⇘Op C⇙ f) X" by (simp add: Hom_Op)
    thus ?thesis by (simp add:  OppositeCategory_def)
  qed
  moreover have "Hom⇘Op C ⇙X (cod⇘Op C⇙ f) = Hom⇘C ⇙(dom⇘C⇙ f) X"
  proof-
    have "Hom⇘Op C ⇙X (cod⇘Op C⇙ f) = Hom⇘C⇙ (cod⇘Op 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⇘C⇙" and "f ∈ mor⇘C⇙" 
  shows "HomC⇘C⇙[f,X] ∈ Mor SET" and "dom⇘SET⇙ (HomC⇘C⇙[f,X]) = Hom⇘C ⇙(cod⇘C⇙ f) X" 
  and "cod⇘SET⇙ (HomC⇘C⇙[f,X]) = Hom⇘C ⇙(dom⇘C⇙ f) X"
proof-
  have "HomC⇘C⇙[f,X] maps⇘SET⇙ Hom⇘C ⇙(cod⇘C⇙ f) X  to Hom⇘C ⇙(dom⇘C⇙ f) X" using assms by (simp add: HomFtorContraMapsTo)
  thus "HomC⇘C⇙[f,X] ∈ Mor SET" and "dom⇘SET⇙ (HomC⇘C⇙[f,X]) = Hom⇘C ⇙(cod⇘C⇙ f) X" 
  and "cod⇘SET⇙ (HomC⇘C⇙[f,X]) = Hom⇘C ⇙(dom⇘C⇙ f) X"
    by auto
qed

lemma HomContraMor:
  assumes "LSCategory C" and "f ∈ Mor C" 
  shows "(Hom⇘C⇙[─,X]) ## f = HomC⇘C⇙[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⇘C⇙[g,dom⇘C⇙ f]) ;;⇘SET⇙ (Hom⇘C⇙[dom⇘C⇙ g,f]) = (Hom⇘C⇙[cod⇘C⇙ g,f]) ;;⇘SET⇙ (HomC⇘C⇙[g,cod⇘C⇙ f])"
proof-
  have ObjDf: "dom⇘C⇙ f ∈ obj⇘C⇙" and ObjDg: "dom⇘C⇙ g ∈ obj⇘C⇙" using assms by (simp add: Category.Cdom)+
  have ObjCg: "cod⇘C⇙ g ∈ obj⇘C⇙" and ObjCf: "cod⇘C⇙ f ∈ obj⇘C⇙" using assms by (simp add: Category.Ccod)+
  have "(HomC⇘C⇙[g,dom⇘C⇙ f]) ;;⇘SET⇙ (Hom⇘C⇙[dom⇘C⇙ g,f]) = (HomC⇘C⇙[g,dom⇘C⇙ f]) |o| (Hom⇘C⇙[dom⇘C⇙ g,f])" 
  proof-
    have "(HomC⇘C⇙[g,dom⇘C⇙ f]) ≈>⇘SET⇙ (Hom⇘C⇙[dom⇘C⇙ g,f])" 
    proof(rule CompDefinedI)
      show "Hom⇘C⇙[dom⇘C⇙ g,f] ∈ Mor SET" using assms ObjDg by (simp add: HomFtorMor)
      show "HomC⇘C⇙[g,dom⇘C⇙ f] ∈ Mor SET" using assms ObjDf by (simp add: HomFtorContraMor)
      show "cod⇘SET⇙ (HomC⇘C⇙[g,dom⇘C⇙ f]) = dom⇘SET⇙ (Hom⇘C⇙[dom⇘C⇙ 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⇘C⇙ (cod⇘C⇙ g) (dom⇘C⇙ f)) (Hom⇘C⇙ (dom⇘C⇙ g) (cod⇘C⇙ f)) 
              ((λ h . m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f)) o (λ h . m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ h))))" 
  proof(simp add: HomFtorMapContra_def HomFtorMap_def, rule ZFfunComp, rule allI, rule impI)
    {
      fix x assume aa: "x |∈| (Hom⇘C⇙ (cod⇘C⇙ g) (dom⇘C⇙ f))"
      show "(m2z⇘C ⇙(g ;;⇘C⇙ (z2m⇘C ⇙x))) |∈| (Hom⇘C⇙ (dom⇘C⇙ g) (dom⇘C⇙ f))"
      proof(rule LSCategory.m2zz2m, simp_all add: assms(1) ObjDg ObjDf)
        have "g maps⇘C⇙ (dom⇘C⇙ g) to (cod⇘C⇙ g)" using assms by auto
        moreover have "(z2m⇘C ⇙x) maps⇘C⇙ (cod⇘C⇙ g) to (dom⇘C⇙ f)" using aa ObjCg ObjDf assms(1) 
          by (simp add: LSCategory.z2mm2z)
        ultimately show "g ;;⇘C⇙ (z2m⇘C ⇙x) maps⇘C⇙ (dom⇘C⇙ g) to (dom⇘C⇙ f)" using assms(1)
          by (simp add: Category.Ccompt)
      qed
    }
  qed
  also have "... = ZFfun (Hom⇘C⇙ (cod⇘C⇙ g) (dom⇘C⇙ f)) (Hom⇘C⇙ (dom⇘C⇙ g) (cod⇘C⇙ f)) 
              ((λ h . m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ h))) o (λ h . m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f)))" 
  proof(rule ZFfun_ext, rule allI, rule impI)
    {
      fix h assume aa: "h |∈| (Hom⇘C⇙ (cod⇘C⇙ g) (dom⇘C⇙ f))"
      show "((λ h . m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f)) o (λ h . m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ h)))) h = 
        ((λ h . m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ h))) o (λ h . m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f))) h"
      proof-
        have MapsTo1: "(z2m⇘C⇙ h) maps⇘C⇙ (cod⇘C⇙ g) to (dom⇘C⇙ f)" using assms(1) ObjCg ObjDf aa by (simp add: LSCategory.z2mm2z)
        have CompDef1: "(z2m⇘C⇙ h) ≈>⇘C⇙ f"
        proof(rule CompDefinedI)
          show "f ∈ mor⇘C⇙" using assms by simp
          show "(z2m⇘C⇙ h) ∈ mor⇘C⇙" and "cod⇘C⇙ (z2m⇘C⇙ h) = dom⇘C⇙ f" using MapsTo1 by auto
        qed
        have CompDef2: "g ≈>⇘C⇙ (z2m⇘C⇙ h)"
        proof(rule CompDefinedI)
          show "g ∈ mor⇘C⇙" using assms by simp
          thus "(z2m⇘C⇙ h) ∈ mor⇘C⇙" and "cod⇘C⇙ g = dom⇘C⇙ (z2m⇘C⇙ h)" using MapsTo1 by auto
        qed
        have c1: "(z2m⇘C⇙ h) ;;⇘C⇙ f ∈ Mor C" using assms CompDef1 by (simp add: Category.MapsToMorDomCod)
        have c2: "g ;;⇘C⇙ (z2m⇘C⇙ h) ∈ Mor C" using assms CompDef2 by (simp add: Category.MapsToMorDomCod)
        have "g ;;⇘C⇙ (z2m⇘C⇙ (m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f))) = g ;;⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f)" using assms(1) c1
          by (simp add: LSCategory.m2zz2mInv)
        also have "... = (g ;;⇘C⇙ (z2m⇘C⇙ h)) ;;⇘C⇙ f" using CompDef1 CompDef2 assms by (simp add: Category.Cassoc)
        also have "... = (z2m⇘C⇙ (m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ h)))) ;;⇘C⇙ f" using assms(1) c2
          by (simp add: LSCategory.m2zz2mInv)
        finally have "g ;;⇘C⇙ (z2m⇘C⇙ (m2z⇘C⇙ ((z2m⇘C⇙ h) ;;⇘C⇙ f))) = (z2m⇘C⇙ (m2z⇘C⇙ (g ;;⇘C⇙ (z2m⇘C⇙ h)))) ;;⇘C⇙ f" .
        thus ?thesis by simp
      qed
    }
  qed
  also have "... = (Hom⇘C⇙[cod⇘C⇙ g,f]) |o| (HomC⇘C⇙[g,cod⇘C⇙ f])"
  proof(simp add: HomFtorMapContra_def HomFtorMap_def, rule ZFfunComp[THEN sym], rule allI, rule impI)
    {
      fix x assume aa: "x |∈| (Hom⇘C⇙ cod⇘C⇙ g dom⇘C⇙ f)"
      show "m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f) |∈| (Hom⇘C⇙ cod⇘C⇙ g cod⇘C⇙ f)" 
      proof(rule LSCategory.m2zz2m, simp_all add: assms(1) ObjCg ObjCf)
        have "f maps⇘C⇙ (dom⇘C⇙ f) to (cod⇘C⇙ f)" using assms by auto
        moreover have "(z2m⇘C ⇙x) maps⇘C⇙ (cod⇘C⇙ g) to (dom⇘C⇙ f)" using aa ObjCg ObjDf assms(1) 
          by (simp add: LSCategory.z2mm2z)
        ultimately show "(z2m⇘C ⇙x) ;;⇘C⇙ f maps⇘C⇙ cod⇘C⇙ g to cod⇘C⇙ f" using assms(1)
          by (simp add: Category.Ccompt)
      qed
    }
  qed
  also have "... = (Hom⇘C⇙[cod⇘C⇙ g,f]) ;;⇘SET⇙ (HomC⇘C⇙[g,cod⇘C⇙ f])"
  proof-
    have "(Hom⇘C⇙[cod⇘C⇙ g,f]) ≈>⇘SET⇙ (HomC⇘C⇙[g,cod⇘C⇙ f])"
    proof(rule CompDefinedI)
      show "Hom⇘C⇙[cod⇘C⇙ g,f] ∈ Mor SET" using assms ObjCg by (simp add: HomFtorMor)
      show "HomC⇘C⇙[g,cod⇘C⇙ f] ∈ Mor SET" using assms ObjCf by (simp add: HomFtorContraMor)
      show "cod⇘SET⇙ (Hom⇘C⇙[cod⇘C⇙ g,f]) = dom⇘SET⇙ (HomC⇘C⇙[g,cod⇘C⇙ 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