(*
Author: Alexander Katovsky
*)

section "Category"

theory Category
imports "HOL-Library.FuncSet"
begin

record ('o,'m) Category = 
  Obj :: "'o set" (‹objı› 70) 
  Mor :: "'m set" (‹morı› 70)
  Dom :: "'m → 'o" (‹domı _› [80] 70)
  Cod :: "'m → 'o" (‹codı _› [80] 70)
  Id  :: "'o → 'm" (‹idı _› [80] 75)
  Comp :: "'m → 'm → 'm" (infixl ‹;;ı› 70)

definition
  MapsTo :: "('o,'m,'a) Category_scheme → 'm → 'o → 'o → bool" (‹_ mapsı _ to _› [60, 60, 60] 65) where
  "MapsTo CC f X Y ≡ f ∈ Mor CC ∧ Dom CC f = X ∧ Cod CC f = Y"

definition
  CompDefined :: "('o,'m,'a) Category_scheme → 'm → 'm → bool" (infixl ‹≈>ı› 65) where
  "CompDefined CC f g ≡ f ∈ Mor CC ∧ g ∈ Mor CC ∧ Cod CC f = Dom CC g"

locale ExtCategory = 
  fixes C :: "('o,'m,'a) Category_scheme" (structure)
  assumes CdomExt: "(Dom C) ∈ extensional (Mor C)"
  and     CcodExt: "(Cod C) ∈ extensional (Mor C)"
  and     CidExt:  "(Id C) ∈ extensional (Obj C)"
  and     CcompExt:  "(case_prod (Comp C)) ∈ extensional ({(f,g) | f g . f ≈> g})"

locale Category = ExtCategory +
  assumes Cdom : "f ∈ mor ==> dom f ∈ obj"
  and     Ccod : "f ∈ mor ==> cod f ∈ obj"
  and     Cidm [dest]: "X ∈ obj ==> (id X) maps X to X"
  and     Cidl : "f ∈ mor ==> id (dom f) ;; f = f"
  and     Cidr : "f ∈ mor ==> f ;; id (cod f) = f"
  and     Cassoc : "[f ≈> g ; g ≈> h] ==> (f ;; g) ;; h = f ;; (g ;; h)"
  and     Ccompt : "[f maps X to Y ; g maps Y to Z] ==> (f ;; g) maps X to Z"

definition 
  MakeCat :: "('o,'m,'a) Category_scheme → ('o,'m,'a) Category_scheme" where
  "MakeCat C ≡ (
      Obj = Obj C ,
      Mor = Mor C ,
      Dom = restrict (Dom C) (Mor C) ,
      Cod = restrict (Cod C) (Mor C) ,
      Id = restrict (Id C) (Obj C) ,
      Comp = λ f g . (restrict (case_prod (Comp C)) ({(f,g) | f g . f ≈> g})) (f,g),
      … = Category.more C
  )"

lemma MakeCatMapsTo: "f maps X to Y ==> f maps _C X to Y"
by (auto simp add: MapsTo_def MakeCat_def)

lemma MakeCatComp: "f ≈> g ==> f ;; _C g = f ;; g"
by (auto simp add: MapsTo_def MakeCat_def)

lemma MakeCatId: "X ∈ obj ==> id X = id _C X"
by (auto simp add: MapsTo_def MakeCat_def)

lemma MakeCatObj: "obj _C = obj"
by (simp add: MakeCat_def)

lemma MakeCatMor: "mor _C = mor"
by (simp add: MakeCat_def)

lemma MakeCatDom: "f ∈ mor ==> dom f = dom _C f"
by (simp add: MakeCat_def)

lemma MakeCatCod: "f ∈ mor ==> cod f = cod _C f"
by (simp add: MakeCat_def)


lemma MakeCatCompDef: "f ≈> _C g = f ≈> g"
by (auto simp add: CompDefined_def MakeCat_def)

