Theory Functors

(*
Author: Alexander Katovsky
*)

section "Functor"

theory Functors
imports Category
begin

record ('o1, 'o2, 'm1, 'm2, 'a, 'b) Functor = 
  CatDom :: "('o1,'m1,'a)Category_scheme" 
  CatCod :: "('o2,'m2,'b)Category_scheme" 
  MapM :: "'m1 ⇒ 'm2" 

abbreviation
  FunctorMorApp :: "('o1, 'o2, 'm1, 'm2, 'a1, 'a2, 'a) Functor_scheme ⇒ 'm1 ⇒ 'm2" (infixr "##" 70) where
  "FunctorMorApp F m ≡ (MapM F) m"

definition
  MapO :: "('o1, 'o2, 'm1, 'm2, 'a1, 'a2, 'a) Functor_scheme ⇒ 'o1 ⇒ 'o2"  where
  "MapO F X ≡ THE Y . Y ∈ Obj(CatCod F) ∧  F ## (Id (CatDom F) X) = Id (CatCod F) Y"

abbreviation
  FunctorObjApp :: "('o1, 'o2, 'm1, 'm2, 'a1, 'a2, 'a) Functor_scheme ⇒ 'o1 ⇒ 'o2" (infixr "@@" 70) where
  "FunctorObjApp F X ≡ (MapO F X)"

locale PreFunctor = 
  fixes F :: "('o1, 'o2, 'm1, 'm2, 'a1, 'a2, 'a) Functor_scheme"  (structure) 
  assumes FunctorComp: "f ≈>⇘CatDom F⇙ g ⟹ F ## (f ;;⇘CatDom F⇙ g) = (F ## f) ;;⇘CatCod F⇙ (F ## g)"
  and     FunctorId:   "X ∈ obj⇘CatDom F⇙ ⟹ ∃ Y ∈ obj⇘CatCod F⇙ . F ## (id⇘CatDom F⇙ X) = id⇘CatCod F⇙ Y"
  and     CatDom[simp]:      "Category(CatDom F)"
  and     CatCod[simp]:      "Category(CatCod F)"

locale FunctorM = PreFunctor +
  assumes     FunctorCompM: "f maps⇘CatDom F⇙ X to Y ⟹ (F ## f) maps⇘CatCod F⇙ (F @@ X) to (F @@ Y)"

locale FunctorExt = 
  fixes F :: "('o1, 'o2, 'm1, 'm2, 'a1, 'a2, 'a) Functor_scheme"  (structure) 
  assumes FunctorMapExt: "(MapM F) ∈ extensional (Mor (CatDom F))"

locale Functor = FunctorM + FunctorExt

definition 
  MakeFtor :: "('o1, 'o2, 'm1, 'm2, 'a, 'b,'r) Functor_scheme ⇒ ('o1, 'o2, 'm1, 'm2, 'a, 'b,'r) Functor_scheme" where
  "MakeFtor F ≡ ⦇
      CatDom = CatDom F , 
      CatCod = CatCod F , 
      MapM = restrict (MapM F) (Mor (CatDom F)) , 
      … = Functor.more F
  ⦈"

lemma PreFunctorFunctor[simp]: "Functor F ⟹ PreFunctor F"
by (simp add: Functor_def FunctorM_def)

lemmas functor_simps = PreFunctor.FunctorComp PreFunctor.FunctorId

definition 
  functor_abbrev ("Ftor _ : _ ⟶ _" [81]) where
  "Ftor F : A ⟶ B ≡ (Functor F) ∧ (CatDom F = A) ∧ (CatCod F = B)"

lemma functor_abbrevE[elim]: "⟦Ftor F : A ⟶ B ; ⟦(Functor F) ; (CatDom F = A) ; (CatCod F = B)⟧ ⟹ R⟧ ⟹ R"
by (auto simp add: functor_abbrev_def)

definition
  functor_comp_def ("_ ≈>;;; _" [81]) where
  "functor_comp_def F G ≡ (Functor F) ∧ (Functor G) ∧ (CatDom G = CatCod F)"

lemma functor_comp_def[elim]: "⟦F ≈>;;; G ; ⟦Functor F ; Functor G ; CatDom G = CatCod F⟧ ⟹ R⟧ ⟹ R"
by (auto simp add: functor_comp_def_def)

