Quelle  Yoneda.thy

(*
Author: Alexander Katovsky
*)

section "Yoneda"

theory Yoneda
imports NatTrans SetCat
begin

definition "YFtorNT' C f ≡ (NTDom = Hom[←-,dom f] , NTCod = Hom[←-,cod f] ,
                       NatTransMap = λ B . Hom[B,f])"

definition "YFtorNT C f ≡ MakeNT (YFtorNT' C f)"

lemmas YFtorNT_defs = YFtorNT'_def YFtorNT_def MakeNT_def

lemma YFtorNTCatDom: "NTCatDom (YFtorNT C f) = Op C"
by (simp add: YFtorNT_defs NTCatDom_def HomFtorContraDom)

lemma YFtorNTCatCod: "NTCatCod (YFtorNT C f) = SET"
by (simp add: YFtorNT_defs NTCatCod_def HomFtorContraCod)

lemma YFtorNTApp1: assumes "X ∈ Obj (NTCatDom (YFtorNT C f))" shows "(YFtorNT C f) $$ X = Hom[X,f]"
proof-
  have "(YFtorNT C f) $$ X = (YFtorNT' C f) $$ X" using assms by (simp add: MakeNTApp YFtorNT_def)
  thus ?thesis by (simp add: YFtorNT'_def)
qed

definition 
  "YFtor' C ≡ (
         CatDom = C ,
         CatCod = CatExp (Op C) SET ,
         MapM = λ f . YFtorNT C f
  )"

definition "YFtor C ≡ MakeFtor(YFtor' C)"

lemmas YFtor_defs = YFtor'_def YFtor_def MakeFtor_def

lemma YFtorNTNatTrans':
  assumes "LSCategory C" and "f ∈ Mor C"
  shows "NatTransP (YFtorNT' C f)"