lemma MakeCatComp2: "f ≈> _C g ==> f ;; _C g = f ;; g"
by (simp add: MakeCatCompDef MakeCatComp)


lemma ExtCategoryMakeCat: "ExtCategory (MakeCat C)"
by (unfold_locales, simp_all add: MakeCat_def extensional_def CompDefined_def)

lemma MakeCat: "Category_axioms C ==> Category (MakeCat C)"
apply(intro_locales, simp add: ExtCategoryMakeCat)
apply (simp add: Category_axioms_def)
apply (auto simp add: MakeCat_def CompDefined_def MapsTo_def)
done

lemma MapsToE[elim]: "[f maps X to Y ; [f ∈ mor ; dom f = X ; cod f = Y] ==> R] ==> R"
  by (auto simp add: MapsTo_def)

lemma MapsToI[intro]: "[f ∈ mor ; dom f = X ; cod f = Y] ==> f maps X to Y"
  by (auto simp add: MapsTo_def)

lemma CompDefinedE[elim]: "[f ≈> g ; [f ∈ mor ; g ∈ mor ; cod f = dom g] ==> R] ==> R"
  by (auto simp add: CompDefined_def)

lemma CompDefinedI[intro]: "[f ∈ mor ; g ∈ mor ; cod f = dom g] ==> f ≈> g"
  by (auto simp add: CompDefined_def)

lemma (in Category) MapsToCompI: assumes "f ≈> g" shows "(f ;; g) maps (dom f) to (cod g)"
proof-
  have "f maps (dom f) to (dom g)" 
  and  "g maps (dom g) to (cod g)" using assms by auto
  thus ?thesis by (simp add: Ccompt[of f "dom f" "dom g" g "cod g"])
qed

lemma MapsToCompDef:
  assumes "f maps X to Y" and "g maps Y to Z"
  shows "f ≈> g"
proof(rule CompDefinedI)
  show "f ∈ mor" and "g ∈ mor" using assms by auto
  have "cod f = Y" and "dom g = Y" using assms by auto
  thus "cod f = dom g" by simp
qed

lemma (in Category) MapsToMorDomCod: 
  assumes "f ≈> g" 
  shows "f ;; g ∈ mor" and "dom (f ;; g) = dom f" and "cod (f ;; g) = cod g"
proof-
  have "(f ;; g) maps (dom f) to (cod g)" using assms by (simp add: MapsToCompI)
  thus "f ;; g ∈ mor" and "dom (f ;; g) = dom f" and "cod (f ;; g) = cod g" by auto
qed

lemma (in Category) MapsToObj: 
  assumes "f maps X to Y"
  shows "X ∈ obj" and "Y ∈ obj"
proof-
  have "dom f = X" and "cod f = Y" and "f ∈ mor" using assms by auto
  thus "X ∈ obj" and "Y ∈ obj" by (auto simp add: Cdom Ccod)
qed

lemma (in Category) IdInj: 
  assumes "X ∈ obj" and "Y ∈ obj" and "id X = id Y"
  shows   "X = Y"
proof-
  have "dom (id X) = dom (id Y)" using assms by simp
  moreover have "dom (id X) = X" and "dom (id Y) = Y" using assms by (auto simp add: MapsTo_def)
  ultimately show ?thesis by simp
qed

lemma (in Category) CompDefComp:
  assumes "f ≈> g" and "g ≈> h"
  shows "f ≈> (g ;; h)" and "(f ;; g) ≈> h"
proof(auto simp add: CompDefined_def)
  show "f ∈ mor" and "h ∈ mor" using assms by auto
  have  1: "g ;; h maps (dom g) to (cod h)" 
    and 2: "f ;; g maps (dom f) to (cod g)" using assms by (simp add: MapsToCompI)+
  thus "g ;; h ∈ mor" and "f ;; g ∈ mor" by auto
  have "cod f = dom g" using assms by auto
  also have "... = dom (g ;; h)" using 1 by auto
  finally show "cod f = dom (g ;; h)" .
  have "dom h = cod g" using assms by auto
  also have "... = cod (f ;; g)" using 2 by auto
  finally show "cod (f ;; g) = dom h" by simp