lemma (in Functor) FunctorMapsTo:
  assumes "f ∈ mor⇘CatDom F⇙"
  shows   "F ## f maps⇘CatCod F⇙ (F @@ (dom⇘CatDom F⇙ f)) to (F @@ (cod⇘CatDom F⇙ f))"
proof-
  have "f maps⇘CatDom F⇙ (dom⇘CatDom F⇙ f) to (cod⇘CatDom F⇙ f)" using assms by auto
  thus ?thesis by (simp add: FunctorCompM[of f "dom⇘CatDom F⇙ f" "cod⇘CatDom F⇙ f"])
qed

lemma (in Functor) FunctorCodDom: 
  assumes "f ∈ mor⇘CatDom F⇙"
  shows "dom⇘CatCod F⇙(F ## f) = F @@ (dom⇘CatDom F⇙ f)" and "cod⇘CatCod F⇙(F ## f) = F @@ (cod⇘CatDom F⇙ f)"
proof-
  have "F ## f maps⇘CatCod F⇙ (F @@ (dom⇘CatDom F⇙ f)) to (F @@ (cod⇘CatDom F⇙ f))" using assms by (simp add: FunctorMapsTo)
  thus "dom⇘CatCod F⇙(F ## f) = F @@ (dom⇘CatDom F⇙ f)" and "cod⇘CatCod F⇙(F ## f) = F @@ (cod⇘CatDom F⇙ f)"
    by auto
qed

lemma (in Functor) FunctorCompPreserved: "f ∈ mor⇘CatDom F⇙ ⟹ F ## f ∈ mor⇘CatCod F⇙"
by (auto dest:FunctorMapsTo)

lemma (in Functor) FunctorCompDef: 
  assumes "f ≈>⇘CatDom F⇙ g" shows "(F ## f) ≈>⇘CatCod F⇙ (F ## g)"
proof(auto simp add: CompDefined_def)
  show "F ## f ∈ mor⇘CatCod F⇙" and "F ## g ∈ mor⇘CatCod F⇙" using assms by (auto simp add: FunctorCompPreserved)
  have "f ∈ mor⇘CatDom F⇙" and "g ∈ mor⇘CatDom F⇙" using assms by auto
  hence a: "cod⇘CatCod F⇙ (F ## f) = F @@ (cod⇘CatDom F⇙ f)" and b: "dom⇘CatCod F⇙(F ## g) = F @@ (dom⇘CatDom F⇙ g)"
    by (simp add: FunctorCodDom)+
  have "cod⇘CatCod F⇙ (F ## f) = F @@ (dom⇘CatDom F⇙ g)" using assms a by auto
  also have "... = dom⇘CatCod F⇙ (F ## g)" using b by simp
  finally show "cod⇘CatCod F⇙ (F ## f) = dom⇘CatCod F⇙ (F ## g)" .
qed

lemma FunctorComp: "⟦Ftor F : A ⟶ B ; f ≈>⇘A⇙ g⟧ ⟹ F ## (f ;;⇘A⇙ g) = (F ## f) ;;⇘B⇙ (F ## g)"
by (auto simp add: PreFunctor.FunctorComp)

lemma FunctorCompDef: "⟦Ftor F : A ⟶ B ; f ≈>⇘A⇙ g⟧ ⟹ (F ## f) ≈>⇘B⇙ (F ## g)"
by (auto simp add: Functor.FunctorCompDef)

lemma FunctorMapsTo: 
  assumes "Ftor F : A ⟶ B" and "f maps⇘A⇙ X to Y" 
  shows "(F ## f) maps⇘B⇙ (F @@ X) to (F @@ Y)"
proof-
  have b: "CatCod F = B" and a: "CatDom F = A" and ff: "Functor F" using assms by auto
  have df: "(dom⇘CatDom F⇙ f) = X" and cf: "(cod⇘CatDom F⇙ f) = Y" using a assms by auto
  have "f ∈ mor⇘CatDom F⇙" using assms by auto
  hence "F ## f maps⇘CatCod F⇙ (F @@ (dom⇘CatDom F⇙ f)) to (F @@ (cod⇘CatDom F⇙ f))" using ff
    by (simp add: Functor.FunctorMapsTo) 
  thus ?thesis using df cf b by simp
qed

lemma (in PreFunctor) FunctorId2: 
  assumes "X ∈ obj⇘CatDom F⇙"
  shows   "F @@ X ∈ obj⇘CatCod F⇙ ∧ F ## (id⇘CatDom F⇙ X) = id⇘CatCod F⇙ (F @@ X)"
