Theory Yoneda

(*
Author: Alexander Katovsky
*)

header "Yoneda"

theory Yoneda
imports NatTrans SetCat
begin

definition "YFtorNT' C f ≡ (|NTDom = Hom⇘C⇙[\<emdash>,dom⇘C⇙ f] , NTCod = Hom⇘C⇙[\<emdash>,cod⇘C⇙ f] ,
                       NatTransMap = λ B . Hom⇘C⇙[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⇘C⇙[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⇘NTCatCod (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⇘C⇙[\<emdash>,dom⇘C⇙ f]) @@ X = Hom⇘C ⇙X dom⇘C⇙ f " using assms Obj by(simp add: HomFtorOpObj Category.Cdom)
      have H2: "(Hom⇘C⇙[\<emdash>,cod⇘C⇙ f]) @@ X = Hom⇘C ⇙X cod⇘C⇙ f " using assms Obj by(simp add: HomFtorOpObj Category.Ccod)
      have "Hom⇘C⇙[X,f] maps⇘SET⇙ (Hom⇘C ⇙X dom⇘C⇙ f) to (Hom⇘C ⇙X cod⇘C⇙ 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⇘NTCatDom (YFtorNT' C f)⇙ X to Y"
    show "((NTDom (YFtorNT' C f)) ## g) ;;⇘NTCatCod (YFtorNT' C f) ⇙(YFtorNT' C f $$ Y) =
       ((YFtorNT' C f) $$ X) ;;⇘NTCatCod (YFtorNT' C f) ⇙(NTCod (YFtorNT' C f) ## g)"
    proof-
      have M1: "g maps⇘Op C⇙ X to Y" using a by (auto simp add: NTCatDom_def YFtorNT'_def HomFtorContraDom)
      have D1: "dom⇘C⇙ g = Y" and C1: "cod⇘C⇙ 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⇘C⇙[g,dom⇘C⇙ f]) = (Hom⇘C⇙[\<emdash>,dom⇘C⇙ f]) ## g" 
        and H2: "(HomC⇘C⇙[g,cod⇘C⇙ f]) = (Hom⇘C⇙[\<emdash>,cod⇘C⇙ f]) ## g" using M1 
        by (auto simp add: HomFtorContra_def HomFtorContra'_def MakeFtor_def)
      have "(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])" using assms morf morg
        by (simp add: HomCHom)
      hence "((Hom⇘C⇙[\<emdash>,dom⇘C⇙ f]) ## g) ;;⇘SET⇙ (Hom⇘C⇙[Y,f]) = (Hom⇘C⇙[X,f]) ;;⇘SET⇙ ((Hom⇘C⇙[\<emdash>,cod⇘C⇙ 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⇘CatExp (Op C) SET⇙ (Hom⇘C⇙[\<emdash>,dom⇘C⇙ f]) to (Hom⇘C⇙[\<emdash>,cod⇘C⇙ f])"
proof(rule MapsToI)
  have "f ∈ Mor C"  using assms by auto
  thus 1: "YFtorNT C f ∈ mor⇘CatExp (Op C) SET⇙" using assms by (simp add: YFtorNTMor)
  show "dom⇘CatExp (Op C) SET⇙ YFtorNT C f = Hom⇘C⇙[\<emdash>,dom⇘C⇙ f]" using 1 by(simp add:CatExpDom YFtorNT_defs)
  show "cod⇘CatExp (Op C) SET⇙ YFtorNT C f = Hom⇘C⇙[\<emdash>,cod⇘C⇙ f]" using 1 by(simp add:CatExpCod YFtorNT_defs)
qed

lemma YFtorNTCompDef:
  assumes "LSCategory C" and "f ≈>⇘C⇙ g"
  shows "YFtorNT C f ≈>⇘CatExp (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⇘CatExp (Op C) SET⇙ (Hom⇘C⇙[\<emdash>,dom⇘C⇙ f]) to (Hom⇘C⇙[\<emdash>,cod⇘C⇙ f])"
    and 2: "YFtorNT C g maps⇘CatExp (Op C) SET⇙ (Hom⇘C⇙[\<emdash>,dom⇘C⇙ g]) to (Hom⇘C⇙[\<emdash>,cod⇘C⇙ g])"
    using assms by (simp add: YFtorNtMapsTo)+
  thus "YFtorNT C f ∈ mor⇘CatExp (Op C) SET⇙"
    and "YFtorNT C g ∈ mor⇘CatExp (Op C) SET⇙" by auto
  have "cod⇘CatExp (Op C) SET⇙ YFtorNT C f = (Hom⇘C⇙[\<emdash>,cod⇘C⇙ f])" using 1 by auto
  moreover have "dom⇘CatExp (Op C) SET⇙ YFtorNT C g = (Hom⇘C⇙[\<emdash>,dom⇘C⇙ g])" using 2 by auto
  moreover have "cod⇘C⇙ f = dom⇘C⇙ g" using assms by auto
  ultimately show "cod⇘CatExp (Op C) SET⇙ YFtorNT C f = dom⇘CatExp (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⇘C ⇙[\<emdash>,X])"
proof(simp add: YFtor'_def, rule NatTransExt)
  have Obj: "X ∈ Obj C" using assms by (simp add: YFtor'_def)
  have HomObj: "(Hom⇘C⇙[\<emdash>,X]) ∈ Obj (CatExp (Op C) SET)" using assms Obj by(simp add: CatExp_defs HomFtorContraFtor)
  hence Id: "Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,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⇘C⇙[\<emdash>,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⇘C⇙[\<emdash>,X]))" using Id by (simp add: CatExp_defs)
  show "NTDom (YFtorNT C (Id C X)) = NTDom (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))"
  proof(simp add: YFtorNT_defs)
    have "Hom⇘C⇙[\<emdash>,dom⇘C⇙ (Id C X)] = Hom⇘C⇙[\<emdash>,X]" using assms Obj by (simp add: Category.CatIdDomCod)
    also have "... = dom⇘CatExp (Op C) SET⇙  (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))" using CAT HomObj
      by (simp add: Category.CatIdDomCod)
    also have "... = NTDom (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))" using Id by (simp add: CatExpDom)
    finally show "Hom⇘C⇙[\<emdash>,dom⇘C⇙ (Id C X)] = NTDom (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))" .
  qed
  show "NTCod (YFtorNT C (Id C X)) = NTCod (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))"
  proof(simp add: YFtorNT_defs)
    have "Hom⇘C⇙[\<emdash>,cod⇘C⇙ (Id C X)] = Hom⇘C⇙[\<emdash>,X]" using assms Obj by (simp add: Category.CatIdDomCod)
    also have "... = cod⇘CatExp (Op C) SET⇙  (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))" using CAT HomObj
      by (simp add: Category.CatIdDomCod)
    also have "... = NTCod (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,X]))" using Id by (simp add: CatExpCod)
    finally show "Hom⇘C⇙[\<emdash>,cod⇘C⇙ (Id C X)] = NTCod (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,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⇘C⇙[\<emdash>,X])) $$ Y"
    proof-
      have CD: "CatDom (Hom⇘C⇙[\<emdash>,X]) = Op C" by (simp add: HomFtorContraDom)
      have CC: "CatCod (Hom⇘C⇙[\<emdash>,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⇘C⇙[Y,(Id C X)])" using a by (simp add: YFtorNTApp1)
      also have "... = id⇘SET⇙ (Hom⇘C ⇙Y X)" using Obj ObjY assms by (simp add: HomFtorId)
      also have "... = id⇘SET⇙ ((Hom⇘C⇙[\<emdash>,X]) @@ Y)" using Obj ObjY assms by (simp add: HomFtorOpObj )
      also have "... = (IdNatTrans (Hom⇘C⇙[\<emdash>,X])) $$ Y" using CD CC ObjYOp by (simp add: IdNatTrans_map)
      also have "... = (Id (CatExp (Op C) SET) (Hom⇘C⇙[\<emdash>,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 ≈>⇘CatDom (YFtor' C)⇙ g"
    show "(YFtor' C) ## (f ;;⇘CatDom (YFtor' C)⇙ g) = ((YFtor' C) ## f) ;;⇘CatCod (YFtor' C)⇙ ((YFtor' C) ## g)" 
    proof(simp add: YFtor'_def, rule NatTransExt)
      have CD: "f ≈>⇘C⇙ g" using a by (simp add: YFtor'_def)
      have CD2: "YFtorNT C f ≈>⇘CatExp (Op C) SET⇙ YFtorNT C g" using CD assms by (simp add: YFtorNTCompDef)
      have Mor1: "YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g ∈ Mor (CatExp (Op C) SET)" using CAT CD2
        by (simp add: Category.MapsToMorDomCod)
      show "NatTrans (YFtorNT C (f ;;⇘C⇙ g))" using assms by (simp add: Category.MapsToMorDomCod CD YFtorNTNatTrans)
      show "NatTrans (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)" using Mor1 by (simp add: CatExpMorNT)
      show "NTDom (YFtorNT C (f ;;⇘C⇙ g)) = NTDom (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)"
      proof-
        have 1: "YFtorNT C f ∈ mor⇘CatExp (Op C) SET⇙" using CD2 by auto
        have "NTDom (YFtorNT C (f ;;⇘C⇙ g)) = Hom⇘C⇙[\<emdash>,dom⇘C⇙ (f ;;⇘C⇙ g)]" by (simp add: YFtorNT_defs)
        also have "... = Hom⇘C⇙[\<emdash>,dom⇘C⇙ f]" using CD assms by (simp add: Category.MapsToMorDomCod)
        also have "... = NTDom (YFtorNT C f)" by (simp add: YFtorNT_defs)
        also have "... = dom⇘CatExp (Op C) SET⇙ (YFtorNT C f)" using 1 by (simp add: CatExpDom)
        also have "... = dom⇘CatExp (Op C) SET⇙ (YFtorNT C f ;;⇘CatExp (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 ;;⇘C⇙ g)) = NTCod (YFtorNT C f ;;⇘CatExp (Op C) SET⇙ YFtorNT C g)"
      proof-
        have 1: "YFtorNT C g ∈ mor⇘CatExp (Op C) SET⇙" using CD2 by auto
        have "NTCod (YFtorNT C (f ;;⇘C⇙ g)) = Hom⇘C⇙[\<emdash>,cod⇘C⇙ (f ;;⇘C⇙ g)]" by (simp add: YFtorNT_defs)
        also have "... = Hom⇘C⇙[\<emdash>,cod⇘C⇙ g]" using CD assms by (simp add: Category.MapsToMorDomCod)
        also have "... = NTCod (YFtorNT C g)" by (simp add: YFtorNT_defs)
        also have "... = cod⇘CatExp (Op C) SET⇙ (YFtorNT C g)" using 1 by (simp add: CatExpCod)
        also have "... = cod⇘CatExp (Op C) SET⇙ (YFtorNT C f ;;⇘CatExp (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 ;;⇘C⇙ g)))"
        show "YFtorNT C (f ;;⇘C⇙ g) $$ X = (YFtorNT C f ;;⇘CatExp (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⇘C⇙[X,f]) = (YFtorNT C f) $$ X" 
            and App2: "(Hom⇘C⇙[X,g]) = (YFtorNT C g) $$ X" using a by (simp add: YFtorNTApp1 YFtorNTCatDom)+
          have "(YFtorNT C (f ;;⇘C⇙ g)) $$ X = (Hom⇘C⇙[X,(f ;;⇘C⇙ g)])" using a by (simp add: YFtorNTApp1)
          also have "... = (Hom⇘C⇙[X,f]) ;;⇘SET⇙ (Hom⇘C⇙[X,g])" using CD assms Obj by (simp add: HomFtorDist)
          also have "... = ((YFtorNT C f) $$ X) ;;⇘SET⇙ ((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⇘C ⇙[\<emdash>,X]" in Set.rev_bexI)
      have "X ∈ Obj C" using a by(simp add: YFtor'_def)
      thus "Hom⇘C ⇙[\<emdash>,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⇘C ⇙[\<emdash>,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⇘C ⇙[\<emdash>,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⇘C ⇙[\<emdash>,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⇘CatDom (YFtor' C) ⇙X to Y"
      show "YFtor' C ## f maps⇘CatCod (YFtor' C)⇙ YFtor' C @@ X to YFtor' C @@ Y"
      proof-
        have Mor1: "f maps⇘C⇙ 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⇘C ⇙[\<emdash>,X]" 
          and "YFtor' C @@ Y = Hom⇘C ⇙[\<emdash>,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⇘CatExp (Op C) SET⇙ (Hom⇘C ⇙[\<emdash>,X]) to (Hom⇘C ⇙[\<emdash>,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⇘C ⇙[\<emdash>,X]"
proof-
  have "CatDom (YFtor' C) = C" by (simp add: YFtor'_def)
  moreover hence "(YFtor' C) @@ X = Hom⇘C ⇙[\<emdash>,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⇘C ⇙X Y"
proof-
  have "Hom⇘C ⇙X Y = ((Hom⇘C⇙[\<emdash>,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 ≡ Hom⇘CatExp (Op C) SET⇙ F G"
*)

definition "YMap C X η ≡ (η $$ X) |@| (m2z⇘C⇙ (id⇘C ⇙X))"
definition "YMapInv' C X F x ≡ (|
      NTDom = ((YFtor C) @@ X), 
      NTCod = F, 
      NatTransMap = λ B . ZFfun (Hom⇘C⇙ B X) (F @@ B) (λ f . (F ## (z2m⇘C⇙ 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⇘C⇙ B X) (F @@ B) (λ f . (F ## (z2m⇘C⇙ 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⇘C⇙[\<emdash>,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⇘C⇙[\<emdash>,X])" using assms by (auto simp add: YFtorObj)
  moreover have "Ftor (Hom⇘C⇙[\<emdash>,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⇘CatCod F ⇙((YFtor C @@ X) @@ X) to (F @@ X)" using assms Obj by (simp add: NatTransMapsTo) 
  ultimately have "η $$ X maps⇘SET⇙ ((YFtor C @@ X) @@ X) to (F @@ X)" by simp 
  moreover have "(m2z⇘C ⇙(Id C X))  |∈| ((YFtor C @@ X) @@ X)" 
  proof-
    have "(Id C X) maps⇘C ⇙X to X" using assms by (simp add: Category.Simps)
    moreover have "((YFtor C @@ X) @@ X) = Hom⇘C⇙ X X" using assms by (simp add: YFtorObj2)
    ultimately show ?thesis using assms by (simp add: LSCategory.m2zz2m)
  qed
  ultimately show "((η $$ X) |@| (m2z⇘C ⇙(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⇘C⇙[\<emdash>,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⇘C⇙ Y X) (F @@ Y) (λf. (F ## (z2m⇘C ⇙f)) |@| x) maps⇘CatCod 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⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x))" 
      proof(rule SETfun, rule allI, rule impI)
        {
          fix y assume yhom: "y |∈| (Hom⇘C⇙ Y X)" show "(F ## (z2m⇘C ⇙y)) |@| x |∈| (F @@ Y)"
          proof-
            let ?f = "(F ## (z2m⇘C ⇙y))"
            have "(z2m⇘C ⇙y) maps⇘C⇙ Y to X" using yhom yobj assms by (simp add: LSCategory.z2mm2z)
            hence "(z2m⇘C ⇙y) maps⇘Op C⇙ X to Y" by (simp add: MapsToOp)
            hence "?f maps⇘SET⇙ (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⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x) ∈ mor⇘SET⇙" using zffun
        by(simp add: SETmor)
      show "cod⇘SET⇙ ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x) = F @@ Y" using zffun
        by(simp add: SETcod)
      have "(Hom⇘C⇙ Y X) = (YFtor C @@ X) @@ Y" using assms yobj by (simp add: YFtorObj2)
      thus "dom⇘SET⇙ ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## z2m⇘C⇙f) |@| x) = (YFtor C @@ X) @@ Y" using zffun
        by(simp add: SETdom)
    qed
  }
  {
    fix f Z Y assume fmaps: "f maps⇘CatDom ((YFtor C ) @@ X)⇙ Z to Y" 
    have fmapsa: "f maps⇘Op C⇙ Z to Y" using fmaps dy by simp
    hence fmapsb: "f maps⇘C⇙ Y to Z" by (rule MapsToOpOp)
    hence fmor: "f ∈ Mor C" and fdom: "dom⇘C⇙ f = Y" and fcod: "cod⇘C⇙ f = Z" by (auto simp add: OppositeCategory_def)
    hence hc: "(Hom⇘C⇙[\<emdash>,X]) ## f = (HomC⇘C⇙[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⇘SET⇙ (F @@ Z) to (F @@ Y)" using assms fmapsa by (simp add: FunctorMapsTo)
    have Fzmaps: "!! h A B . [|h |∈| (Hom⇘C⇙ A B) ; A ∈ Obj C ; B ∈ Obj C|] ==> 
      (F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ B) to (F @@ A)"
    proof-
      fix h A B assume h: "h |∈| (Hom⇘C⇙ A B)" and oA: "A ∈ Obj C" and oB: "B ∈ Obj C"  
      have "(z2m⇘C ⇙h) maps⇘C⇙ A to B" using assms h oA oB by (simp add: LSCategory.z2mm2z)
      hence "(z2m⇘C ⇙h) maps⇘Op C⇙ B to A" by (rule MapsToOp)
      thus "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ B) to (F @@ A)" using assms by (simp add: FunctorMapsTo)
    qed
    have hHomF: "!!h. h |∈| (Hom⇘C⇙ Z X) ==> (F ## (z2m⇘C ⇙h)) |@| x |∈| (F @@ Z)" using xobj zobj xinF
    proof-
      fix h assume h: "h |∈| (Hom⇘C⇙ Z X)"
      have "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ X) to (F @@ Z)" using xobj zobj h by (simp add: Fzmaps)
      thus "(F ## (z2m⇘C ⇙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⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) ≈>⇘SET⇙ 
          ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x)" 
    proof(rule CompDefinedI, simp_all add: SETmor[THEN sym])
      show "isZFfun (ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))"
      proof(rule SETfun, rule allI, rule impI)
        fix h assume h: "h |∈| (Hom⇘C⇙ Z X)"
        have "(z2m⇘C ⇙h) maps⇘C⇙ Z to X" using assms h xobj zobj by (simp add: LSCategory.z2mm2z)
        hence "f ;;⇘C⇙ (z2m⇘C ⇙h) maps⇘C⇙ Y to X" using fmapsb assms(1) by (simp add: Category.Ccompt)
        thus "(m2z⇘C⇙ (f ;;⇘C⇙ (z2m⇘C ⇙h))) |∈| (Hom⇘C⇙ Y X)" using assms by (simp add: LSCategory.m2zz2m)
      qed
      moreover show "isZFfun (ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x))" 
      proof(rule SETfun, rule allI, rule impI)
        fix h assume h: "h |∈| (Hom⇘C⇙ Y X)"
        have "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ X) to (F @@ Y)" using xobj yobj h by (simp add: Fzmaps)
        thus "(F ## (z2m⇘C ⇙h)) |@| x |∈| (F @@ Y)" using assms by (simp add: SETfunDomAppCod)
      qed
      ultimately show "cod⇘SET⇙(ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h)))) = 
        dom⇘SET⇙(ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x))" by (simp add: SETcod SETdom)
    qed      
    have compdefb: "ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x) ≈>⇘SET⇙ 
          ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h)" 
    proof(rule CompDefinedI, simp_all add: SETmor[THEN sym])
      show "isZFfun (ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙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⇘SET⇙ F @@ Z to F @@ Y" using Ffmaps .
        thus "(F ## f) |@| h |∈| (F @@ Y)" using h by (simp add: SETfunDomAppCod)
      qed
      ultimately show "cod⇘SET⇙ (ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x)) = 
            dom⇘SET⇙ (ZFfun (F @@ Z) (F @@ Y) (λh. (F ## f) |@| h))" by (simp add: SETcod SETdom)
    qed
    have "ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) ;;⇘SET⇙ 
          ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x) = 
          ZFfun (Hom⇘C⇙ Z X) (Hom⇘C⇙ Y X) (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) |o| 
          ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λh. (F ## (z2m⇘C ⇙h)) |@| x)" using Ff compdefa by (simp add: SETComp)
    also have "... = ZFfun (Hom⇘C⇙ Z X) (F @@ Y) ((λh. (F ## (z2m⇘C ⇙h)) |@| x) o (λh. m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))"
    proof(rule ZFfunComp, rule allI, rule impI) 
      {
        fix h assume h: "h |∈| (Hom⇘C⇙ Z X)" 
        show "(m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))) |∈| (Hom⇘C⇙ Y X)" 
        proof-
          have "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)
          hence "(z2m⇘C ⇙h) maps⇘C⇙ Z to X" using assms h by (simp add: LSCategory.z2mm2z)
          hence "f ;;⇘C⇙ (z2m⇘C ⇙h) maps⇘C⇙ 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⇘C⇙ Z X) (F @@ Y) ((λh. (F ## f) |@| h) o (λh. (F ## (z2m⇘C ⇙h)) |@| x))"
    proof(rule ZFfun_ext, rule allI, rule impI, simp)
      {
        fix h assume h: "h |∈| (Hom⇘C⇙ Z X)" 
        have zObj: "Z ∈ Obj C" using fmapsb assms by (simp add: Category.MapsToObj)
        hence hmaps: "(z2m⇘C ⇙h) maps⇘C⇙ Z to X" using assms h by (simp add: LSCategory.z2mm2z) 
        hence "(z2m⇘C ⇙h) ∈ Mor C" and "dom⇘C⇙ (z2m⇘C ⇙h) = cod⇘C⇙ f" using fcod by auto
        hence CompDef_hf: "f ≈>⇘C⇙ (z2m⇘C ⇙h)" using fmor by auto
        hence CompDef_hfOp: "(z2m⇘C ⇙h) ≈>⇘Op C⇙ f" by (simp add: CompDefOp)
        hence CompDef_FhfOp: "(F ## (z2m⇘C ⇙h)) ≈>⇘SET⇙ (F ## f)" using assms by (simp add: FunctorCompDef)
        hence "(z2m⇘C ⇙h) maps⇘Op C⇙ X to Z" using hmaps by (simp add: MapsToOp) 
        hence "(F ## (z2m⇘C ⇙h)) maps⇘SET⇙ (F @@ X) to (F @@ Z)" using assms by (simp add: FunctorMapsTo)
        hence xin: "x |∈| |dom|(F ## (z2m⇘C ⇙h))" using assms by (simp add: SETmapsTo)
        have "(f ;;⇘C⇙ (z2m⇘C ⇙h)) ∈ Mor C" using CompDef_hf assms by(simp add: Category.MapsToMorDomCod)
        hence "(F ## (z2m⇘C ⇙(m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))) |@| x = (F ## (f ;;⇘C⇙ (z2m⇘C ⇙h))) |@| x" 
          using assms by (simp add: LSCategory.m2zz2mInv)
        also have "... = (F ## ((z2m⇘C ⇙h) ;;⇘Op C⇙ f)) |@| x" by (simp add: OppositeCategory_def)
        also have "... = ((F ## (z2m⇘C ⇙h)) ;;⇘SET ⇙(F ## f)) |@| x" using assms CompDef_hfOp by (simp add: FunctorComp)
        also have "... = (F ## f) |@| ((F ## (z2m⇘C ⇙h)) |@| x)" using CompDef_FhfOp xin by(rule SETCompAt)
        finally show "(F ## (z2m⇘C ⇙(m2z⇘C ⇙(f ;;⇘C⇙ (z2m⇘C ⇙h))))) |@| x = (F ## f) |@| ((F ## (z2m⇘C ⇙h)) |@| x)" .
      }
    qed
    also have "... = ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙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⇘C⇙ Z X) (F @@ Z) (λh. (F ## (z2m⇘C ⇙h)) |@| x) ;;⇘SET⇙ (F ## f)"
      using Ff compdefb by (simp add: SETComp)
    finally show "(((YFtor C) @@ X) ## f) ;;⇘CatCod F⇙ ZFfun (Hom⇘C⇙ Y X) (F @@ Y) (λf. (F ## (z2m⇘C ⇙f)) |@| x) =
             ZFfun (Hom⇘C⇙ Z X) (F @@ Z) (λf. (F ## (z2m⇘C ⇙f)) |@| x) ;;⇘CatCod 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⇘C⇙[\<emdash>,X]) : (Op C) --> SET" using LSCat XObj by (simp add: HomFtorContraFtor)
    hence CDH: "CatDom (Hom⇘C⇙[\<emdash>,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⇘SET⇙ (Hom⇘C ⇙Y X) to (F @@ Y)" 
    proof-
      have "((YMapInv C X F (YMap C X η)) $$ Y) maps⇘SET⇙ ((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⇘SET⇙ (Hom⇘C ⇙Y X) to (F @@ Y)" 
    proof-
      have "(η $$ Y) maps⇘SET⇙ ((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⇘C⇙ Y X)" using yinv_mapsTo fdomYinv by (simp add: SETmapsTo)
        hence fMapsTo: "(z2m⇘C ⇙f) maps⇘C ⇙Y to X" using assms YObj by (simp add: LSCategory.z2mm2z)
        hence fCod: "(cod⇘C⇙ (z2m⇘C ⇙f)) = X" and fDom: "(dom⇘C⇙ (z2m⇘C ⇙f)) = Y" and fMor: "(z2m⇘C ⇙f) ∈ Mor C" by auto
        have "(YMapInv C X F (YMap C X η) $$ Y) |@| f = 
              (F ## (z2m⇘C ⇙f)) |@| ((η $$ X) |@| (m2z⇘C ⇙(Id C X)))" 
          using fHom assms YObj by (simp add: ZFfunApp YMapInvApp YMap_def)
        also have "... = ((η $$ X) ;;⇘SET⇙ (F ## (z2m⇘C ⇙f))) |@| (m2z⇘C ⇙(Id C X))" 
        proof-
          have aa: "(η $$ X) maps⇘SET⇙ ((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⇘C ⇙f)) maps⇘SET⇙ (F @@ X) to (F @@ Y)" 
            using fMapsTo Fftor by (simp add: MapsToOp FunctorMapsTo)
          have "(η $$ X) ≈>⇘SET⇙ (F ## (z2m⇘C ⇙f))" using aa bb by (simp add: MapsToCompDef)
          moreover have "(m2z⇘C ⇙(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⇘C⇙[z2m⇘C ⇙f,X]) ;;⇘SET⇙ (η $$ Y)) |@| (m2z⇘C ⇙(Id C X))" 
        proof-
          have "NTDom η = (Hom⇘C⇙[\<emdash>,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⇘C ⇙f) maps⇘Op C ⇙X to Y" 
            using fMapsTo MapsToOp[where ?f = "(z2m⇘C ⇙f)" and ?X = Y and ?Y = X and ?C = C] by simp
          ultimately have "(η $$ X) ;;⇘SET⇙ (F ## (z2m⇘C ⇙f)) = ((Hom⇘C⇙[\<emdash>,X]) ## (z2m⇘C ⇙f)) ;;⇘SET⇙ (η $$ Y)"
            using NatTransP.NatTrans[of η "(z2m⇘C ⇙f)" X Y] by simp
          moreover have "((Hom⇘C⇙[\<emdash>,X]) ## (z2m⇘C ⇙f)) = (HomC⇘C⇙[(z2m⇘C ⇙f),X])" using assms fMor by (simp add: HomContraMor)
          ultimately show ?thesis by simp
        qed
        also have "... = (η $$ Y) |@| ((HomC⇘C⇙[z2m⇘C ⇙f,X]) |@| (m2z⇘C ⇙(Id C X)))" 
        proof-
          have "(HomC⇘C⇙[z2m⇘C ⇙f,X]) ≈>⇘SET⇙ (η $$ Y)" 
            using fCod fDom XObj LSCat fMor HomFtorContraMapsTo[of C X "z2m⇘C ⇙f"] eta_mapsTo by (simp add: MapsToCompDef)
          moreover have "|dom| (HomC⇘C⇙[z2m⇘C ⇙f,X]) = (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) X)" 
            by (simp add: ZFfunDom HomFtorMapContra_def)
          moreover have "(m2z⇘C ⇙(Id C X)) |∈| (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) X)" 
            using assms fCod by (simp add: Category.Cidm LSCategory.m2zz2m)
          ultimately show ?thesis by (simp add: SETCompAt)
        qed
        also have "... = (η $$ Y) |@| (m2z⇘C⇙ ((z2m⇘C ⇙f) ;;⇘C⇙ (z2m⇘C⇙ (m2z⇘C ⇙(Id C X)))))" 
        proof-
          have "(Id C X) maps⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) to X" using assms fCod by (simp add: Category.Cidm)
          hence "(m2z⇘C ⇙(Id C X)) |∈| (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙f)) X)" using assms by (simp add: LSCategory.m2zz2m)
          thus ?thesis by (simp add: HomContraAt)
        qed
        also have "... = (η $$ Y) |@| (m2z⇘C⇙ ((z2m⇘C ⇙f) ;;⇘C⇙ (Id C X)))" 
          using assms by (simp add: LSCategory.m2zz2mInv Category.CatIdInMor)
        also have "... = (η $$ Y) |@| (m2z⇘C⇙ (z2m⇘C ⇙f))" using assms(1) fCod fMor Category.Cidr[of C "(z2m⇘C ⇙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⇘C⇙ X X) (F @@ X) (λ f . (F ## (z2m⇘C⇙ f)) |@| x)" using assms by (simp add: YMapInvApp)
  moreover have "(m2z⇘C ⇙(Id C X)) |∈| (Hom⇘C⇙ X X)" using assms by (simp add: Category.Simps LSCategory.m2zz2m)
  ultimately have "(?η $$ X) |@| (m2z⇘C ⇙(Id C X)) = (F ## (z2m⇘C⇙ (m2z⇘C ⇙(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⇘C ⇙(Id C X)) = x" .
qed

lemma YFtorNT_YMapInv:
  assumes "LSCategory C" and "f maps⇘C⇙ X to Y"
  shows "YFtorNT C f = YMapInv C X (Hom⇘C⇙[\<emdash>,Y]) (m2z⇘C⇙ f)"
proof(simp only: YFtorNT_def YMapInv_def, rule NatTransExt')
  have Cf: "cod⇘C⇙ f = Y" and Df: "dom⇘C⇙ f = X" using assms by auto
  thus "NTCod (YFtorNT' C f) = NTCod (YMapInv' C X (Hom⇘C⇙[\<emdash>,Y]) (m2z⇘C⇙f))"
    by(simp add: YFtorNT'_def YMapInv'_def )
  have "Hom⇘C⇙[\<emdash>,dom⇘C⇙ f] = YFtor C @@ X" using Df assms by (simp add: YFtorObj Category.MapsToObj)
  thus "NTDom (YFtorNT' C f) = NTDom (YMapInv' C X (Hom⇘C⇙[\<emdash>,Y]) (m2z⇘C⇙f))"
    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⇘C⇙ Z X)"
      have "m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ f) = ((Hom⇘C⇙[\<emdash>,Y]) ## (z2m⇘C ⇙x)) |@| (m2z⇘C⇙f)"
      proof-
        have morf: "f ∈ Mor C" using assms by auto
        have mapsx: "(z2m⇘C ⇙x) maps⇘C⇙ Z to X" using x assms(1) ObjZ2 ObjX by (simp add: LSCategory.z2mm2z)
        hence morx: "(z2m⇘C ⇙x) ∈ Mor C" by auto
        hence "(Hom⇘C⇙[\<emdash>,Y]) ## (z2m⇘C ⇙x) = (HomC⇘C⇙[(z2m⇘C ⇙x),Y])" using assms by (simp add: HomContraMor)
        moreover have "(HomC⇘C⇙[(z2m⇘C ⇙x),Y]) |@| (m2z⇘C ⇙f) = m2z⇘C ⇙((z2m⇘C ⇙x) ;;⇘C⇙ (z2m⇘C ⇙(m2z⇘C ⇙f)))"
        proof (rule HomContraAt)
          have "cod⇘C⇙ (z2m⇘C ⇙x) = X" using mapsx by auto
          thus "(m2z⇘C ⇙f) |∈| (Hom⇘C⇙ (cod⇘C⇙ (z2m⇘C ⇙x)) Y)" using assms by (simp add: LSCategory.m2zz2m)
        qed
        moreover have "(z2m⇘C ⇙(m2z⇘C ⇙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⇘C⇙[\<emdash>,Y]) (m2z⇘C⇙f)) $$ 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⇘C⇙ X to Y"
  shows "YFtor C ## f = YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ 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⇘C⇙[\<emdash>,Y]) (m2z⇘C⇙ 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⇘C⇙ (YMap C X η)) = η"
  and "z2m⇘C⇙ (YMap C X η) maps⇘C⇙ 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⇘C⇙ X Y)" using assms by (simp add: YFtorObj2)
  thus "(z2m⇘C⇙ (YMap C X η)) maps⇘C⇙ X to Y" using assms by (simp add: LSCategory.z2mm2z)
  hence "YFtor C ## (z2m⇘C⇙ (YMap C X η)) = YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ (z2m⇘C⇙ (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⇘C⇙ (YMap C X η)) = η" using assms ftor by (simp add: YMap1)
qed

lemma YonedaFaithful:
  assumes "LSCategory C" and "f maps⇘C⇙ X to Y" and "g maps⇘C⇙ 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⇘C⇙ f) |∈| ((YFtor C @@ Y) @@ X)" and M2Zg: "(m2z⇘C⇙ 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⇘C⇙ f) = YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ g)"
    using assms by (simp add: YMapYoneda)
  hence "YMap C X (YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ f)) = YMap C X (YMapInv C X (YFtor C @@ Y) (m2z⇘C⇙ g))"
    by simp
  hence "(m2z⇘C⇙ f) = (m2z⇘C⇙ 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⇘C⇙[\<emdash>,A]) : (Op C) --> SET" and FtorB: "Ftor (Hom⇘C⇙[\<emdash>,B]) : (Op C) --> SET" 
    using assms by (simp add: HomFtorContraFtor)+
  have "Hom⇘C⇙[\<emdash>,A] = Hom⇘C⇙[\<emdash>,B]" using assms by (simp add: YFtorObj)
  hence "(Hom⇘C⇙[\<emdash>,A]) ## (Id (Op C) A) = (Hom⇘C⇙[\<emdash>,B]) ## (Id (Op C) A)" by simp
  hence "Id SET ((Hom⇘C⇙[\<emdash>,A]) @@ A) = Id SET ((Hom⇘C⇙[\<emdash>,B]) @@ A)" 
    using AObjOp BObjOp FtorA FtorB by (simp add: FunctorId)
  hence "Id SET (Hom⇘C ⇙A A) = Id SET (Hom⇘C ⇙A B)" using assms by (simp add: HomFtorOpObj)
  hence "Hom⇘C ⇙A A = Hom⇘C ⇙A B" using SETCategory by (simp add: Category.IdInj SETobj[of "Hom⇘C ⇙A A"] SETobj[of "Hom⇘C ⇙A B"])
  moreover have "(m2z⇘C⇙ (Id C A)) |∈| (Hom⇘C ⇙A A)" using assms by (simp add: Category.Cidm LSCategory.m2zz2m)
  ultimately have "(m2z⇘C⇙ (Id C A)) |∈| (Hom⇘C ⇙A B)" by simp
  hence "(z2m⇘C⇙ (m2z⇘C⇙ (Id C A))) maps⇘C⇙ A to B" using assms by (simp add: LSCategory.z2mm2z)
  hence "(Id C A) maps⇘C⇙ A to B" using assms by (simp add: Category.CatIdInMor LSCategory.m2zz2mInv)
  hence "cod⇘C⇙ (Id C A) = B" by auto
  thus ?thesis using assms by (simp add: Category.CatIdDomCod)
qed

end