qed

lemma (in Category) CatIdInMor: "X ∈ obj ==> id X ∈ mor"
by (auto simp add: Cidm)

lemma (in Category) MapsToId: assumes "X ∈ obj" shows "id X ≈> id X"
proof(rule CompDefinedI)
  have "id X maps X to X" using assms by (simp add: Cidm)
  thus "id X ∈ mor" and "id X ∈ mor" and "cod (id X) = dom (id X)" by auto
qed

lemmas (in Category) Simps = Cdom Ccod Cidm Cidl Cidr MapsToCompI IdInj MapsToId

lemma (in Category) LeftRightInvUniq: 
  assumes 0: "h ≈> f" and  z: "f ≈> g"
  assumes 1: "f ;; g = id (dom f)" 
  and     2: "h ;; f = id (cod f)"
  shows   "h = g"
proof-
  have mor: "h ∈ mor ∧ g ∈ mor" 
  and  dc : "dom f = cod h ∧ cod f = dom g" using 0 z by auto
  then have "h = h ;; id (dom f)" by (auto simp add: Simps)
  also have "... = h ;; (f ;; g)" using 1 by simp+
  also have "... = (h ;; f) ;; g" using 0 z by (simp add: Cassoc)
  also have "... = (id (cod f)) ;; g" using 2 by simp+
  also have "... = g" using mor dc by (auto simp add: Simps)
  finally show ?thesis .
qed

lemma (in Category) CatIdDomCod:
  assumes "X ∈ obj"
  shows "dom (id X) = X" and "cod (id X) = X"
proof-
  have "id X maps X to X" using assms
    by (simp add: Simps)
  thus "dom (id X) = X" and "cod (id X) = X" by auto
qed

lemma (in Category) CatIdCompId:
  assumes "X ∈ obj"
  shows   "id X ;; id X = id X"
proof-
  have 0: "id X ∈ mor" using assms by (auto simp add: Simps)
  moreover have "cod (id X) = X" using assms by auto
  moreover have "id X ;; id (cod (id X)) = id X" using 0 by (simp add: Simps)
  ultimately show ?thesis by simp
qed

(*lemmas (in Category) simps2 = simps CatIdCompId Cassoc CatIdDomCod*)

lemma (in Category) CatIdUniqR: 
  assumes iota: "ι maps X to X"
  and     rid:  "∀ f . f ≈> ι ⟶ f ;; ι = f"
  shows "id X = ι"
proof(rule LeftRightInvUniq [of "id X" "id X" ι ])
  have 0: "X ∈ obj" using iota by (auto simp add: Simps)
  hence "id X maps X to X" by (simp add: Cidm)
  thus 1: "id X ≈> ι" using iota by (auto simp add: Simps)
  show    "id X ≈> id X" using 0 by (auto simp add: Simps)
  show    "(id X) ;; ι = (id (dom (id X)))" using 0 1 rid by (auto simp add: Simps CompDefined_def MapsTo_def)
  show    "(id X) ;; (id X) = (id (cod (id X)))" using 0 by (auto simp add: CatIdCompId CompDefined_def MapsTo_def)
qed
  
definition
  inverse_rel :: "('o,'m,'a) Category_scheme → 'm → 'm → bool" (‹cinvı _ _› 60) where
  "inverse_rel C f g ≡ (f ≈> g) ∧ (f ;; g) = (id (dom f)) ∧ (g ;; f) = (id (cod f))"

definition 
  isomorphism :: "('o,'m,'a) Category_scheme → 'm → bool" (‹cisoı _› [70]) where
  "isomorphism C f ≡ ∃ g . inverse_rel C f g"

lemma (in Category) Inverse_relI: "[f ≈> g ; f ;; g = id (dom f) ; g ;; f = id (cod f)] ==> (cinv f g)"
by (auto simp add: inverse_rel_def)