proof-
  let ?Q = "λ E Y . Y ∈ obj⇘CatCod F⇙ ∧ E = id⇘CatCod F⇙ Y"
  let ?P = "?Q (F ## (id⇘CatDom F⇙ X))"
  from assms FunctorId obtain Y where "?P Y" by auto
  moreover  { 
    fix y e z have "⟦?Q e y ; ?Q e z⟧ ⟹ y = z"
      by (auto intro: Category.IdInj[of "CatCod F" y z])
  }
  ultimately have "∃! Z . ?P Z" by auto
  hence "?P (THE Y . ?P Y)" by (rule theI')
  thus ?thesis by (auto simp add: MapO_def)
qed

lemma FunctorId:
  assumes "Ftor F : C ⟶ D" and "X ∈ Obj C"
  shows "F ## (Id C X) = Id D (F @@ X)"
proof-
  have "CatDom F = C" and "CatCod F = D" and "PreFunctor F" using assms by auto
  thus ?thesis using assms PreFunctor.FunctorId2[of F X] by simp
qed

lemma (in Functor) DomFunctor: "f ∈ mor⇘CatDom F⇙ ⟹ dom⇘CatCod F⇙ (F ## f) = F @@ (dom⇘CatDom F⇙ f)"
by (simp add: FunctorCodDom)

lemma (in Functor) CodFunctor: "f ∈ mor⇘CatDom F⇙ ⟹ cod⇘CatCod F⇙ (F ## f) = F @@ (cod⇘CatDom F⇙ f)"
by (simp add: FunctorCodDom) 

lemma (in Functor) FunctorId3Dom:
  assumes "f ∈ mor⇘CatDom F⇙"
  shows   "F ## (id⇘CatDom F⇙ (dom⇘CatDom F⇙ f)) = id⇘CatCod F⇙ (dom⇘CatCod F⇙ (F ## f))"
proof-
  have "(dom⇘CatDom F⇙ f) ∈ obj⇘CatDom F⇙" using assms by (simp add: Category.Cdom)
  hence "F ## (id⇘CatDom F⇙ (dom⇘CatDom F⇙ f)) = id⇘CatCod F⇙ (F @@ (dom⇘CatDom F⇙ f))" by (simp add: FunctorId2)
  also have "... = id⇘CatCod F⇙ (dom⇘CatCod F⇙ (F ## f))" using assms by (simp add: DomFunctor)
  finally show ?thesis by simp
qed

lemma (in Functor) FunctorId3Cod:
  assumes "f ∈ mor⇘CatDom F⇙"
  shows   "F ## (id⇘CatDom F⇙ (cod⇘CatDom F⇙ f)) = id⇘CatCod F⇙ (cod⇘CatCod F⇙ (F ## f))"
proof-
  have "(cod⇘CatDom F⇙ f) ∈ obj⇘CatDom F⇙" using assms by (simp add: Category.Ccod)
  hence "F ## (id⇘CatDom F⇙ (cod⇘CatDom F⇙ f)) = id⇘CatCod F⇙ (F @@ (cod⇘CatDom F⇙ f))" by (simp add: FunctorId2)
  also have "... = id⇘CatCod F⇙ (cod⇘CatCod F⇙ (F ## f))" using assms by (simp add: CodFunctor)
  finally show ?thesis by simp
qed

lemma (in PreFunctor) FmToFo: "⟦X ∈ obj⇘CatDom F⇙ ; Y ∈ obj⇘CatCod F⇙ ; F ## (id⇘CatDom F⇙ X) = id⇘CatCod F⇙ Y⟧ ⟹ F @@ X = Y"
  by (auto simp add: FunctorId2 intro: Category.IdInj[of "CatCod F" "F @@ X" Y])

lemma MakeFtorPreFtor: 
  assumes "PreFunctor F" shows "PreFunctor (MakeFtor F)"
proof-
  {
    fix X assume a: "X ∈ obj⇘CatDom F⇙" have "id⇘CatDom F ⇙X ∈ mor⇘CatDom F⇙"
    proof-
      have "Category (CatDom F)" using assms by (simp add: PreFunctor_def)
      hence "id⇘CatDom F ⇙X maps⇘CatDom F⇙ X to X" using a by (simp add: Category.Cidm)
      thus ?thesis using a by (auto)
    qed
  }
  thus "PreFunctor (MakeFtor F)" using assms
    by(auto simp add: PreFunctor_def MakeFtor_def Category.MapsToMorDomCod)
qed

lemma MakeFtorMor: "f ∈ mor⇘CatDom F⇙ ⟹ MakeFtor F ## f = F ## f"
by(simp add: MakeFtor_def)

lemma MakeFtorObj: 
  assumes "PreFunctor F" and "X ∈ obj⇘CatDom F⇙"
  shows "MakeFtor F @@ X = F @@ X"
proof-
  have "X ∈ obj⇘CatDom (MakeFtor F)⇙" using assms(2) by (simp add: MakeFtor_def)
  moreover have "(F @@ X) ∈ obj⇘CatCod (MakeFtor F)⇙" using assms by (simp add: PreFunctor.FunctorId2 MakeFtor_def)
  moreover have "MakeFtor F ## id⇘CatDom (MakeFtor F) ⇙X = id⇘CatCod (MakeFtor F) ⇙(F @@ X)" 
  proof-
    have "Category (CatDom F)" using assms(1) by (simp add: PreFunctor_def)
    hence "id⇘CatDom F ⇙X  maps⇘CatDom F⇙ X to X" using assms(2) by (auto simp add: Category.Cidm)
    hence "id⇘CatDom F ⇙X ∈ mor⇘CatDom F⇙" by auto
    hence "MakeFtor F ## id⇘CatDom (MakeFtor F) ⇙X = F ## id⇘CatDom F ⇙X" by (simp add: MakeFtor_def)
    also have "... = id⇘CatCod F ⇙(F @@ X)" using assms by (simp add: PreFunctor.FunctorId2)
    finally show ?thesis by (simp add: MakeFtor_def)
  qed
  moreover have "PreFunctor (MakeFtor F)" using assms(1) by (simp add: MakeFtorPreFtor)
  ultimately show ?thesis by (simp add: PreFunctor.FmToFo)
qed

lemma MakeFtor: assumes "FunctorM F" shows "Functor (MakeFtor F)" 
proof(intro_locales)
  show "PreFunctor (MakeFtor F)" using assms by (simp add: MakeFtorPreFtor FunctorM_def)
  show "FunctorM_axioms (MakeFtor F)"
  proof(auto simp add: FunctorM_axioms_def)
    {
      fix f X Y assume aa: "f maps⇘CatDom (MakeFtor F)⇙ X to Y"
      show "((MakeFtor F) ## f) maps⇘CatCod (MakeFtor F)⇙ ((MakeFtor F) @@ X) to ((MakeFtor F) @@ Y)"
      proof-
        have "((MakeFtor F) ## f) = F ## f" using aa by (auto simp add: MakeFtor_def)
        moreover have "((MakeFtor F) @@ X) = F @@ X" and "((MakeFtor F) @@ Y) = F @@ Y"
        proof-
          have "Category (CatDom F)" using assms by (simp add: FunctorM_def PreFunctor_def)
          hence "X ∈ obj⇘CatDom F⇙" and "Y ∈ obj⇘CatDom F⇙" 
            using aa by (auto simp add: Category.MapsToObj MakeFtor_def)
          moreover have "PreFunctor F" using assms(1) by (simp add: FunctorM_def)
          ultimately show "((MakeFtor F) @@ X) = F @@ X" and "((MakeFtor F) @@ Y) = F @@ Y"
            by (simp add: MakeFtorObj)+
        qed
        moreover have "F ## f maps⇘CatCod F⇙ (F @@ X) to (F @@ Y)" using assms(1) aa 
          by (simp add: FunctorM.FunctorCompM MakeFtor_def)
        ultimately show ?thesis by (simp add: MakeFtor_def)
      qed
    }
  qed
  show "FunctorExt (MakeFtor F)" by(simp add: FunctorExt_def MakeFtor_def)
qed

definition 
  IdentityFunctor' :: "('o,'m,'a) Category_scheme ⇒ ('o,'o,'m,'m,'a,'a) Functor" ("FId'' _" [70]) where
  "IdentityFunctor' C ≡ ⦇CatDom = C , CatCod = C , MapM = (λ f . f) ⦈"

