(*
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 ≈> _F g ==> F ## (f ;; _F g) = (F ## f) ;; _F (F ## g)"
  and     FunctorId:   "X ∈ obj _F ==> ∃ Y ∈ obj _F . F ## (id _F X) = id _F Y"
  and     CatDom[simp]:      "Category(CatDom F)"
  and     CatCod[simp]:      "Category(CatCod F)"

locale FunctorM = PreFunctor +
  assumes     FunctorCompM: "f maps _F X to Y ==> (F ## f) maps _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 _F"
  shows   "F ## f maps _F (F @@ (dom _F f)) to (F @@ (cod _F f))"
proof-
  have "f maps _F (dom _F f) to (cod _F f)" using assms by auto
  thus ?thesis by (simp add: FunctorCompM[of f "dom _F f" "cod _F f"])
qed

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

lemma (in Functor) FunctorCompPreserved: "f ∈ mor _F ==> F ## f ∈ mor _F"
by (auto dest:FunctorMapsTo)

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

lemma FunctorComp: "[Ftor F : A ⟶ B ; f ≈> g] ==> F ## (f ;; g) = (F ## f) ;; (F ## g)"
by (auto simp add: PreFunctor.FunctorComp)

lemma FunctorCompDef: "[Ftor F : A ⟶ B ; f ≈> g] ==> (F ## f) ≈> (F ## g)"
by (auto simp add: Functor.FunctorCompDef)

lemma FunctorMapsTo: 
  assumes "Ftor F : A ⟶ B" and "f maps X to Y" 
  shows "(F ## f) maps (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 _F f) = X" and cf: "(cod _F f) = Y" using a assms by auto
  have "f ∈ mor _F" using assms by auto
  hence "F ## f maps _F (F @@ (dom _F f)) to (F @@ (cod _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 _F"
  shows   "F @@ X ∈ obj _F ∧ F ## (id _F X) = id _F (F @@ X)"
proof-
  let ?Q = "λ E Y . Y ∈ obj _F ∧ E = id _F Y"
  let ?P = "?Q (F ## (id _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 _F ==> dom _F (F ## f) = F @@ (dom _F f)"
by (simp add: FunctorCodDom)

lemma (in Functor) CodFunctor: "f ∈ mor _F ==> cod _F (F ## f) = F @@ (cod _F f)"
by (simp add: FunctorCodDom) 

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

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

lemma (in PreFunctor) FmToFo: "[X ∈ obj _F ; Y ∈ obj _F ; F ## (id _F X) = id _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 _F" have "id _F X ∈ mor _F"
    proof-
      have "Category (CatDom F)" using assms by (simp add: PreFunctor_def)
      hence "id _F X maps _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 _F ==> MakeFtor F ## f = F ## f"
by(simp add: MakeFtor_def)

lemma MakeFtorObj: 
  assumes "PreFunctor F" and "X ∈ obj _F"
  shows "MakeFtor F @@ X = F @@ X"
proof-
  have "X ∈ obj _{(MakeFtor F)}" using assms(2) by (simp add: MakeFtor_def)
  moreover have "(F @@ X) ∈ obj _{(MakeFtor F)}" using assms by (simp add: PreFunctor.FunctorId2 MakeFtor_def)
  moreover have "MakeFtor F ## id _{(MakeFtor F)} X = id _{(MakeFtor F)} (F @@ X)" 
  proof-
    have "Category (CatDom F)" using assms(1) by (simp add: PreFunctor_def)
    hence "id _F X maps _F X to X" using assms(2) by (auto simp add: Category.Cidm)
    hence "id _F X ∈ mor _F" by auto
    hence "MakeFtor F ## id _{(MakeFtor F)} X = F ## id _F X" by (simp add: MakeFtor_def)
    also have "... = id _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 _{(MakeFtor F)} X to Y"
      show "((MakeFtor F) ## f) maps _{(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 _F" and "Y ∈ obj _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 _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 _{(FId' C)}"
  shows "(FId' C) @@ X = X"
proof-
  have "(FId' C) ## id _{(FId' C)} X = id _{(FId' C)} X" by(simp add: IdentityFunctor'_def)
  moreover have "X ∈ obj _{(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 _{(FId' C)} X to Y" 
    show "((FId' C) ## f) maps _{(FId' C)} ((FId' C) @@ X) to ((FId' C) @@ Y)"
    proof-
      have "X ∈ obj _{(FId' C)}" and "Y ∈ obj _{(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" "b ∈ obj" "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" 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 ≈> _F g"
  and "F ≈>;;; G"
  shows "G ## (F ## (f ;; _F g)) = (G ## (F ## f)) ;; _G (G ## (F ## g))"
proof-
  have [simp]: "PreFunctor G ∧ PreFunctor F" using assms by auto
  have [simp]: "(F ## f) ≈> _G (F ## g)" using assms by (auto simp add: Functor.FunctorCompDef[of F f g])
  have "F ## (f ;; _F g) = (F ## f) ;; _F (F ## g)" using assms
    by (auto simp add: PreFunctor.FunctorComp)
  hence "G ## (F ## (f ;; _F g)) = G ## ((F ## f) ;; _F (F ## g))" by simp
  also have "... = G ## ((F ## f) ;; _G (F ## g))" using assms by auto
  also have "... = (G ## (F ## f)) ;; _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 _F X)) = id _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 _G" using assms
    by (auto simp add: PreFunctor.FunctorId2)
  have "G ## F ## (id _F X) = G ## (id _F(F @@ X))" using b a
    by (simp add: PreFunctor.FunctorId2[of F "X"])
  also have "... = G ## (id _G(F @@ X))" using assms by auto
  also have "... = id _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 _{(F ;;: G)}(X)) = G ## (F ## (id _F(X)))" using assms
    by (simp add: FunctorComp'_def)
  also have "... = id _G(G @@ (F @@ (X)))" using assms a
    by(auto simp add: FtorCompId[of _ F G])
  finally have "(F ;;: G) ## (id _{(F ;;: G)}(X)) = id _{(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 _{(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 _{(F ;;: G)}" and "F ≈>;;; G"
  shows "(G ## (F ## f)) maps _G (G @@ (F @@ (dom _F f))) to (G @@ (F @@ (cod _F f)))"
proof-
  have "f ∈ mor _F ∧ Functor F" using assms by (auto simp add: FunctorComp'_def)
  hence "(F ## f) maps _G (F @@ (dom _F f)) to (F @@ (cod _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 _F f)" "F @@ (cod _F f)"])
qed

lemma FunctorCompMapsTo2:
  assumes "f ∈ mor _{(F ;;: G)}" 
  and "F ≈>;;; G"
  and "PreFunctor (F ;;: G)" 
  shows "((F ;;: G) ## f) maps _{(F ;;: G)} ((F ;;: G) @@ (dom _{(F ;;: G)} f)) to
                                               ((F ;;: G) @@ (cod _{(F ;;: G)} f))"
proof-
  have "Category (CatDom (F ;;: G))" using assms by (simp add: PreFunctor_def) 
  hence 1: "(dom _{(F ;;: G)} f) ∈ obj _F ∧ (cod _{(F ;;: G)} f) ∈ obj _F" using assms 
    by (auto simp add: Category.Simps FunctorComp'_def)
  have "(G ## (F ## f)) maps _G (G @@ (F @@ (dom _F f))) to (G @@ (F @@ (cod _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 _{(F ;;: G)} f) = (G @@ (F @@ (dom_{(F ;;: G)} f))) ∧
        (F ;;: G) @@ (cod _{(F ;;: G)} f) = (G @@ (F @@ (cod_{(F ;;: G)} f)))" 
    by (auto simp add: FtorCompIdDef[of _ F G] 1 assms)
  ultimately show ?thesis by auto
qed

lemma FunctorCompMapsTo3:
  assumes "f maps _{(F ;;: G)} X to Y"
  and "F ≈>;;; G"
  and "PreFunctor (F ;;: G)" 
  shows "F ;;: G ## f maps _{(F ;;: G)} F ;;: G @@ X to F ;;: G @@ Y"
proof-
  have  "f ∈ mor _{(F ;;: G)}" 
    and "dom _{(F ;;: G)} f = X" 
    and "cod _{(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 _{(F ;;: G)} X to Y"
    have "F ;;: G ## f maps _{(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 _F k"
  shows       "ciso _F (F ## k)"
proof-
  have [simp]: "k ∈ mor _F" using assms by (simp add: Category.IsoIsMor)
  have "cinv _F (F ## k) (F ## (Cinv _F k))" 
    proof(rule Category.Inverse_relI)
      show "Category (CatCod F)" by simp
      show "(F ## k) ≈> _F (F ## (Cinv _F k))" 
        by (rule FunctorCompDef, simp add: Category.IsoCompInv assms)
      show "(F ## k) ;; _F (F ## (Cinv _F k)) = id _F (dom _F (F ## k))" 
      proof-
        have      "(F ## k) ;; _F (F ## (Cinv _F k)) = F ## (k ;; _F (Cinv _F k))" using assms
          by(auto simp add: FunctorComp Category.IsoCompInv)
        also have "... = F ## (id _F (dom _F k))" using assms by (simp add: Category.IsoInvId2)
        also have "... = id _F (dom _F (F ## k))" by (simp add: FunctorId3Dom) 
        finally show ?thesis by simp
      qed 
      show "(F ## (Cinv _F k)) ;; _F (F ## k) = id _F (cod _F (F ## k))" 
      proof-
        have      "(F ## (Cinv _F k)) ;; _F (F ## k) = F ## ((Cinv _F k) ;; _F k)" using assms
          by(auto simp add: FunctorComp Category.InvCompIso)
        also have "... = F ## (id _F (cod _F k))" using assms by (simp add: Category.IsoInvId1)
        also have "... = id _F (cod _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 _F (F @@ A) to (F @@ B)] ==>
                 ∃ f . (f maps _F A to B) ∧ (F ## f = h)"
  and Faithful: "[f maps _F A to B ; g maps _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