lemma (in Category) Inverse_relE[elim]: "[cinv f g ; [f ≈> g ; f ;; g = id (dom f) ; g ;; f = id (cod f)] ==> P] ==> P"
by (auto simp add: inverse_rel_def)

lemma (in Category) Inverse_relSym: 
  assumes "cinv f g"
  shows   "cinv g f"
proof(rule Inverse_relI)
  have 1: "f ≈> g" using assms by auto
  show 2: "g ≈> f"
  proof(rule CompDefinedI)
    show "g ∈ mor" and 0: "f ∈ mor" using assms by auto
    have "f ;; g maps dom f to cod g" using 1 by (simp add: MapsToCompI)
    hence "cod g = cod (f ;; g)" by auto
    also have "... = cod (id (dom f))" using assms by (auto simp add: inverse_rel_def)
    also have "... = dom f"
    proof-
      have "dom f ∈ obj" using 0 by (simp add: Simps)
      hence "id (dom f) maps (dom f) to (dom f)" by (simp add: Simps)
      thus ?thesis by auto
    qed
    finally show 2: "cod g = dom f" by simp
  qed
  show "g ;; f = id (dom g)" using assms by (auto simp add: inverse_rel_def)
  show "f ;; g = id (cod g)"using assms 1 2 by (auto simp add: inverse_rel_def)
qed

lemma (in Category) InverseUnique: 
  assumes 1: "cinv f g"
  and     2: "cinv f h"
  shows   "g = h"
proof(rule LeftRightInvUniq [of g f h])
  have "cinv g f" using 1 2 by (simp only: Inverse_relSym[of f g])
  thus "g ≈> f" and
    "g ;; f = id (cod f)" using 1 by auto
  show "f ≈> h" using 2 by auto
  show "f ;; h = id (dom f)" using 2 by auto
qed

lemma (in Category) InvId: assumes "X ∈ obj" shows "(cinv (id X) (id X))"
proof(rule Inverse_relI)
  show "id X ≈> id X" using assms by (simp add: Simps)
  have "dom (id X) = X" and "dom (id X) = X" using assms by (simp add: CatIdDomCod)+
  thus "id X ;; id X = id (dom (id X))" and "id X ;; id X = id (cod (id X))" 
    using assms by (simp add: CatIdCompId CatIdDomCod)+
qed
    
definition
  inverse :: "('o,'m,'a) Category_scheme → 'm → 'm" (‹Cinvı _› [70]) where
  "inverse C f ≡ THE g . inverse_rel C f g"

lemma (in Category) inv2Inv:
  assumes "cinv f g"
  shows   "ciso f" and "Cinv f = g"
proof-
  show "ciso f" using assms by (auto simp add: isomorphism_def)
  hence "∃! g . cinv f g" using assms by (auto simp add: InverseUnique)
  thus "Cinv f = g" using assms by (auto simp add: inverse_def)
qed

lemma (in Category) iso2Inv:
  assumes "ciso f"
  shows   "cinv f (Cinv f)"