definition 
  IdentityFunctor ("FId _" [70]) where
  "IdentityFunctor C ≡ MakeFtor(IdentityFunctor' C)"

lemma IdFtor'PreFunctor: "Category C ⟹ PreFunctor (FId' C)"
by(auto simp add: PreFunctor_def IdentityFunctor'_def)

lemma IdFtor'Obj:
  assumes "Category C" and "X ∈ obj⇘CatDom (FId' C)⇙"
  shows "(FId' C) @@ X = X"
proof-
  have "(FId' C) ## id⇘CatDom (FId' C)⇙ X = id⇘CatCod (FId' C)⇙ X" by(simp add: IdentityFunctor'_def)
  moreover have "X ∈ obj⇘CatCod (FId' C)⇙" using assms by (simp add: IdentityFunctor'_def)
  ultimately show ?thesis using assms by (simp add: PreFunctor.FmToFo IdFtor'PreFunctor)
qed

lemma IdFtor'FtorM:  
  assumes "Category C" shows "FunctorM (FId' C)"
proof(auto simp add: FunctorM_def IdFtor'PreFunctor assms FunctorM_axioms_def)
  {
    fix f X Y assume a: "f maps⇘CatDom (FId' C)⇙ X to Y" 
    show "((FId' C) ## f) maps⇘CatCod (FId' C)⇙ ((FId' C) @@ X) to ((FId' C) @@ Y)"
    proof-
      have "X ∈ obj⇘CatDom (FId' C)⇙" and "Y ∈ obj⇘CatDom (FId' C)⇙"
        using a assms by (simp add: Category.MapsToObj IdentityFunctor'_def)+
      moreover have "(FId' C) ## f = f" and "CatDom (FId' C) = CatCod (FId' C)" by (simp add: IdentityFunctor'_def)+
      ultimately show ?thesis using assms a by(simp add: IdFtor'Obj)
    qed
  }
qed

lemma IdFtorFtor:  "Category C ⟹ Functor (FId C)"
by (auto simp add: IdentityFunctor_def IdFtor'FtorM intro: MakeFtor)

definition 
  ConstFunctor' :: "('o1,'m1,'a) Category_scheme ⇒ 
                  ('o2,'m2,'b) Category_scheme ⇒ 'o2 ⇒ ('o1,'o2,'m1,'m2,'a,'b) Functor"  where
  "ConstFunctor' A B b ≡ ⦇
         CatDom = A , 
         CatCod = B , 
         MapM = (λ f . (Id B) b)
  ⦈"

definition "ConstFunctor A B b ≡ MakeFtor(ConstFunctor' A B b)"

lemma ConstFtor' : 
  assumes "Category A" "Category B" "b ∈ (Obj B)"
  shows   "PreFunctor (ConstFunctor' A B b)"
  and     "FunctorM (ConstFunctor' A B b)"
proof-
  show "PreFunctor (ConstFunctor' A B b)" using assms
    apply (subst PreFunctor_def)
    apply (rule conjI)+
    by (auto simp add: ConstFunctor'_def Category.Simps Category.CatIdCompId)
  moreover 
  {
    fix X  assume "X ∈ obj⇘A⇙" "b ∈ obj⇘B⇙" "PreFunctor (ConstFunctor' A B b)" 
    hence "(ConstFunctor' A B b) @@ X = b"
      by (auto simp add: ConstFunctor'_def PreFunctor.FmToFo Category.Simps)
  }
  ultimately show "FunctorM (ConstFunctor' A B b)" using assms
    by (intro_locales, auto simp add: ConstFunctor'_def Category.Simps FunctorM_axioms_def)
qed

lemma ConstFtor: 
  assumes "Category A" "Category B" "b ∈ (Obj B)"
  shows "Functor (ConstFunctor A B b)"
by (auto simp add: assms ConstFtor' ConstFunctor_def MakeFtor)

definition 
  UnitFunctor :: "('o,'m,'a) Category_scheme ⇒ ('o,unit,'m,unit,'a,unit) Functor"  where
  "UnitFunctor C ≡ ConstFunctor C UnitCategory ()"

lemma UnitFtor: 
  assumes "Category C" 
  shows "Functor(UnitFunctor C)"
proof-
  have "() ∈ obj⇘UnitCategory⇙" by (simp add: UnitCategory_def MakeCatObj)
  hence "Functor(ConstFunctor C UnitCategory ())" using assms 
    by (simp add: ConstFtor)
  thus ?thesis by (simp add: UnitFunctor_def)
qed

definition
  FunctorComp' :: "('o1,'o2,'m1,'m2,'a1,'a2) Functor ⇒ ('o2,'o3,'m2,'m3,'b1,'b2) Functor
                    ⇒ ('o1,'o3,'m1,'m3,'a1,'b2) Functor" (infixl ";;:" 71) where
  "FunctorComp' F G ≡ ⦇
        CatDom = CatDom F , 
        CatCod = CatCod G ,
        MapM   = λ f . (MapM G)((MapM F) f)
  ⦈"

definition FunctorComp (infixl ";;;" 71) where "FunctorComp F G ≡ MakeFtor (FunctorComp' F G)"

lemma FtorCompComp':
  assumes "f ≈>⇘CatDom F⇙ g"
  and "F ≈>;;; G"
  shows "G ## (F ## (f ;;⇘CatDom F⇙ g)) = (G ## (F ## f)) ;;⇘CatCod G⇙ (G ## (F ## g))"
proof-
  have [simp]: "PreFunctor G ∧ PreFunctor F" using assms by auto
  have [simp]: "(F ## f) ≈>⇘CatDom G⇙ (F ## g)" using assms by (auto simp add: Functor.FunctorCompDef[of F f g])
  have "F ## (f ;;⇘CatDom F⇙ g) = (F ## f) ;;⇘CatCod F⇙ (F ## g)" using assms
    by (auto simp add: PreFunctor.FunctorComp)
  hence "G ## (F ## (f ;;⇘CatDom F⇙ g)) = G ## ((F ## f) ;;⇘CatCod F⇙ (F ## g))" by simp
  also have "... = G ## ((F ## f) ;;⇘CatDom G⇙ (F ## g))" using assms by auto
  also have "... = (G ## (F ## f)) ;;⇘CatCod G⇙ (G ## (F ## g))"
    by (simp add: PreFunctor.FunctorComp[of G "(F ## f)" "(F ## g)"])
  finally show ?thesis by simp
qed

lemma FtorCompId: 
  assumes a: "X ∈ (Obj (CatDom F))"
  and "F ≈>;;; G"
  shows "G ## (F ## (id⇘CatDom F ⇙X)) = id⇘CatCod G⇙(G @@ (F @@ X)) ∧ G @@ (F @@ X) ∈ (Obj (CatCod G))"
proof-
  have [simp]: "PreFunctor G ∧ PreFunctor F" using assms by auto
  have b: "(F @@ X) ∈ obj⇘CatDom G⇙" using assms
    by (auto simp add: PreFunctor.FunctorId2)
  have "G ## F ## (id⇘CatDom F ⇙X) = G ## (id⇘CatCod F⇙(F @@ X))" using b a
    by (simp add: PreFunctor.FunctorId2[of F "X"])
  also have "... = G ## (id⇘CatDom G⇙(F @@ X))" using assms by auto
  also have "... = id⇘CatCod G⇙(G @@ (F @@ X)) ∧ G @@ (F @@ X) ∈ (Obj (CatCod G))" using b
    by (simp add: PreFunctor.FunctorId2[of G "(F @@ X)"])
  finally show ?thesis by simp
qed

lemma FtorCompIdDef: 
  assumes a: "X ∈ (Obj (CatDom F))" and b: "PreFunctor (F ;;: G)" 
  and "F ≈>;;; G"
  shows "(F ;;: G) @@ X = (G @@ (F @@ X))"
proof-
  have "(F ;;: G) ## (id⇘CatDom (F ;;: G)⇙(X)) = G ## (F ## (id⇘CatDom F⇙(X)))" using assms
    by (simp add: FunctorComp'_def)
  also have "... = id⇘CatCod G⇙(G @@ (F @@ (X)))" using assms a
    by(auto simp add: FtorCompId[of _ F G])
  finally have "(F ;;: G) ## (id⇘CatDom (F ;;: G)⇙(X)) = id⇘CatCod (F ;;: G)⇙(G @@ (F @@ X))" using assms
    by (simp add: FunctorComp'_def)
  moreover have "G @@ (F @@ (X)) ∈ (Obj (CatCod (F ;;: G)))" using assms a
    by(auto simp add: FtorCompId[of _ F G] FunctorComp'_def)
  moreover have "X ∈ obj⇘CatDom (F ;;: G)⇙" using a by (simp add: FunctorComp'_def)
  ultimately show ?thesis using b 
    by (simp add: PreFunctor.FmToFo[of "F ;;: G" X "G @@ (F @@ X)"])
qed

lemma FunctorCompMapsTo: 
  assumes "f ∈ mor⇘CatDom (F ;;: G)⇙" and "F ≈>;;; G"
  shows "(G ## (F ## f)) maps⇘CatCod G⇙ (G @@ (F @@ (dom⇘CatDom F⇙ f))) to (G @@ (F @@ (cod⇘CatDom F⇙ f)))"
proof-
  have "f ∈ mor⇘CatDom F ⇙∧ Functor F" using assms by (auto simp add: FunctorComp'_def)
  hence "(F ## f) maps⇘CatDom G⇙ (F @@ (dom⇘CatDom F⇙ f)) to (F @@ (cod⇘CatDom F⇙ f))" using assms 
    by (auto simp add: Functor.FunctorMapsTo[of F f])
  moreover have "FunctorM G" using assms by (auto simp add: FunctorComp_def Functor_def)
  ultimately show ?thesis by(simp add: FunctorM.FunctorCompM[of G "F ## f" "F @@ (dom⇘CatDom F⇙ f)" "F @@ (cod⇘CatDom F⇙ f)"])
qed

lemma FunctorCompMapsTo2:
  assumes "f ∈ mor⇘CatDom (F ;;: G)⇙" 
  and "F ≈>;;; G"
  and "PreFunctor (F ;;: G)" 
  shows "((F ;;: G) ## f) maps⇘CatCod (F ;;: G)⇙ ((F ;;: G) @@ (dom⇘CatDom (F ;;: G)⇙ f)) to 
                                               ((F ;;: G) @@ (cod⇘CatDom (F ;;: G)⇙ f))"
proof-
  have "Category (CatDom (F ;;: G))" using assms by (simp add: PreFunctor_def) 
  hence 1: "(dom⇘CatDom (F ;;: G)⇙ f) ∈ obj⇘CatDom F ⇙∧ (cod⇘CatDom (F ;;: G)⇙ f) ∈ obj⇘CatDom F⇙" using assms 
    by (auto simp add: Category.Simps FunctorComp'_def)
  have "(G ## (F ## f)) maps⇘CatCod G⇙ (G @@ (F @@ (dom⇘CatDom F⇙ f))) to (G @@ (F @@ (cod⇘CatDom F⇙ f)))"
    using assms by (auto simp add: FunctorCompMapsTo[of f F G])
  moreover have "CatDom F = CatDom(F ;;: G) ∧ CatCod G = CatCod(F ;;: G) ∧ (G ## (F ## f)) = ((F ;;: G) ## f)" using assms
    by (simp add: FunctorComp'_def)
  moreover have "(F ;;: G) @@ (dom⇘CatDom (F ;;: G)⇙ f) = (G @@ (F @@ (dom⇘CatDom(F ;;: G)⇙ f))) ∧
        (F ;;: G) @@ (cod⇘CatDom (F ;;: G)⇙ f) = (G @@ (F @@ (cod⇘CatDom(F ;;: G)⇙ f)))" 
    by (auto simp add: FtorCompIdDef[of _ F G] 1 assms)
  ultimately show ?thesis by auto
qed

lemma FunctorCompMapsTo3:
  assumes "f maps⇘CatDom (F ;;: G)⇙ X to Y"
  and "F ≈>;;; G"
  and "PreFunctor (F ;;: G)" 
  shows "F ;;: G ## f maps⇘CatCod (F ;;: G)⇙ F ;;: G @@ X to F ;;: G @@ Y"
proof-
  have  "f ∈ mor⇘CatDom (F ;;: G)⇙" 
    and "dom⇘CatDom (F ;;: G)⇙ f = X" 
    and "cod⇘CatDom (F ;;: G)⇙ f = Y" using assms by auto
  thus ?thesis using assms by (auto intro: FunctorCompMapsTo2)
qed

lemma FtorCompPreFtor:
  assumes "F ≈>;;; G"
  shows   "PreFunctor (F ;;: G)"
proof-
  have 1: "PreFunctor G ∧ PreFunctor F" using assms by auto
  show "PreFunctor (F ;;: G)" using assms
  proof(auto simp add: PreFunctor_def FunctorComp'_def Category.Simps
       FtorCompId[of _ F G] intro:FtorCompComp')
    show "Category (CatDom F)" and "Category (CatCod G)" using assms 1 by (auto simp add: PreFunctor_def)
  qed
qed

lemma FtorCompM : 
  assumes "F ≈>;;; G"
  shows   "FunctorM (F ;;: G)"
proof(auto simp only: FunctorM_def)
  show 1: "PreFunctor (F ;;: G)" using assms by (rule FtorCompPreFtor)
  {
    fix X Y f assume a: "f maps⇘CatDom (F ;;: G)⇙ X to Y"
    have "F ;;: G ## f maps⇘CatCod (F ;;: G)⇙ F ;;: G @@ X to F ;;: G @@ Y" 
      using a assms 1 by (rule FunctorCompMapsTo3)
  }
  thus "FunctorM_axioms (F ;;: G)" 
    by(auto simp add: 1 FunctorM_axioms_def)
qed

lemma FtorComp:   
  assumes "F ≈>;;; G"
  shows   "Functor (F ;;; G)"
proof-
  have "FunctorM (F ;;: G)" using assms by (rule FtorCompM)
  thus ?thesis by (simp add: FunctorComp_def MakeFtor)
qed

lemma (in Functor) FunctorPreservesIso: 
  assumes     "ciso⇘CatDom F⇙ k"
  shows       "ciso⇘CatCod F⇙ (F ## k)"
proof-
  have [simp]: "k ∈ mor⇘CatDom F⇙" using assms by (simp add: Category.IsoIsMor)
  have "cinv⇘CatCod F⇙ (F ## k) (F ## (Cinv⇘CatDom F⇙ k))" 
    proof(rule Category.Inverse_relI)
      show "Category (CatCod F)" by simp
      show "(F ## k) ≈>⇘CatCod F⇙ (F ## (Cinv⇘CatDom F⇙ k))" 
        by (rule FunctorCompDef, simp add: Category.IsoCompInv assms)
      show "(F ## k) ;;⇘CatCod F⇙ (F ## (Cinv⇘CatDom F⇙ k)) = id⇘CatCod F⇙ (dom⇘CatCod F⇙ (F ## k))" 
      proof-
        have      "(F ## k) ;;⇘CatCod F⇙ (F ## (Cinv⇘CatDom F⇙ k)) = F ## (k ;;⇘CatDom F⇙ (Cinv⇘CatDom F⇙ k))" using assms
          by(auto simp add: FunctorComp Category.IsoCompInv)
        also have "... = F ## (id⇘CatDom F⇙ (dom⇘CatDom F⇙ k))" using assms by (simp add: Category.IsoInvId2)
        also have "... = id⇘CatCod F⇙ (dom⇘CatCod F⇙ (F ## k))" by (simp add: FunctorId3Dom) 
        finally show ?thesis by simp
      qed 
      show "(F ## (Cinv⇘CatDom F⇙ k)) ;;⇘CatCod F⇙ (F ## k) = id⇘CatCod F⇙ (cod⇘CatCod F⇙ (F ## k))" 
      proof-
        have      "(F ## (Cinv⇘CatDom F⇙ k)) ;;⇘CatCod F⇙ (F ## k) = F ## ((Cinv⇘CatDom F⇙ k) ;;⇘CatDom F⇙  k)" using assms
          by(auto simp add: FunctorComp Category.InvCompIso)
        also have "... = F ## (id⇘CatDom F⇙ (cod⇘CatDom F⇙ k))" using assms by (simp add: Category.IsoInvId1)
        also have "... = id⇘CatCod F⇙ (cod⇘CatCod F⇙ (F ## k))" using assms by (simp add: FunctorId3Cod) 
        finally show ?thesis by simp
      qed   
    qed
  thus ?thesis by(auto simp add: isomorphism_def)
qed

declare PreFunctor.CatDom[simp] PreFunctor.CatCod [simp]

lemma FunctorMFunctor[simp]: "Functor F ⟹ FunctorM F"
by (simp add: Functor_def)

locale Equivalence = Functor +
  assumes Full: "⟦A ∈ Obj (CatDom F) ; B ∈ Obj (CatDom F) ; 
                  h maps⇘CatCod F⇙ (F @@ A) to (F @@ B)⟧ ⟹
                 ∃ f . (f maps⇘CatDom F⇙ A to B) ∧ (F ## f = h)"
  and Faithful: "⟦f maps⇘CatDom F⇙ A to B ; g maps⇘CatDom F⇙ A to B ; F ## f = F ## g⟧ ⟹ f = g"
  and IsoDense: "C ∈ Obj (CatCod F) ⟹ ∃ A ∈ Obj (CatDom F) . ObjIso (CatCod F) (F @@ A) C"

end