header "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