proof(auto simp only: NatTransP_def)
  have Fd: "Ftor (NTDom (YFtorNT' C f)) : (Op C) ⟶ SET" using assms 
    by (simp add:  HomFtorContraFtor Category.Cdom YFtorNT'_def)
  have Fc: "Ftor (NTCod (YFtorNT' C f)) : (Op C) ⟶ SET" using assms 
    by (simp add:  HomFtorContraFtor Category.Ccod YFtorNT'_def)
  show "Functor (NTDom (YFtorNT' C f))" using Fd by auto
  show "Functor (NTCod (YFtorNT' C f))" using Fc by auto
  show "NTCatDom (YFtorNT' C f) = CatDom (NTCod (YFtorNT' C f))"
    by(simp add: YFtorNT'_def NTCatDom_def HomFtorContraDom)
  show "NTCatCod (YFtorNT' C f) = CatCod (NTDom (YFtorNT' C f))"
    by(simp add: YFtorNT'_def NTCatCod_def HomFtorContraCod)
  {
    fix X assume a: "X ∈ Obj (NTCatDom (YFtorNT' C f))"
    show "(YFtorNT' C f) $$ X maps _{(YFtorNT' C f)} (NTDom (YFtorNT' C f) @@ X) to (NTCod (YFtorNT' C f) @@ X)"
    proof-
      have Obj: "X ∈ Obj C" using a by (simp add: NTCatDom_def YFtorNT'_def HomFtorContraDom OppositeCategory_def)
      have H1: "(Hom[←-,dom f]) @@ X = Hom X dom f " using assms Obj by(simp add: HomFtorOpObj Category.Cdom)
      have H2: "(Hom[←-,cod f]) @@ X = Hom X cod f " using assms Obj by(simp add: HomFtorOpObj Category.Ccod)
      have "Hom[X,f] maps (Hom X dom f) to (Hom X cod f)" using assms Obj by (simp add: HomFtorMapsTo)
      thus ?thesis using H1 H2 by(simp add: YFtorNT'_def NTCatCod_def NTCatDom_def HomFtorContraCod)
    qed
  }
  {
    fix g X Y assume a: "g maps _{(YFtorNT' C f)} X to Y"
    show "((NTDom (YFtorNT' C f)) ## g) ;; _{(YFtorNT' C f)} (YFtorNT' C f $$ Y) =
       ((YFtorNT' C f) $$ X) ;; _{(YFtorNT' C f)} (NTCod (YFtorNT' C f) ## g)"
    proof-
      have M1: "g maps _C X to Y" using a by (auto simp add: NTCatDom_def YFtorNT'_def HomFtorContraDom)
      have D1: "dom g = Y" and C1: "cod g = X" using M1 by (auto simp add: OppositeCategory_def)
      have morf: "f ∈ Mor C" and morg: "g ∈ Mor C" using assms M1 by (auto simp add: OppositeCategory_def)
      have H1: "(HomC[g,dom f]) = (Hom[←-,dom f]) ## g" 
        and H2: "(HomC[g,cod f]) = (Hom[←-,cod f]) ## g" using M1 
        by (auto simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
      have "(HomC[g,dom f]) ;; (Hom[dom g,f]) = (Hom[cod g,f]) ;; (HomC[g,cod f])" using assms morf morg
        by (simp add: HomCHom)
      hence "((Hom[←-,dom f]) ## g) ;; (Hom[Y,f]) = (Hom[X,f]) ;; ((Hom[←-,cod f]) ## g)"
        using H1 H2 D1 C1 by simp
      thus ?thesis by (simp add: YFtorNT'_def NTCatCod_def HomFtorContraCod)
    qed
  }
qed

lemma YFtorNTNatTrans:
  assumes "LSCategory C" and "f ∈ Mor C"
  shows "NatTrans (YFtorNT C f)"
by (simp add: assms YFtorNTNatTrans' YFtorNT_def MakeNT)

lemma YFtorNTMor:
  assumes "LSCategory C" and "f ∈ Mor C"
  shows "YFtorNT C f ∈ Mor (CatExp (Op C) SET)"
proof(auto simp add: CatExp_def CatExp'_def MakeCatMor)
  have "f ∈ Mor C" using assms by auto
  thus "NatTrans (YFtorNT C f)" using assms by (simp add: YFtorNTNatTrans)
  show "NTCatDom (YFtorNT C f) = Op C" by (simp add: YFtorNTCatDom) 
  show "NTCatCod (YFtorNT C f) = SET" by (simp add: YFtorNTCatCod) 
qed

lemma YFtorNtMapsTo:
  assumes "LSCategory C" and "f ∈ Mor C"
  shows "YFtorNT C f maps _{(Op C) SET} (Hom[←-,dom f]) to (Hom[←-,cod f])"
proof(rule MapsToI)
  have "f ∈ Mor C"  using assms by auto
  thus 1: "YFtorNT C f ∈ mor _{(Op C) SET}" using assms by (simp add: YFtorNTMor)
  show "dom _{(Op C) SET} YFtorNT C f = Hom[←-,dom f]" using 1 by(simp add:CatExpDom YFtorNT_defs)
  show "cod _{(Op C) SET} YFtorNT C f = Hom[←-,cod f]" using 1 by(simp add:CatExpCod YFtorNT_defs)
qed

lemma YFtorNTCompDef:
  assumes "LSCategory C" and "f ≈> g"
  shows "YFtorNT C f ≈> _{(Op C) SET} YFtorNT C g"
proof(rule CompDefinedI)
  have "f ∈ Mor C" and "g ∈ Mor C" using assms by auto
  hence 1: "YFtorNT C f maps _{(Op C) SET} (Hom[←-,dom f]) to (Hom[←-,cod f])"
    and 2: "YFtorNT C g maps _{(Op C) SET} (Hom[←-,dom g]) to (Hom[←-,cod g])"
    using assms by (simp add: YFtorNtMapsTo)+
  thus "YFtorNT C f ∈ mor _{(Op C) SET}"
    and "YFtorNT C g ∈ mor _{(Op C) SET}" by auto
  have "cod _{(Op C) SET} YFtorNT C f = (Hom[←-,cod f])" using 1 by auto
  moreover have "dom _{(Op C) SET} YFtorNT C g = (Hom[←-,dom g])" using 2 by auto
  moreover have "cod f = dom g" using assms by auto
  ultimately show "cod _{(Op C) SET} YFtorNT C f = dom _{(Op C) SET} YFtorNT C g" by simp
qed

lemma PreSheafCat: "LSCategory C ==> Category (CatExp (Op C) SET)"
by(simp add: YFtor'_def OpCatCat SETCategory CatExpCat)

lemma YFtor'Obj1:
  assumes "X ∈ Obj (CatDom (YFtor' C))" and "LSCategory C"
  shows "(YFtor' C) ## (Id (CatDom (YFtor' C)) X) = Id (CatCod (YFtor' C)) (Hom [←-,X])"
proof(simp add: YFtor'_def, rule NatTransExt)
  have Obj: "X ∈ Obj C" using assms by (simp add: YFtor'_def)
  have HomObj: "(Hom[←-,X]) ∈ Obj (CatExp (Op C) SET)" using assms Obj by(simp add: CatExp_defs HomFtorContraFtor)
  hence Id: "Id (CatExp (Op C) SET) (Hom[←-,X]) ∈ Mor (CatExp (Op C) SET)" using assms 
    by (simp add: PreSheafCat Category.CatIdInMor)
  have CAT: "Category(CatExp (Op C) SET)" using assms by (simp add: PreSheafCat)
  have HomObj: "(Hom[←-,X]) ∈ Obj (CatExp (Op C) SET)" using assms Obj 
    by(simp add: CatExp_defs HomFtorContraFtor)
  show "NatTrans (YFtorNT C (Id C X))"
  proof(rule YFtorNTNatTrans)
    show "LSCategory C" using assms(2) .
    show "Id C X ∈ Mor C" using assms Obj by (simp add: Category.CatIdInMor)
  qed
  show "NatTrans(Id (CatExp (Op C) SET) (Hom[←-,X]))" using Id by (simp add: CatExp_defs)
  show "NTDom (YFtorNT C (Id C X)) = NTDom (Id (CatExp (Op C) SET) (Hom[←-,X]))"
  proof(simp add: YFtorNT_defs)
    have "Hom[←-,dom (Id C X)] = Hom[←-,X]" using assms Obj by (simp add: Category.CatIdDomCod)
    also have "... = dom _{(Op C) SET} (Id (CatExp (Op C) SET) (Hom[←-,X]))" using CAT HomObj
      by (simp add: Category.CatIdDomCod)
    also have "... = NTDom (Id (CatExp (Op C) SET) (Hom[←-,X]))" using Id by (simp add: CatExpDom)
    finally show "Hom[←-,dom (Id C X)] = NTDom (Id (CatExp (Op C) SET) (Hom[←-,X]))" .
  qed
  show "NTCod (YFtorNT C (Id C X)) = NTCod (Id (CatExp (Op C) SET) (Hom[←-,X]))"
  proof(simp add: YFtorNT_defs)
    have "Hom[←-,cod (Id C X)] = Hom[←-,X]" using assms Obj by (simp add: Category.CatIdDomCod)
    also have "... = cod _{(Op C) SET} (Id (CatExp (Op C) SET) (Hom[←-,X]))" using CAT HomObj
      by (simp add: Category.CatIdDomCod)
    also have "... = NTCod (Id (CatExp (Op C) SET) (Hom[←-,X]))" using Id by (simp add: CatExpCod)
    finally show "Hom[←-,cod (Id C X)] = NTCod (Id (CatExp (Op C) SET) (Hom[←-,X]))" .
  qed
  {
    fix Y assume a: "Y ∈ Obj (NTCatDom (YFtorNT C (Id C X)))"
    show "(YFtorNT C (Id C X)) $$ Y = (Id (CatExp (Op C) SET) (Hom[←-,X])) $$ Y"
    proof-
      have CD: "CatDom (Hom[←-,X]) = Op C" by (simp add: HomFtorContraDom)
      have CC: "CatCod (Hom[←-,X]) = SET" by (simp add: HomFtorContraCod)
      have ObjY: "Y ∈ Obj C" and ObjYOp: "Y ∈ Obj (Op C)" using a by(simp add: YFtorNTCatDom OppositeCategory_def)+
      have "(YFtorNT C (Id C X)) $$ Y = (Hom[Y,(Id C X)])" using a by (simp add: YFtorNTApp1)
      also have "... = id (Hom Y X)" using Obj ObjY assms by (simp add: HomFtorId)
      also have "... = id ((Hom[←-,X]) @@ Y)" using Obj ObjY assms by (simp add: HomFtorOpObj )
      also have "... = (IdNatTrans (Hom[←-,X])) $$ Y" using CD CC ObjYOp by (simp add: IdNatTrans_map)
      also have "... = (Id (CatExp (Op C) SET) (Hom[←-,X])) $$ Y" using HomObj by (simp add: CatExpId)
      finally show ?thesis .
    qed
  }
qed

lemma YFtorPreFtor:
  assumes "LSCategory C"
  shows   "PreFunctor (YFtor' C)"
proof(auto simp only: PreFunctor_def)
  have CAT: "Category(CatExp (Op C) SET)" using assms by (simp add: PreSheafCat)
  {
    fix f g assume a: "f ≈> _{(YFtor' C)} g"
    show "(YFtor' C) ## (f ;; _{(YFtor' C)} g) = ((YFtor' C) ## f) ;; _{(YFtor' C)} ((YFtor' C) ## g)" 
    proof(simp add: YFtor'_def, rule NatTransExt)
      have CD: "f ≈> g" using a by (simp add: YFtor'_def)
      have CD2: "YFtorNT C f ≈> _{(Op C) SET} YFtorNT C g" using CD assms by (simp add: YFtorNTCompDef)
      have Mor1: "YFtorNT C f ;; _{(Op C) SET} YFtorNT C g ∈ Mor (CatExp (Op C) SET)" using CAT CD2
        by (simp add: Category.MapsToMorDomCod)
      show "NatTrans (YFtorNT C (f ;; g))" using assms by (simp add: Category.MapsToMorDomCod CD YFtorNTNatTrans)
      show "NatTrans (YFtorNT C f ;; _{(Op C) SET} YFtorNT C g)" using Mor1 by (simp add: CatExpMorNT)
      show "NTDom (YFtorNT C (f ;; g)) = NTDom (YFtorNT C f ;; _{(Op C) SET} YFtorNT C g)"
      proof-
        have 1: "YFtorNT C f ∈ mor _{(Op C) SET}" using CD2 by auto
        have "NTDom (YFtorNT C (f ;; g)) = Hom[←-,dom (f ;; g)]" by (simp add: YFtorNT_defs)
        also have "... = Hom[←-,dom f]" using CD assms by (simp add: Category.MapsToMorDomCod)
        also have "... = NTDom (YFtorNT C f)" by (simp add: YFtorNT_defs)
        also have "... = dom _{(Op C) SET} (YFtorNT C f)" using 1 by (simp add: CatExpDom)
        also have "... = dom _{(Op C) SET} (YFtorNT C f ;; _{(Op C) SET} YFtorNT C g)" using CD2 CAT
          by (simp add: Category.MapsToMorDomCod)
        finally show ?thesis using Mor1 by (simp add: CatExpDom)
      qed
      show "NTCod (YFtorNT C (f ;; g)) = NTCod (YFtorNT C f ;; _{(Op C) SET} YFtorNT C g)"
      proof-
        have 1: "YFtorNT C g ∈ mor _{(Op C) SET}" using CD2 by auto
        have "NTCod (YFtorNT C (f ;; g)) = Hom[←-,cod (f ;; g)]" by (simp add: YFtorNT_defs)
        also have "... = Hom[←-,cod g]" using CD assms by (simp add: Category.MapsToMorDomCod)
        also have "... = NTCod (YFtorNT C g)" by (simp add: YFtorNT_defs)
        also have "... = cod _{(Op C) SET} (YFtorNT C g)" using 1 by (simp add: CatExpCod)
        also have "... = cod _{(Op C) SET} (YFtorNT C f ;; _{(Op C) SET} YFtorNT C g)" using CD2 CAT
          by (simp add: Category.MapsToMorDomCod)
        finally show ?thesis using Mor1 by (simp add: CatExpCod)
      qed
      {
        fix X assume a: "X ∈ Obj (NTCatDom (YFtorNT C (f ;; g)))"
        show "YFtorNT C (f ;; g) $$ X = (YFtorNT C f ;; _{(Op C) SET} YFtorNT C g) $$ X"
        proof-
          have Obj: "X ∈ Obj C" and ObjOp: "X ∈ Obj (Op C)" using a by (simp add: YFtorNTCatDom OppositeCategory_def)+
          have App1: "(Hom[X,f]) = (YFtorNT C f) $$ X" 
            and App2: "(Hom[X,g]) = (YFtorNT C g) $$ X" using a by (simp add: YFtorNTApp1 YFtorNTCatDom)+
          have "(YFtorNT C (f ;; g)) $$ X = (Hom[X,(f ;; g)])" using a by (simp add: YFtorNTApp1)
          also have "... = (Hom[X,f]) ;; (Hom[X,g])" using CD assms Obj by (simp add: HomFtorDist)
          also have "... = ((YFtorNT C f) $$ X) ;; ((YFtorNT C g) $$ X)" using App1 App2 by simp
          finally show ?thesis using ObjOp CD2 by (simp add: CatExpDist)
        qed
      }
    qed
  }
  {
    fix X assume a: "X ∈ Obj (CatDom (YFtor' C))"
    show "∃ Y ∈ Obj (CatCod (YFtor' C)) . YFtor' C ## (Id (CatDom (YFtor' C)) X) = Id (CatCod (YFtor' C)) Y"
    proof(rule_tac x="Hom [←-,X]" in Set.rev_bexI)
      have "X ∈ Obj C" using a by(simp add: YFtor'_def)
      thus "Hom [←-,X] ∈ Obj (CatCod (YFtor' C))" using assms by(simp add: YFtor'_def CatExp_defs HomFtorContraFtor)
      show "(YFtor' C) ## (Id (CatDom (YFtor' C)) X) = Id (CatCod (YFtor' C)) (Hom [←-,X])" using a assms
        by (simp add: YFtor'Obj1)
    qed
  }
  show "Category (CatDom (YFtor' C))" using assms by (simp add: YFtor'_def)
  show "Category (CatCod (YFtor' C))" using CAT by (simp add: YFtor'_def)
qed

lemma YFtor'Obj:
  assumes "X ∈ Obj (CatDom (YFtor' C))"
  and     "LSCategory C" 
  shows   "(YFtor' C) @@ X = Hom [←-,X]"
proof(rule PreFunctor.FmToFo, simp_all add: assms YFtor'Obj1 YFtorPreFtor)
  have "X ∈ Obj C" using assms by(simp add: YFtor'_def)
  thus "Hom [←-,X] ∈ Obj (CatCod (YFtor' C))" using assms by(simp add: YFtor'_def CatExp_defs HomFtorContraFtor)
qed

lemma YFtorFtor':
  assumes "LSCategory C"
  shows   "FunctorM (YFtor' C)"
proof(auto simp only: FunctorM_def)
  show "PreFunctor (YFtor' C)" using assms by (rule YFtorPreFtor)
  show "FunctorM_axioms (YFtor' C)" 
  proof(auto simp add:FunctorM_axioms_def)
    {
      fix f X Y assume aa: "f maps _{(YFtor' C)} X to Y"
      show "YFtor' C ## f maps _{(YFtor' C)} YFtor' C @@ X to YFtor' C @@ Y"
      proof-
        have Mor1: "f maps X to Y" using aa by (simp add: YFtor'_def)
        have "Category (CatDom (YFtor' C))" using assms by (simp add: YFtor'_def)
        hence Obj1: "X ∈ Obj (CatDom (YFtor' C))" and
              Obj2: "Y ∈ Obj (CatDom (YFtor' C))" using aa assms by (simp add: Category.MapsToObj)+
        have "(YFtor' C ## f) = YFtorNT C f" by (simp add: YFtor'_def)
        moreover have "YFtor' C @@ X = Hom [←-,X]" 
          and "YFtor' C @@ Y = Hom [←-,Y]" using Obj1 Obj2 assms by (simp add: YFtor'Obj)+
        moreover have "CatCod (YFtor' C) = CatExp (Op C) SET" by (simp add: YFtor'_def)
        moreover have "YFtorNT C f maps _{(Op C) SET} (Hom [←-,X]) to (Hom [←-,Y])" 
          using assms Mor1 by (auto simp add: YFtorNtMapsTo)
        ultimately show ?thesis by simp 
      qed
    }
  qed
qed

lemma YFtorFtor: assumes "LSCategory C" shows "Ftor (YFtor C) : C ⟶ (CatExp (Op C) SET)"
proof(auto simp only: functor_abbrev_def)
  show "Functor (YFtor C)" using assms by(simp add: MakeFtor YFtor_def YFtorFtor')
  show "CatDom (YFtor C) = C" and "CatCod (YFtor C) = (CatExp (Op C) SET)" 
    using assms by(simp add: MakeFtor_def YFtor_def YFtor'_def)+
qed

lemma YFtorObj: 
  assumes "LSCategory C" and "X ∈ Obj C"
  shows "(YFtor C) @@ X = Hom [←-,X]"
proof-
  have "CatDom (YFtor' C) = C" by (simp add: YFtor'_def)
  moreover hence "(YFtor' C) @@ X = Hom [←-,X]" using assms by(simp add: YFtor'Obj)
  moreover have "PreFunctor (YFtor' C)" using assms by (simp add: YFtorPreFtor)
  ultimately show ?thesis using assms by (simp add: MakeFtorObj YFtor_def)
qed

lemma YFtorObj2:
  assumes "LSCategory C" and "X ∈ Obj C" and "Y ∈ Obj C"
  shows "((YFtor C) @@ Y) @@ X = Hom X Y"
proof-
  have "Hom X Y = ((Hom[←-,Y]) @@ X)" using assms by (simp add: HomFtorOpObj)
  also have "... = ((YFtor C @@ Y) @@ X)" using assms by (simp add: YFtorObj)
  finally show ?thesis by simp
qed

lemma YFtorMor: "[LSCategory C ; f ∈ Mor C] ==> (YFtor C) ## f = YFtorNT C f"
by (simp add: YFtor_defs MakeFtorMor)

(*
We can't do this because the presheaf category may not be locally small
definition 
  NatHom ("Nat\<index> _ _") where
  "NatHom C F G \<equiv> Hom\<^bsub>CatExp (Op C) SET\<^esub> F G"
*)

definition "YMap C X η ≡ (η $$ X) |@| (m2z (id X))"
definition "YMapInv' C X F x ≡ (
      NTDom = ((YFtor C) @@ X),
      NTCod = F,
      NatTransMap = λ B . ZFfun (Hom B X) (F @@ B) (λ f . (F ## (z2m f)) |@| x)
  )"
definition "YMapInv C X F x ≡ MakeNT (YMapInv' C X F x)"

lemma YMapInvApp: 
  assumes "X ∈ Obj C" and "B ∈ Obj C" and "LSCategory C"
  shows "(YMapInv C X F x) $$ B = ZFfun (Hom B X) (F @@ B) (λ f . (F ## (z2m f)) |@| x)"
proof-
  have "NTCatDom (MakeNT (YMapInv' C X F x)) = CatDom (NTDom (YMapInv' C X F x))" by (simp add: MakeNT_def NTCatDom_def)
  also have "... = CatDom (Hom[←-,X])" using assms by (simp add: YFtorObj YMapInv'_def)
  also have "... = Op C" using assms HomFtorContraFtor[of C X] by auto
  finally have "NTCatDom (MakeNT (YMapInv' C X F x)) = Op C" .
  hence 1: "B ∈ Obj (NTCatDom (MakeNT (YMapInv' C X F x)))" using assms by (simp add: OppositeCategory_def)
  have "(YMapInv C X F x) $$ B = (MakeNT (YMapInv' C X F x)) $$ B" by (simp add: YMapInv_def)
  also have "... = (YMapInv' C X F x) $$ B" using 1 by(simp add: MakeNTApp)
  finally show ?thesis by (simp add: YMapInv'_def)
qed 

lemma YMapImage:
  assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C"
  and "NT η : (YFtor C @@ X) ==> F"
  shows "(YMap C X η) |∈| (F @@ X)"
proof(simp only: YMap_def)
  have "(YFtor C @@ X) = (Hom[←-,X])" using assms by (auto simp add: YFtorObj)
  moreover have "Ftor (Hom[←-,X]) : (Op C) ⟶ SET" using assms by (simp add: HomFtorContraFtor)
  ultimately have "CatDom (YFtor C @@ X) = Op C" by auto
  hence Obj: "X ∈ Obj (CatDom (YFtor C @@ X))" using assms by (simp add: OppositeCategory_def)
  moreover have "CatCod F = SET" using assms by auto
  moreover have "η $$ X maps _F ((YFtor C @@ X) @@ X) to (F @@ X)" using assms Obj by (simp add: NatTransMapsTo) 
  ultimately have "η $$ X maps ((YFtor C @@ X) @@ X) to (F @@ X)" by simp 
  moreover have "(m2z (Id C X)) |∈| ((YFtor C @@ X) @@ X)" 
  proof-
    have "(Id C X) maps X to X" using assms by (simp add: Category.Simps)
    moreover have "((YFtor C @@ X) @@ X) = Hom X X" using assms by (simp add: YFtorObj2)
    ultimately show ?thesis using assms by (simp add: LSCategory.m2zz2m)
  qed
  ultimately show "((η $$ X) |@| (m2z (Id C X))) |∈| (F @@ X)" by (simp add: SETfunDomAppCod)
qed

lemma YMapInvNatTransP:
  assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and xobj: "X ∈ Obj C" and xinF: "x |∈| (F @@ X)"
  shows "NatTransP (YMapInv' C X F x)"
proof(auto simp only: NatTransP_def, simp_all add: YMapInv'_def NTCatCod_def NTCatDom_def)
  have yf: "(YFtor C @@ X) = Hom[←-,X]" using assms by (simp add: YFtorObj)
  hence hf: "Ftor (YFtor C @@ X) : (Op C) ⟶ SET" using assms by (simp add: HomFtorContraFtor)
  thus "Functor (YFtor C @@ X)" by auto
  show ftf: "Functor F" using assms by auto
  have df: "CatDom F = Op C" and cf: "CatCod F = SET" using assms by auto
  have dy: "CatDom ((YFtor C) @@ X) = Op C" and cy: "CatCod ((YFtor C) @@ X) = SET" using hf by auto
  show "CatDom ((YFtor C) @@ X) = CatDom F" using df dy by simp
  show "CatCod F = CatCod ((YFtor C) @@ X)" using cf cy by simp
  {
    fix Y assume yobja: "Y ∈ Obj (CatDom ((YFtor C) @@ X))"
    show "ZFfun (Hom Y X) (F @@ Y) (λf. (F ## (z2m f)) |@| x) maps _F ((YFtor C @@ X) @@ Y) to (F @@ Y)"
    proof(simp add: cf, rule MapsToI)
      have yobj: "Y ∈ Obj C" using yobja dy by (simp add: OppositeCategory_def)
      have zffun: "isZFfun (ZFfun (Hom Y X) (F @@ Y) (λf. (F ## z2mf) |@| x))" 
      proof(rule SETfun, rule allI, rule impI)
        {
          fix y assume yhom: "y |∈| (Hom Y X)" show "(F ## (z2m y)) |@| x |∈| (F @@ Y)"
          proof-
            let ?f = "(F ## (z2m y))"
            have "(z2m y) maps Y to X" using yhom yobj assms by (simp add: LSCategory.z2mm2z)
            hence "(z2m y) maps _C X to Y" by (simp add: MapsToOp)
            hence "?f maps (F @@ X) to (F @@ Y)" using assms by (simp add: FunctorMapsTo)
            hence "isZFfun (?f)" and "|dom| ?f = F @@ X" and "|cod| ?f = F @@ Y" by (simp add: SETmapsTo)+
            thus "(?f |@| x) |∈| (F @@ Y)" using assms ZFfunDomAppCod[of ?f x] by simp
          qed
        }
      qed
      show "ZFfun (Hom Y X) (F @@ Y) (λf. (F ## z2mf) |@| x) ∈ mor" using zffun
        by(simp add: SETmor)
      show "cod ZFfun (Hom Y X) (F @@ Y) (λf. (F ## z2mf) |@| x) = F @@ Y" using zffun
        by(simp add: SETcod)
      have "(Hom Y X) = (YFtor C @@ X) @@ Y" using assms yobj by (simp add: YFtorObj2)
      thus "dom ZFfun (Hom Y X) (F @@ Y) (λf. (F ## z2mf) |@| x) = (YFtor C @@ X) @@ Y" using zffun
        by(simp add: SETdom)
    qed
  }
  {
    fix f Z Y assume fmaps: "f maps _{((YFtor C ) @@ X)} Z to Y" 
    have fmapsa: "f maps _C Z to Y" using fmaps dy by simp
    hence fmapsb: "f maps Y to Z" by (rule MapsToOpOp)
    hence fmor: "f ∈ Mor C" and fdom: "dom f = Y" and fcod: "cod f = Z" by (auto simp add: OppositeCategory_def)
    hence hc: "(Hom[←-,X]) ## f = (HomC[f,X])" using assms by (simp add: HomContraMor)
    have yobj: "Y ∈ Obj C" and zobj: "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)+
    have Ffmaps: "(F ## f) maps (F @@ Z) to (F @@ Y)" using assms fmapsa by (simp add: FunctorMapsTo)
    have Fzmaps: "∧ h A B . [h |∈| (Hom A B) ; A ∈ Obj C ; B ∈ Obj C] ==>
      (F ## (z2m h)) maps (F @@ B) to (F @@ A)"
    proof-
      fix h A B assume h: "h |∈| (Hom A B)" and oA: "A ∈ Obj C" and oB: "B ∈ Obj C"  
      have "(z2m h) maps A to B" using assms h oA oB by (simp add: LSCategory.z2mm2z)
      hence "(z2m h) maps _C B to A" by (rule MapsToOp)
      thus "(F ## (z2m h)) maps (F @@ B) to (F @@ A)" using assms by (simp add: FunctorMapsTo)
    qed
    have hHomF: "∧h. h |∈| (Hom Z X) ==> (F ## (z2m h)) |@| x |∈| (F @@ Z)" using xobj zobj xinF
    proof-
      fix h assume h: "h |∈| (Hom Z X)"
      have "(F ## (z2m h)) maps (F @@ X) to (F @@ Z)" using xobj zobj h by (simp add: Fzmaps)
      thus "(F ## (z2m h)) |@| x |∈| (F @@ Z)"  using assms by (simp add: SETfunDomAppCod)
    qed
    have Ff: "F ## f = ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)" using Ffmaps by (simp add: SETZFfun)
    have compdefa: "ZFfun (Hom Z X) (Hom Y X) (λh. m2z (f ;; (z2m h))) ≈>
          ZFfun (Hom Y X) (F @@ Y) (λh. (F ## (z2m h)) |@| x)" 
    proof(rule CompDefinedI, simp_all add: SETmor[THEN sym])
      show "isZFfun (ZFfun (Hom Z X) (Hom Y X) (λh. m2z (f ;; (z2m h))))"
      proof(rule SETfun, rule allI, rule impI)
        fix h assume h: "h |∈| (Hom Z X)"
        have "(z2m h) maps Z to X" using assms h xobj zobj by (simp add: LSCategory.z2mm2z)
        hence "f ;; (z2m h) maps Y to X" using fmapsb assms(1) by (simp add: Category.Ccompt)
        thus "(m2z (f ;; (z2m h))) |∈| (Hom Y X)" using assms by (simp add: LSCategory.m2zz2m)
      qed
      moreover show "isZFfun (ZFfun (Hom Y X) (F @@ Y) (λh. (F ## (z2m h)) |@| x))" 
      proof(rule SETfun, rule allI, rule impI)
        fix h assume h: "h |∈| (Hom Y X)"
        have "(F ## (z2m h)) maps (F @@ X) to (F @@ Y)" using xobj yobj h by (simp add: Fzmaps)
        thus "(F ## (z2m h)) |@| x |∈| (F @@ Y)" using assms by (simp add: SETfunDomAppCod)
      qed
      ultimately show "cod(ZFfun (Hom Z X) (Hom Y X) (λh. m2z (f ;; (z2m h)))) =
        dom(ZFfun (Hom Y X) (F @@ Y) (λh. (F ## (z2m h)) |@| x))" by (simp add: SETcod SETdom)
    qed      
    have compdefb: "ZFfun (Hom Z X) (F @@ Z) (λh. (F ## (z2m h)) |@| x) ≈>
          ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)" 
    proof(rule CompDefinedI, simp_all add: SETmor[THEN sym])
      show "isZFfun (ZFfun (Hom Z X) (F @@ Z) (λh. (F ## (z2m h)) |@| x))" using hHomF by (simp add: SETfun)
      moreover show "isZFfun (ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h))" 
      proof(rule SETfun, rule allI, rule impI)
        fix h assume h: "h |∈| (F @@ Z)"
        have "F ## f maps F @@ Z to F @@ Y" using Ffmaps .
        thus "(F ## f) |@| h |∈| (F @@ Y)" using h by (simp add: SETfunDomAppCod)
      qed
      ultimately show "cod (ZFfun (Hom Z X) (F @@ Z) (λh. (F ## (z2m h)) |@| x)) =
            dom (ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h))" by (simp add: SETcod SETdom)
    qed
    have "ZFfun (Hom Z X) (Hom Y X) (λh. m2z (f ;; (z2m h))) ;;
          ZFfun (Hom Y X) (F @@ Y) (λh. (F ## (z2m h)) |@| x) =
          ZFfun (Hom Z X) (Hom Y X) (λh. m2z (f ;; (z2m h))) |o|
          ZFfun (Hom Y X) (F @@ Y) (λh. (F ## (z2m h)) |@| x)" using Ff compdefa by (simp add: SETComp)
    also have "... = ZFfun (Hom Z X) (F @@ Y) ((λh. (F ## (z2m h)) |@| x) o (λh. m2z (f ;; (z2m h))))"
    proof(rule ZFfunComp, rule allI, rule impI) 
      {
        fix h assume h: "h |∈| (Hom Z X)" 
        show "(m2z (f ;; (z2m h))) |∈| (Hom Y X)" 
        proof-
          have "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)
          hence "(z2m h) maps Z to X" using assms h by (simp add: LSCategory.z2mm2z)
          hence "f ;; (z2m h) maps Y to X" using fmapsb assms(1) by (simp add: Category.Ccompt)
          thus ?thesis using assms by (simp add: LSCategory.m2zz2m)
        qed
      } 
    qed
    also have "... = ZFfun (Hom Z X) (F @@ Y) ((λh. (F ## f) |@| h) o (λh. (F ## (z2m h)) |@| x))"
    proof(rule ZFfun_ext, rule allI, rule impI, simp)
      {
        fix h assume h: "h |∈| (Hom Z X)" 
        have zObj: "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)
        hence hmaps: "(z2m h) maps Z to X" using assms h by (simp add: LSCategory.z2mm2z) 
        hence "(z2m h) ∈ Mor C" and "dom (z2m h) = cod f" using fcod by auto
        hence CompDef_hf: "f ≈> (z2m h)" using fmor by auto
        hence CompDef_hfOp: "(z2m h) ≈> _C f" by (simp add: CompDefOp)
        hence CompDef_FhfOp: "(F ## (z2m h)) ≈> (F ## f)" using assms by (simp add: FunctorCompDef)
        hence "(z2m h) maps _C X to Z" using hmaps by (simp add: MapsToOp) 
        hence "(F ## (z2m h)) maps (F @@ X) to (F @@ Z)" using assms by (simp add: FunctorMapsTo)
        hence xin: "x |∈| |dom|(F ## (z2m h))" using assms by (simp add: SETmapsTo)
        have "(f ;; (z2m h)) ∈ Mor C" using CompDef_hf assms by(simp add: Category.MapsToMorDomCod)
        hence "(F ## (z2m (m2z (f ;; (z2m h))))) |@| x = (F ## (f ;; (z2m h))) |@| x" 
          using assms by (simp add: LSCategory.m2zz2mInv)
        also have "... = (F ## ((z2m h) ;; _C f)) |@| x" by (simp add: OppositeCategory_def)
        also have "... = ((F ## (z2m h)) ;; (F ## f)) |@| x" using assms CompDef_hfOp by (simp add: FunctorComp)
        also have "... = (F ## f) |@| ((F ## (z2m h)) |@| x)" using CompDef_FhfOp xin by(rule SETCompAt)
        finally show "(F ## (z2m (m2z (f ;; (z2m h))))) |@| x = (F ## f) |@| ((F ## (z2m h)) |@| x)" .
      }
    qed
    also have "... = ZFfun (Hom Z X) (F @@ Z) (λh. (F ## (z2m h)) |@| x) |o|
          ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)"
      by(rule ZFfunComp[THEN sym], rule allI, rule impI, simp add: hHomF) 
    also have "... = ZFfun (Hom Z X) (F @@ Z) (λh. (F ## (z2m h)) |@| x) ;; (F ## f)"
      using Ff compdefb by (simp add: SETComp)
    finally show "(((YFtor C) @@ X) ## f) ;; _F ZFfun (Hom Y X) (F @@ Y) (λf. (F ## (z2m f)) |@| x) =
             ZFfun (Hom Z X) (F @@ Z) (λf. (F ## (z2m f)) |@| x) ;; _F (F ## f)"
      by(simp add: cf yf hc fdom fcod HomFtorMapContra_def)
  }
qed

lemma YMapInvNatTrans:
  assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C" and "x |∈| (F @@ X)"
  shows "NatTrans (YMapInv C X F x)"
by (simp add: assms YMapInv_def MakeNT YMapInvNatTransP)

lemma YMapInvImage:
  assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C"
  and "x |∈| (F @@ X)"
  shows "NT (YMapInv C X F x) : (YFtor C @@ X) ==> F"
proof(auto simp only: nt_abbrev_def)
  show "NatTrans (YMapInv C X F x)" using assms by (simp add: YMapInvNatTrans)
  show "NTDom (YMapInv C X F x) = YFtor C @@ X" by(simp add: YMapInv_def MakeNT_def YMapInv'_def)
  show "NTCod (YMapInv C X F x) = F" by(simp add: YMapInv_def MakeNT_def YMapInv'_def)
qed

lemma YMap1:
  assumes LSCat: "LSCategory C" and Fftor: "Ftor F : (Op C) ⟶ SET" and XObj: "X ∈ Obj C"
  and NT: "NT η : (YFtor C @@ X) ==> F"
  shows "YMapInv C X F (YMap C X η) = η"
proof(rule NatTransExt)
  have "(YMap C X η) |∈| (F @@ X)" using assms by (simp add: YMapImage)
  hence 1: "NT (YMapInv C X F (YMap C X η)) : (YFtor C @@ X) ==> F" using assms by (simp add: YMapInvImage)
  thus "NatTrans (YMapInv C X F (YMap C X η))" by auto
  show "NatTrans η" using assms by auto
  have NTDYI: "NTDom (YMapInv C X F (YMap C X η)) = (YFtor C @@ X)" using 1 by auto
  moreover have NTDeta: "NTDom η = (YFtor C @@ X)" using assms by auto
  ultimately show "NTDom (YMapInv C X F (YMap C X η)) = NTDom η" by simp
  have "NTCod (YMapInv C X F (YMap C X η)) = F" using 1 by auto
  moreover have NTCeta: "NTCod η = F" using assms by auto
  ultimately show "NTCod (YMapInv C X F (YMap C X η)) = NTCod η" by simp
  {
    fix Y assume Yobja: "Y ∈ Obj (NTCatDom (YMapInv C X F (YMap C X η)))"
    have CCF: "CatCod F = SET" using assms by auto
    have "Ftor (Hom[←-,X]) : (Op C) ⟶ SET" using LSCat XObj by (simp add: HomFtorContraFtor)
    hence CDH: "CatDom (Hom[←-,X]) = Op C" by auto
    hence CDYF: "CatDom (YFtor C @@ X) = Op C" using XObj LSCat by (auto simp add: YFtorObj)
    hence "NTCatDom (YMapInv C X F (YMap C X η)) = Op C" using LSCat XObj NTDYI CDH  by (simp add: NTCatDom_def)
    hence YObjOp: "Y ∈ Obj (Op C)" using Yobja by simp
    hence YObj: "Y ∈ Obj C" and XObjOp: "X ∈ Obj (Op C)" using XObj by (simp add: OppositeCategory_def)+
    have yinv_mapsTo: "((YMapInv C X F (YMap C X η)) $$ Y) maps (Hom Y X) to (F @@ Y)" 
    proof-
      have "((YMapInv C X F (YMap C X η)) $$ Y) maps ((YFtor C @@ X) @@ Y) to (F @@ Y)" 
        using 1 CCF CDYF YObjOp NatTransMapsTo[of "(YMapInv C X F (YMap C X η))" "(YFtor C @@ X)" F Y] by simp
      thus ?thesis using LSCat XObj YObj by (simp add: YFtorObj2)
    qed
    have eta_mapsTo: "(η $$ Y) maps (Hom Y X) to (F @@ Y)" 
    proof-
      have "(η $$ Y) maps ((YFtor C @@ X) @@ Y) to (F @@ Y)" 
        using NT CDYF CCF YObjOp NatTransMapsTo[of η "(YFtor C @@ X)" F Y] by simp
      thus ?thesis using LSCat XObj YObj by (simp add: YFtorObj2)
    qed
    show "(YMapInv C X F (YMap C X η)) $$ Y = η $$ Y"
    proof(rule ZFfunExt)
      show "|dom|(YMapInv C X F (YMap C X η) $$ Y) = |dom|(η $$ Y)"  
        using yinv_mapsTo eta_mapsTo by (simp add: SETmapsTo)
      show "|cod|(YMapInv C X F (YMap C X η) $$ Y) = |cod|(η $$ Y)" 
        using yinv_mapsTo eta_mapsTo by (simp add: SETmapsTo)
      show "isZFfun (YMapInv C X F (YMap C X η) $$ Y)" 
        using yinv_mapsTo by (simp add: SETmapsTo)
      show "isZFfun (η $$ Y)" 
        using eta_mapsTo by (simp add: SETmapsTo)
      {
        fix f assume fdomYinv: "f |∈| |dom|(YMapInv C X F (YMap C X η) $$ Y)"
        have fHom: "f |∈| (Hom Y X)" using yinv_mapsTo fdomYinv by (simp add: SETmapsTo)
        hence fMapsTo: "(z2m f) maps Y to X" using assms YObj by (simp add: LSCategory.z2mm2z)
        hence fCod: "(cod (z2m f)) = X" and fDom: "(dom (z2m f)) = Y" and fMor: "(z2m f) ∈ Mor C" by auto
        have "(YMapInv C X F (YMap C X η) $$ Y) |@| f =
              (F ## (z2m f)) |@| ((η $$ X) |@| (m2z (Id C X)))" 
          using fHom assms YObj by (simp add: ZFfunApp YMapInvApp YMap_def)
        also have "... = ((η $$ X) ;; (F ## (z2m f))) |@| (m2z (Id C X))" 
        proof-
          have aa: "(η $$ X) maps ((YFtor C @@ X) @@ X) to (F @@ X)" 
            using NT CDYF CCF YObjOp XObjOp NatTransMapsTo[of η "(YFtor C @@ X)" F X] by simp
          have bb: "(F ## (z2m f)) maps (F @@ X) to (F @@ Y)" 
            using fMapsTo Fftor by (simp add: MapsToOp FunctorMapsTo)
          have "(η $$ X) ≈> (F ## (z2m f))" using aa bb by (simp add: MapsToCompDef)
          moreover have "(m2z (Id C X)) |∈| |dom| (η $$ X)" using assms aa 
            by (simp add: SETmapsTo YFtorObj2 Category.Cidm LSCategory.m2zz2m)
          ultimately show ?thesis by (simp add: SETCompAt)
        qed
        also have "... = ((HomC[z2m f,X]) ;; (η $$ Y)) |@| (m2z (Id C X))" 
        proof-
          have "NTDom η = (Hom[←-,X])" using NTDeta assms by (simp add: YFtorObj)
          moreover hence "NTCatDom η = Op C" by (simp add: NTCatDom_def HomFtorContraDom)
          moreover have "NTCatCod η = SET" using assms by (auto simp add: NTCatCod_def)
          moreover have "NatTrans η" and "NTCod η = F" using assms by auto
          moreover have "(z2m f) maps _C X to Y" 
            using fMapsTo MapsToOp[where ?f = "(z2m f)" and ?X = Y and ?Y = X and ?C = C] by simp
          ultimately have "(η $$ X) ;; (F ## (z2m f)) = ((Hom[←-,X]) ## (z2m f)) ;; (η $$ Y)"
            using NatTransP.NatTrans[of η "(z2m f)" X Y] by simp
          moreover have "((Hom[←-,X]) ## (z2m f)) = (HomC[(z2m f),X])" using assms fMor by (simp add: HomContraMor)
          ultimately show ?thesis by simp
        qed
        also have "... = (η $$ Y) |@| ((HomC[z2m f,X]) |@| (m2z (Id C X)))" 
        proof-
          have "(HomC[z2m f,X]) ≈> (η $$ Y)" 
            using fCod fDom XObj LSCat fMor HomFtorContraMapsTo[of C X "z2m f"] eta_mapsTo by (simp add: MapsToCompDef)
          moreover have "|dom| (HomC[z2m f,X]) = (Hom (cod (z2m f)) X)" 
            by (simp add: ZFfunDom HomFtorMapContra_def)
          moreover have "(m2z (Id C X)) |∈| (Hom (cod (z2m f)) X)" 
            using assms fCod by (simp add: Category.Cidm LSCategory.m2zz2m)
          ultimately show ?thesis by (simp add: SETCompAt)
        qed
        also have "... = (η $$ Y) |@| (m2z ((z2m f) ;; (z2m (m2z (Id C X)))))" 
        proof-
          have "(Id C X) maps (cod (z2m f)) to X" using assms fCod by (simp add: Category.Cidm)
          hence "(m2z (Id C X)) |∈| (Hom (cod (z2m f)) X)" using assms by (simp add: LSCategory.m2zz2m)
          thus ?thesis by (simp add: HomContraAt)
        qed
        also have "... = (η $$ Y) |@| (m2z ((z2m f) ;; (Id C X)))" 
          using assms by (simp add: LSCategory.m2zz2mInv Category.CatIdInMor)
        also have "... = (η $$ Y) |@| (m2z (z2m f))" using assms(1) fCod fMor Category.Cidr[of C "(z2m f)"] by (simp)
        also have "... = (η $$ Y) |@| f" using assms YObj fHom by (simp add: LSCategory.z2mm2z)
        finally show "(YMapInv C X F (YMap C X η) $$ Y) |@| f = (η $$ Y) |@| f" .
      }
    qed
  }
qed

lemma YMap2:
  assumes "LSCategory C" and "Ftor F : (Op C) ⟶ SET" and "X ∈ Obj C"
  and "x |∈| (F @@ X)"
  shows "YMap C X (YMapInv C X F x) = x"
proof(simp only: YMap_def)
  let ?η = "(YMapInv C X F x)"
  have "(?η $$ X) = ZFfun (Hom X X) (F @@ X) (λ f . (F ## (z2m f)) |@| x)" using assms by (simp add: YMapInvApp)
  moreover have "(m2z (Id C X)) |∈| (Hom X X)" using assms by (simp add: Category.Simps LSCategory.m2zz2m)
  ultimately have "(?η $$ X) |@| (m2z (Id C X)) = (F ## (z2m (m2z (Id C X)))) |@| x" 
    by (simp add: ZFfunApp)
  also have "... = (F ## (Id C X)) |@| x" using assms by (simp add: Category.CatIdInMor LSCategory.m2zz2mInv)
  also have "... = (Id SET (F @@ X)) |@| x" 
  proof-
    have "X ∈ Obj (Op C)" using assms by (auto simp add: OppositeCategory_def)
    hence "(F ## (Id (Op C) X)) = (Id SET (F @@ X))" 
      using assms by(simp add: FunctorId)
    moreover have "(Id (Op C) X) = (Id C X)" using assms by (auto simp add: OppositeCategory_def)
    ultimately show ?thesis by simp
  qed
  also have "... = x" using assms by (simp add: SETId)
  finally show "(?η $$ X) |@| (m2z (Id C X)) = x" .
qed

lemma YFtorNT_YMapInv:
  assumes "LSCategory C" and "f maps X to Y"
  shows "YFtorNT C f = YMapInv C X (Hom[←-,Y]) (m2z f)"
proof(simp only: YFtorNT_def YMapInv_def, rule NatTransExt')
  have Cf: "cod f = Y" and Df: "dom f = X" using assms by auto
  thus "NTCod (YFtorNT' C f) = NTCod (YMapInv' C X (Hom[←-,Y]) (m2zf))"
    by(simp add: YFtorNT'_def YMapInv'_def )
  have "Hom[←-,dom f] = YFtor C @@ X" using Df assms by (simp add: YFtorObj Category.MapsToObj)
  thus "NTDom (YFtorNT' C f) = NTDom (YMapInv' C X (Hom[←-,Y]) (m2zf))"
    by(simp add: YFtorNT'_def YMapInv'_def )
  {
    fix Z assume ObjZ1: "Z ∈ Obj (NTCatDom (YFtorNT' C f))"
    have ObjZ2: "Z ∈ Obj C" using ObjZ1 by (simp add: YFtorNT'_def NTCatDom_def OppositeCategory_def HomFtorContraDom) 
    moreover have ObjX: "X ∈ Obj C" and ObjY: "Y ∈ Obj C" using assms by (simp add: Category.MapsToObj)+
    moreover 
    {
      fix x assume x: "x |∈| (Hom Z X)"
      have "m2z ((z2m x) ;; f) = ((Hom[←-,Y]) ## (z2m x)) |@| (m2zf)"
      proof-
        have morf: "f ∈ Mor C" using assms by auto
        have mapsx: "(z2m x) maps Z to X" using x assms(1) ObjZ2 ObjX by (simp add: LSCategory.z2mm2z)
        hence morx: "(z2m x) ∈ Mor C" by auto
        hence "(Hom[←-,Y]) ## (z2m x) = (HomC[(z2m x),Y])" using assms by (simp add: HomContraMor)
        moreover have "(HomC[(z2m x),Y]) |@| (m2z f) = m2z ((z2m x) ;; (z2m (m2z f)))"
        proof (rule HomContraAt)
          have "cod (z2m x) = X" using mapsx by auto
          thus "(m2z f) |∈| (Hom (cod (z2m x)) Y)" using assms by (simp add: LSCategory.m2zz2m)
        qed
        moreover have "(z2m (m2z f)) = f" using assms morf by (simp add: LSCategory.m2zz2mInv) 
        ultimately show ?thesis by simp
      qed
    }
    ultimately show "(YFtorNT' C f) $$ Z = (YMapInv' C X (Hom[←-,Y]) (m2zf)) $$ Z" using Cf Df assms
      apply(simp add: YFtorNT'_def YMapInv'_def HomFtorMap_def HomFtorOpObj)
      apply(rule ZFfun_ext, rule allI, rule impI, simp)
      done
  }
qed

lemma YMapYoneda:
  assumes "LSCategory C" and "f maps X to Y"
  shows "YFtor C ## f = YMapInv C X (YFtor C @@ Y) (m2z f)"
proof-
  have "f ∈ Mor C" using assms by auto
  moreover have "Y ∈ Obj C" using assms by (simp add: Category.MapsToObj)
  moreover have "YFtorNT C f = YMapInv C X (Hom[←-,Y]) (m2z f)" using assms by (simp add: YFtorNT_YMapInv)
  ultimately show ?thesis using assms by (simp add: YFtorMor YFtorObj)
qed

lemma YonedaFull: 
  assumes "LSCategory C" and "X ∈ Obj C" and "Y ∈ Obj C"
  and "NT η : (YFtor C @@ X) ==> (YFtor C @@ Y)"
  shows "YFtor C ## (z2m (YMap C X η)) = η"
  and "z2m (YMap C X η) maps X to Y"
proof-
  have ftor: "Ftor (YFtor C @@ Y) : (Op C) ⟶ SET" using assms by (simp add: YFtorObj HomFtorContraFtor)
  hence "(YMap C X η) |∈| ((YFtor C @@ Y) @@ X)" using assms by (simp add: YMapImage)
  hence yh: "(YMap C X η) |∈| (Hom X Y)" using assms by (simp add: YFtorObj2)
  thus "(z2m (YMap C X η)) maps X to Y" using assms by (simp add: LSCategory.z2mm2z)
  hence "YFtor C ## (z2m (YMap C X η)) = YMapInv C X (YFtor C @@ Y) (m2z (z2m (YMap C X η)))"
    using assms yh by (simp add: YMapYoneda)
  also have "... = YMapInv C X (YFtor C @@ Y) (YMap C X η)" 
    using assms yh by (simp add: LSCategory.z2mm2z)
  finally show "YFtor C ## (z2m (YMap C X η)) = η" using assms ftor by (simp add: YMap1)
qed

lemma YonedaFaithful:
  assumes "LSCategory C" and "f maps X to Y" and "g maps X to Y"
  and "YFtor C ## f = YFtor C ## g"
  shows "f = g"
proof-
  have ObjX: "X ∈ Obj C" and ObjY: "Y ∈ Obj C" using assms by (simp add: Category.MapsToObj)+
  have M2Zf: "(m2z f) |∈| ((YFtor C @@ Y) @@ X)" and M2Zg: "(m2z g) |∈| ((YFtor C @@ Y) @@ X)"
    using assms ObjX ObjY by (simp add: LSCategory.m2zz2m YFtorObj2)+
  have Ftor: "Ftor (YFtor C @@ Y) : (Op C) ⟶ SET" using assms ObjY by (simp add: YFtorObj HomFtorContraFtor)
  have Morf: "f ∈ Mor C" and Morg: "g ∈ Mor C" using assms by auto
  have "YMapInv C X (YFtor C @@ Y) (m2z f) = YMapInv C X (YFtor C @@ Y) (m2z g)"
    using assms by (simp add: YMapYoneda)
  hence "YMap C X (YMapInv C X (YFtor C @@ Y) (m2z f)) = YMap C X (YMapInv C X (YFtor C @@ Y) (m2z g))"
    by simp
  hence "(m2z f) = (m2z g)" using assms ObjX ObjY M2Zf M2Zg Ftor by (simp add: YMap2)
  thus "f = g" using assms Morf Morg by (simp add: LSCategory.mor2ZFInj)
qed

lemma YonedaEmbedding:
  assumes "LSCategory C" and "A ∈ Obj C" and "B ∈ Obj C" and "(YFtor C) @@ A = (YFtor C) @@ B"
  shows "A = B"
proof-
  have AObjOp: "A ∈ Obj (Op C)" and BObjOp: "B ∈ Obj (Op C)" using assms by (simp add: OppositeCategory_def)+
  hence FtorA: "Ftor (Hom[←-,A]) : (Op C) ⟶ SET" and FtorB: "Ftor (Hom[←-,B]) : (Op C) ⟶ SET" 
    using assms by (simp add: HomFtorContraFtor)+
  have "Hom[←-,A] = Hom[←-,B]" using assms by (simp add: YFtorObj)
  hence "(Hom[←-,A]) ## (Id (Op C) A) = (Hom[←-,B]) ## (Id (Op C) A)" by simp
  hence "Id SET ((Hom[←-,A]) @@ A) = Id SET ((Hom[←-,B]) @@ A)" 
    using AObjOp BObjOp FtorA FtorB by (simp add: FunctorId)
  hence "Id SET (Hom A A) = Id SET (Hom A B)" using assms by (simp add: HomFtorOpObj)
  hence "Hom A A = Hom A B" using SETCategory by (simp add: Category.IdInj SETobj[of "Hom A A"] SETobj[of "Hom A B"])
  moreover have "(m2z (Id C A)) |∈| (Hom A A)" using assms by (simp add: Category.Cidm LSCategory.m2zz2m)
  ultimately have "(m2z (Id C A)) |∈| (Hom A B)" by simp
  hence "(z2m (m2z (Id C A))) maps A to B" using assms by (simp add: LSCategory.z2mm2z)
  hence "(Id C A) maps A to B" using assms by (simp add: Category.CatIdInMor LSCategory.m2zz2mInv)
  hence "cod (Id C A) = B" by auto
  thus ?thesis using assms by (simp add: Category.CatIdDomCod)
qed

end