proof-
  have "∃! g . cinv f g" using assms by (auto simp add: InverseUnique isomorphism_def)
  thus ?thesis by (auto simp add:  inverse_def intro:theI')
qed

lemma (in Category) InvInv:
  assumes "ciso f" 
  shows   "ciso (Cinv f)" and "(Cinv (Cinv f)) = f"
proof-
  have "cinv f (Cinv f)" using assms by (simp add: iso2Inv)
  hence "cinv (Cinv f) f" by (simp add: Inverse_relSym[of f])
  thus  "ciso (Cinv f)" and "Cinv (Cinv f) = f" by (auto simp add: inv2Inv)
qed

lemma (in Category) InvIsMor: "(cinv f g) ==> (f ∈ mor ∧ g ∈ mor)"
  by (auto simp add: inverse_rel_def)

lemma (in Category) IsoIsMor: "ciso f ==> f ∈ mor"
  by (auto simp add: InvIsMor dest: iso2Inv)

lemma (in Category) InvDomCod:
  assumes "ciso f"
  shows "dom (Cinv f) = cod f" and "cod (Cinv f) = dom f" and "Cinv f ∈ mor"
proof-
  have 1: "cinv f (Cinv f)" using assms by (auto simp add: iso2Inv)
  thus "dom (Cinv f) = cod f" by (auto simp add: inverse_rel_def)
  from 1 have "cinv (Cinv f) f" by (auto simp add: Inverse_relSym[of f])
  thus  "cod (Cinv f) = dom f" by (auto simp add: inverse_rel_def)
  show "Cinv f ∈ mor" using 1 by (auto simp add: inverse_rel_def)
qed

lemma (in Category) IsoCompInv: "ciso f ==> f ≈> Cinv f"
  by (auto simp add: IsoIsMor InvDomCod)

lemma (in Category) InvCompIso: "ciso f ==> Cinv f ≈> f"
  by (auto simp add: IsoIsMor InvDomCod)

lemma (in Category) IsoInvId1 : "ciso f ==> (Cinv f) ;; f = (id (cod f))"
by (auto dest: iso2Inv)

lemma (in Category) IsoInvId2 :  "ciso f ==> f ;; (Cinv f) = (id (dom f))"
by (auto dest: iso2Inv)

lemma (in Category) IsoCompDef:
  assumes 1: "f ≈> g" and 2: "ciso f" and 3: "ciso g"
  shows "(Cinv g) ≈> (Cinv f)"
proof(rule CompDefinedI)
  show "Cinv g ∈ mor" and "Cinv f ∈ mor" using assms by (auto simp add: InvDomCod)
  have "cod (Cinv g) = dom g" using 3 by (simp add: InvDomCod)
  also have "... = cod f" using 1 by auto
  also have "... = dom (Cinv f)" using 2 by (simp add: InvDomCod)
  finally show "cod (Cinv g) = dom (Cinv f)" .
qed

lemma (in Category) IsoCompose: 
  assumes 1: "f ≈> g" and 2: "ciso f" and 3: "ciso g"
  shows "ciso (f ;; g)" and "Cinv (f ;; g) = (Cinv g) ;; (Cinv f)"
proof-
  have  a: "(Cinv g) ≈> (Cinv f)" using assms by (simp add: IsoCompDef)
  hence b: "(Cinv g) ;; (Cinv f) maps (dom (Cinv g)) to (cod (Cinv f))" by (simp add: MapsToCompI)
  hence c: "(Cinv g) ;; (Cinv f) maps (cod g) to (dom f)" using 2 3 by (simp add: InvDomCod) 
  have  d: "f ;; g maps (dom f) to (cod g)" using 1 by (simp add: Simps)
  have "cinv (f ;; g) ((Cinv g) ;; (Cinv f))"
  proof(auto simp add: inverse_rel_def)
    show "f ;; g ≈> (Cinv g) ;; (Cinv f)"
    proof(rule CompDefinedI)
      show "f ;; g ∈ mor" using d by auto
      show "(Cinv g) ;; (Cinv f) ∈ mor" using c by auto
      have "cod (f ;; g) = cod g" using d by auto
      also have "... = dom (Cinv g)" using assms by (simp add: InvDomCod)
      also have "... = dom ((Cinv g) ;; (Cinv f))" using b by auto
      finally show "cod (f ;; g) = dom ((Cinv g) ;; (Cinv f))" .
    qed
    show "f ;; g ;; ((Cinv g) ;; (Cinv f)) = id (dom (f ;; g))"
    proof-
      have e: "g ≈> (Cinv g)" using assms by (simp add: IsoCompInv)
      have f: "f ∈ mor" using 1 by auto
      have "(f ;; g) ;; ((Cinv g) ;; (Cinv f)) = (f ;; (g ;; (Cinv g))) ;; (Cinv f)" 
        using 1 e a by (auto simp add: Cassoc CompDefComp)
      also have "... = f ;; (id (dom g)) ;; (Cinv f)" using 3 by (simp add: IsoInvId2)
      also have "... = f ;; id (cod f) ;; (Cinv f)" using 1 by (auto simp add: Simps)
      also have "... = f ;; (Cinv f)" using f by (auto simp add: Cidr)
      also have "... = id (dom f)" using 2 by (simp add: IsoInvId2)
      also have "... = id (dom (f ;; g))" using d by auto
      finally show ?thesis by simp
    qed
    show "((Cinv g) ;; (Cinv f)) ;; (f ;; g) = id (cod (f ;; g))"
    proof-
      have e: "(Cinv f) ≈> f" using assms by (simp add: InvCompIso)
      have f: "g ∈ mor" using 1 by auto
      have "((Cinv g) ;; (Cinv f)) ;; (f ;; g) = (Cinv g) ;; (((Cinv f) ;; f) ;; g)"
        using 1 e a by (auto simp add: Cassoc CompDefComp)
      also have "... = (Cinv g) ;; ((id (cod f)) ;; g)" using 2 by (simp add: IsoInvId1)
      also have "... = (Cinv g) ;; ((id (dom g)) ;; g)" using 1 by (auto simp add: Simps)
      also have "... = (Cinv g) ;; g" using f by (auto simp add: Cidl)
      also have "... = id (cod g)" using 3 by (simp add: IsoInvId1)
      also have "... = id (cod (f ;; g))" using d by auto
      finally show ?thesis by simp
    qed
  qed
  thus "ciso (f ;; g)" and "Cinv (f ;; g) = (Cinv g) ;; (Cinv f)" by (auto simp add: inv2Inv)
qed

definition "ObjIso C A B ≡ ∃ k . (k maps A to B) ∧ ciso k"

definition 
  UnitCategory :: "(unit, unit) Category" where
  "UnitCategory = MakeCat (
      Obj = {()} ,
      Mor = {()} ,
      Dom = (λf.()) ,
      Cod = (λf.()) ,
      Id = (λf.()) ,
      Comp = (λf g. ())
  )"

lemma [simp]: "Category(UnitCategory)"
apply (simp add: UnitCategory_def, rule MakeCat)
by (unfold_locales, auto simp add: UnitCategory_def)

definition 
  OppositeCategory :: "('o,'m,'a) Category_scheme → ('o,'m,'a) Category_scheme" (‹Op _› [65] 65) where
  "OppositeCategory C ≡ (
      Obj = Obj C ,
      Mor = Mor C ,
      Dom = Cod C ,
      Cod = Dom C ,
      Id = Id C ,
      Comp = (λf g. g ;; f),
      … = Category.more C
  )"

lemma OpCatOpCat: "Op (Op C) = C"
  by (simp add: OppositeCategory_def)


lemma OpCatCatAx: "Category_axioms C ==> Category_axioms (Op C)"
  by (simp add: OppositeCategory_def Category_axioms_def MapsTo_def CompDefined_def)

lemma OpCatCatExt: "ExtCategory C ==> ExtCategory (Op C)"
  by (auto simp add: OppositeCategory_def ExtCategory_def MapsTo_def CompDefined_def extensional_def)

lemma OpCatCat: "Category C ==> Category (Op C)"
  by (intro_locales, simp_all add: Category_def OpCatCatAx OpCatCatExt)


lemma MapsToOp: "f maps X to Y ==> f maps _C Y to X"
by (simp add: MapsTo_def OppositeCategory_def)

lemma MapsToOpOp: "f maps _C X to Y ==> f maps Y to X"
by (simp add: MapsTo_def OppositeCategory_def)

lemma CompDefOp: "f ≈> g ==> g ≈> _C f"
by (simp add: CompDefined_def OppositeCategory_def)

end