Theory CZH_ECAT_Category

(* Copyright 2021 (C) Mihails Milehins *)

section‹Category›
theory CZH_ECAT_Category
  imports 
    CZH_ECAT_Introduction
    CZH_Foundations.CZH_SMC_Semicategory
begin



subsection‹Background›

lemmas [cat_cs_simps] = dg_shared_cs_simps
lemmas [cat_cs_intros] = dg_shared_cs_intros

definition CId :: V
  where [dg_field_simps]: "CId = 5"



subsubsection‹Slicing›

definition cat_smc :: "V  V"
  where "cat_smc  = [Obj, Arr, Dom, Cod, Comp]"


text‹Components.›

lemma cat_smc_components[slicing_simps]:
  shows "cat_smc Obj = Obj"
    and "cat_smc Arr = Arr"
    and "cat_smc Dom = Dom"
    and "cat_smc Cod = Cod"
    and "cat_smc Comp = Comp"
  unfolding cat_smc_def dg_field_simps by (auto simp: nat_omega_simps)


text‹Regular definitions.›

lemma cat_smc_is_arr[slicing_simps]: 
  "f : a cat_smc b  f : a b"
  unfolding is_arr_def slicing_simps ..

lemmas [slicing_intros] = cat_smc_is_arr[THEN iffD2]

lemma cat_smc_composable_arrs[slicing_simps]:
  "composable_arrs (cat_smc ) = composable_arrs "
  unfolding composable_arrs_def slicing_simps ..

lemma cat_smc_is_monic_arr[slicing_simps]: 
  "f : a moncat_smc b  f : a monb"
  unfolding is_monic_arr_def slicing_simps ..

lemmas [slicing_intros] = cat_smc_is_monic_arr[THEN iffD2]

lemma cat_smc_is_epic_arr[slicing_simps]: 
  "f : a epicat_smc b  f : a epib"
  unfolding is_epic_arr_def slicing_simps op_smc_def 
  by (simp add: nat_omega_simps)

lemmas [slicing_intros] = cat_smc_is_epic_arr[THEN iffD2]

lemma cat_smc_is_idem_arr[slicing_simps]:
  "f : idecat_smc b  f : ideb"
  unfolding is_idem_arr_def slicing_simps ..

lemmas [slicing_intros] = cat_smc_is_idem_arr[THEN iffD2]

lemma cat_smc_obj_terminal[slicing_simps]:
  "obj_terminal (cat_smc ) a  obj_terminal  a"
  unfolding obj_terminal_def slicing_simps ..

lemmas [slicing_intros] = cat_smc_obj_terminal[THEN iffD2]

lemma cat_smc_obj_intial[slicing_simps]:
  "obj_initial (cat_smc ) a  obj_initial  a"
  unfolding obj_initial_def obj_terminal_def 
  unfolding smc_op_simps slicing_simps
  ..

lemmas [slicing_intros] = cat_smc_obj_intial[THEN iffD2]

lemma cat_smc_obj_null[slicing_simps]: 
  "obj_null (cat_smc ) a  obj_null  a"
  unfolding obj_null_def slicing_simps smc_op_simps ..

lemmas [slicing_intros] = cat_smc_obj_null[THEN iffD2]

lemma cat_smc_is_zero_arr[slicing_simps]:
  "f : a 0cat_smc b  f : a 0b"
  unfolding is_zero_arr_def slicing_simps ..

lemmas [slicing_intros] = cat_smc_is_zero_arr[THEN iffD2]



subsection‹Definition and elementary properties›


text‹
The definition of a category that is used in this work is
is similar to the definition that can be found in Chapter I-2 in 
cite"mac_lane_categories_2010". The amendments to the definitions that are 
associated with size have already been explained in 
cite"milehins_category_2021".
›

locale category = 𝒵 α + vfsequence  + CId: vsv CId for α  +
  assumes cat_length[cat_cs_simps]: "vcard  = 6"
    and cat_semicategory[slicing_intros]: "semicategory α (cat_smc )"
    and cat_CId_vdomain[cat_cs_simps]: "𝒟 (CId) = Obj"
    and cat_CId_is_arr[cat_cs_intros]: "a  Obj  CIda : a a"
    and cat_CId_left_left[cat_cs_simps]: 
      "f : a b  CIdb Af = f"
    and cat_CId_right_left[cat_cs_simps]: 
      "f : b c  f ACIdb = f"

lemmas [cat_cs_simps] = 
  category.cat_length
  category.cat_CId_vdomain
  category.cat_CId_left_left
  category.cat_CId_right_left

lemma (in category) cat_CId_is_arr'[cat_cs_intros]:
  assumes "a  Obj" and "b = a" and "c = a" and "ℭ' = "
  shows "CIda : b ℭ'c"
  using assms(1) unfolding assms(2-4) by (rule cat_CId_is_arr)

lemmas [cat_cs_intros] = category.cat_CId_is_arr'

lemma (in category) cat_CId_is_arr''[cat_cs_intros]:
  assumes "a  Obj" and "f = CIda"
  shows "f : a a"
  using assms(1) 
  unfolding assms(2) 
  by (cs_concl cs_shallow cs_intro: cat_cs_intros)

lemmas [cat_cs_intros] = category.cat_CId_is_arr''

lemmas [slicing_intros] = category.cat_semicategory

lemma (in category) cat_CId_vrange: " (CId)  Arr"
proof
  fix f assume "f   (CId)"
  with cat_CId_vdomain obtain a where "a  Obj" and "f = CIda" 
    by (auto elim!: CId.vrange_atE)
  with cat_CId_is_arr show "f  Arr" by auto
qed


text‹Rules.›

lemma (in category) category_axioms'[cat_cs_intros]:
  assumes "α' = α"
  shows "category α' "
  unfolding assms by (rule category_axioms)

mk_ide rf category_def[unfolded category_axioms_def]
  |intro categoryI|
  |dest categoryD[dest]|
  |elim categoryE[elim]|

lemma categoryI':
  assumes "𝒵 α"
    and "vfsequence "
    and "vcard  = 6"
    and "vsv (Dom)"
    and "vsv (Cod)"
    and "vsv (Comp)"
    and "vsv (CId)"
    and "𝒟 (Dom) = Arr"
    and " (Dom)  Obj"
    and "𝒟 (Cod) = Arr"
    and " (Cod)  Obj"
    and "gf. gf  𝒟 (Comp) 
      (g f b c a. gf = [g, f]  g : b c  f : a b)"
    and "𝒟 (CId) = Obj"
    and "b c g a f.  g : b c; f : a b   g Af : a c"
    and "c d h b g a f.  h : c d; g : b c; f : a b  
      (h Ag) Af = h A(g Af)"
    and "a. a  Obj  CIda : a a"
    and "a b f. f : a b  CIdb Af = f"
    and "b c f. f : b c  f ACIdb = f"
    and "Obj  Vset α"
    and "A B.  A  Obj; B  Obj; A  Vset α; B  Vset α  
      (aA. bB. Hom  a b)  Vset α"
  shows "category α "
  by (intro categoryI semicategoryI', unfold cat_smc_components slicing_simps)
    (simp_all add: assms smc_dg_def nat_omega_simps cat_smc_def)

lemma categoryD':
  assumes "category α " 
  shows "𝒵 α"
    and "vfsequence "
    and "vcard  = 6"
    and "vsv (Dom)"
    and "vsv (Cod)"
    and "vsv (Comp)"
    and "vsv (CId)"
    and "𝒟 (Dom) = Arr"
    and " (Dom)  Obj"
    and "𝒟 (Cod) = Arr"
    and " (Cod)  Obj"
    and "gf. gf  𝒟 (Comp) 
      (g f b c a. gf = [g, f]  g : b c  f : a b)"
    and "𝒟 (CId) = Obj"
    and "b c g a f.  g : b c; f : a b   g Af : a c"
    and "c d h b g a f.  h : c d; g : b c; f : a b  
      (h Ag) Af = h A(g Af)"
    and "a. a  Obj  CIda : a a"
    and "a b f. f : a b  CIdb Af = f"
    and "b c f. f : b c  f ACIdb = f"
    and "Obj  Vset α"
    and "A B.  A  Obj; B  Obj; A  Vset α; B  Vset α  
      (aA. bB. Hom  a b)  Vset α"
  by 
    (
      simp_all add: 
        categoryD(2-9)[OF assms] 
        semicategoryD'[OF categoryD(5)[OF assms], unfolded slicing_simps]
    )

lemma categoryE':
  assumes "category α " 
  obtains "𝒵 α"
    and "vfsequence "
    and "vcard  = 6"
    and "vsv (Dom)"
    and "vsv (Cod)"
    and "vsv (Comp)"
    and "vsv (CId)"
    and "𝒟 (Dom) = Arr"
    and " (Dom)  Obj"
    and "𝒟 (Cod) = Arr"
    and " (Cod)  Obj"
    and "gf. gf  𝒟 (Comp) 
      (g f b c a. gf = [g, f]  g : b c  f : a b)"
    and "𝒟 (CId) = Obj"
    and "b c g a f.  g : b c; f : a b   g Af : a c"
    and "c d h b g a f.  h : c d; g : b c; f : a b  
      (h Ag) Af = h A(g Af)"
    and "a. a  Obj  CIda : a a"
    and "a b f. f : a b  CIdb Af = f"
    and "b c f. f : b c  f ACIdb = f"
    and "Obj  Vset α"
    and "A B.  A  Obj; B  Obj; A  Vset α; B  Vset α  
      (aA. bB. Hom  a b)  Vset α"
  using assms by (simp add: categoryD')


text‹Slicing.›

context category
begin

interpretation smc: semicategory α cat_smc  by (rule cat_semicategory)

sublocale Dom: vsv Dom 
  by (rule smc.Dom.vsv_axioms[unfolded slicing_simps])
sublocale Cod: vsv Cod 
  by (rule smc.Cod.vsv_axioms[unfolded slicing_simps])
sublocale Comp: pbinop Arr Comp
  by (rule smc.Comp.pbinop_axioms[unfolded slicing_simps])

lemmas_with [unfolded slicing_simps]:
  cat_Dom_vdomain[cat_cs_simps] = smc.smc_Dom_vdomain
  and cat_Dom_vrange = smc.smc_Dom_vrange
  and cat_Cod_vdomain[cat_cs_simps] = smc.smc_Cod_vdomain
  and cat_Cod_vrange = smc.smc_Cod_vrange
  and cat_Obj_vsubset_Vset = smc.smc_Obj_vsubset_Vset
  and cat_Hom_vifunion_in_Vset[cat_cs_intros] = smc.smc_Hom_vifunion_in_Vset
  and cat_Obj_if_Dom_vrange = smc.smc_Obj_if_Dom_vrange
  and cat_Obj_if_Cod_vrange = smc.smc_Obj_if_Cod_vrange
  and cat_is_arrD = smc.smc_is_arrD
  and cat_is_arrE[elim] = smc.smc_is_arrE
  and cat_in_ArrE[elim] = smc.smc_in_ArrE
  and cat_Hom_in_Vset[cat_cs_intros] = smc.smc_Hom_in_Vset
  and cat_Arr_vsubset_Vset = smc.smc_Arr_vsubset_Vset
  and cat_Dom_vsubset_Vset = smc.smc_Dom_vsubset_Vset
  and cat_Cod_vsubset_Vset = smc.smc_Cod_vsubset_Vset
  and cat_Obj_in_Vset = smc.smc_Obj_in_Vset
  and cat_in_Obj_in_Vset[cat_cs_intros] = smc.smc_in_Obj_in_Vset
  and cat_Arr_in_Vset = smc.smc_Arr_in_Vset
  and cat_in_Arr_in_Vset[cat_cs_intros] = smc.smc_in_Arr_in_Vset
  and cat_Dom_in_Vset = smc.smc_Dom_in_Vset
  and cat_Cod_in_Vset = smc.smc_Cod_in_Vset
  and cat_semicategory_if_ge_Limit = smc.smc_semicategory_if_ge_Limit
  and cat_Dom_app_in_Obj = smc.smc_Dom_app_in_Obj
  and cat_Cod_app_in_Obj = smc.smc_Cod_app_in_Obj
  and cat_Arr_vempty_if_Obj_vempty = smc.smc_Arr_vempty_if_Obj_vempty
  and cat_Dom_vempty_if_Arr_vempty = smc.smc_Dom_vempty_if_Arr_vempty
  and cat_Cod_vempty_if_Arr_vempty = smc.smc_Cod_vempty_if_Arr_vempty

lemmas [cat_cs_intros] = cat_is_arrD(2,3)

lemmas_with [unfolded slicing_simps slicing_commute]:
  cat_Comp_vdomain = smc.smc_Comp_vdomain
  and cat_Comp_is_arr[cat_cs_intros] = smc.smc_Comp_is_arr
  and cat_Comp_assoc[cat_cs_intros] = smc.smc_Comp_assoc
  and cat_Comp_vdomainI[cat_cs_intros] = smc.smc_Comp_vdomainI
  and cat_Comp_vdomainE[elim!] = smc.smc_Comp_vdomainE
  and cat_Comp_vdomain_is_composable_arrs = 
    smc.smc_Comp_vdomain_is_composable_arrs
  and cat_Comp_vrange = smc.smc_Comp_vrange
  and cat_Comp_vsubset_Vset = smc.smc_Comp_vsubset_Vset
  and cat_Comp_in_Vset = smc.smc_Comp_in_Vset
  and cat_Comp_vempty_if_Arr_vempty = smc.smc_Comp_vempty_if_Arr_vempty
  and cat_assoc_helper = smc.smc_assoc_helper
  and cat_pattern_rectangle_right = smc.smc_pattern_rectangle_right
  and cat_pattern_rectangle_left = smc.smc_pattern_rectangle_left
  and is_epic_arrI = smc.is_epic_arrI
  and is_epic_arrD[dest] = smc.is_epic_arrD
  and is_epic_arrE[elim!] = smc.is_epic_arrE
  and cat_comp_is_monic_arr[cat_arrow_cs_intros] = smc.smc_Comp_is_monic_arr
  and cat_comp_is_epic_arr[cat_arrow_cs_intros] = smc.smc_Comp_is_epic_arr
  and cat_comp_is_monic_arr_is_monic_arr =
    smc.smc_Comp_is_monic_arr_is_monic_arr
  and cat_is_zero_arr_comp_right[cat_arrow_cs_intros] = 
    smc.smc_is_zero_arr_Comp_right
  and cat_is_zero_arr_comp_left[cat_arrow_cs_intros] = 
    smc.smc_is_zero_arr_Comp_left

lemma cat_Comp_is_arr'[cat_cs_intros]:
  assumes "g : b c"
    and "f : a b"
    and "ℭ' = "
  shows "g Af : a ℭ'c"
  using assms(1,2) unfolding assms(3) by (rule cat_Comp_is_arr)

end

lemmas [cat_cs_simps] = is_idem_arrD(2)

lemmas [cat_cs_simps] = category.cat_Comp_assoc

lemmas [cat_cs_intros] =
  category.cat_Comp_vdomainI
  category.cat_Hom_in_Vset
  category.cat_is_arrD(1-3)
  category.cat_Comp_is_arr'
  category.cat_Comp_is_arr

lemmas [cat_arrow_cs_intros] = 
  is_monic_arrD(1) 
  is_epic_arr_is_arr
  category.cat_comp_is_monic_arr
  category.cat_comp_is_epic_arr
  category.cat_is_zero_arr_comp_right
  category.cat_is_zero_arr_comp_left

lemmas [cat_cs_intros] = HomI
lemmas [cat_cs_simps] = in_Hom_iff


text‹Elementary properties.›

lemma cat_eqI:
  assumes "category α 𝔄" 
    and "category α 𝔅"
    and "𝔄Obj = 𝔅Obj"
    and "𝔄Arr = 𝔅Arr"
    and "𝔄Dom = 𝔅Dom"
    and "𝔄Cod = 𝔅Cod"
    and "𝔄Comp = 𝔅Comp"
    and "𝔄CId = 𝔅CId"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔅: category α 𝔅 by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟 𝔄 = 6" 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
    show "𝒟 𝔄 = 𝒟 𝔅" 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
    show "a  𝒟 𝔄  𝔄a = 𝔅a" for a 
      by (unfold dom, elim_in_numeral, insert assms) (auto simp: dg_field_simps)
  qed auto
qed

lemma cat_smc_eqI:
  assumes "category α 𝔄"
    and "category α 𝔅"
    and "𝔄CId = 𝔅CId"
    and "cat_smc 𝔄 = cat_smc 𝔅"
  shows "𝔄 = 𝔅"
proof(rule cat_eqI[of α])
  from assms(4) have 
    "cat_smc 𝔄Obj = cat_smc 𝔅Obj"
    "cat_smc 𝔄Arr = cat_smc 𝔅Arr"
    "cat_smc 𝔄Dom = cat_smc 𝔅Dom"
    "cat_smc 𝔄Cod = cat_smc 𝔅Cod" 
    "cat_smc 𝔄Comp = cat_smc 𝔅Comp" 
    by auto
  then show
    "𝔄Obj = 𝔅Obj"
    "𝔄Arr = 𝔅Arr"
    "𝔄Dom = 𝔅Dom"
    "𝔄Cod = 𝔅Cod"
    "𝔄Comp = 𝔅Comp" 
    unfolding slicing_simps by simp_all
qed (auto simp: assms)

lemma (in category) cat_def: 
  " = [Obj, Arr, Dom, Cod, Comp, CId]"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟  = 6" 
    by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
  have dom_rhs: "𝒟 [Obj, Arr, Dom, Cod, Comp, CId] = 6"
    by (simp add: nat_omega_simps)
  then show "𝒟  = 𝒟 [Obj, Arr, Dom, Cod, Comp, CId]"
    unfolding dom_lhs dom_rhs by simp
  show "a  𝒟  
    a = [Obj, Arr, Dom, Cod, Comp, CId]a" 
    for a
    unfolding dom_lhs
    by elim_in_numeral (simp_all add: dg_field_simps nat_omega_simps)
qed auto


text‹Size.›

lemma (in category) cat_CId_vsubset_Vset: "CId  Vset α"
proof(intro vsubsetI)
  fix af assume "af  CId"
  then obtain a f 
    where af_def: "af = a, f" 
      and a: "a  𝒟 (CId)" 
      and f: "f   (CId)"
    by (auto elim: CId.vbrelation_vinE)
  from a have "a  Vset α" by (auto simp: cat_cs_simps intro: cat_cs_intros)
  from f cat_CId_vrange have "f  Arr" by auto
  then have "f  Vset α" by (auto simp: cat_cs_simps intro: cat_cs_intros)
  then show "af  Vset α" 
    by (simp add: af_def Limit_vpair_in_VsetI a  Vset α)
qed

lemma (in category) cat_category_in_Vset_4: "  Vset (α + 4)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
    cat_Obj_vsubset_Vset
    cat_Arr_vsubset_Vset
    cat_Dom_vsubset_Vset
    cat_Cod_vsubset_Vset
    cat_Comp_vsubset_Vset
    cat_CId_vsubset_Vset
  show ?thesis
    by (subst cat_def, succ_of_numeral)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps 
          cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma (in category) cat_CId_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "CId  Vset β"
proof-
  interpret 𝒵 β by (rule assms(1))
  from assms have "𝒟 (CId)  Vset β" 
    by (auto simp: cat_cs_simps cat_Obj_in_Vset)
  moreover from assms cat_CId_vrange have " (CId)  Vset β"  
    by (auto intro: cat_Arr_in_Vset)
  ultimately show ?thesis by (blast intro: 𝒵_Limit_αω)
qed

lemma (in category) cat_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "  Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  show ?thesis
  proof(rule vsv.vsv_Limit_vsv_in_VsetI)
    have dom: "𝒟  = 6" 
      by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
    from assms show "𝒟   Vset β"
      unfolding dom by (simp add: 𝒵.ord_of_nat_in_Vset)
    have "n  𝒟   n  Vset β" for n
      unfolding dom
      by 
        (
          elim_in_numeral, 
          allrewrite in "  _" dg_field_simps[symmetric],
          insert assms
        )
        (
          auto simp:
            cat_Obj_in_Vset
            cat_Arr_in_Vset
            cat_Dom_in_Vset
            cat_Cod_in_Vset
            cat_Comp_in_Vset
            cat_CId_in_Vset
        )
    then show "   Vset β" by (metis vsubsetI vrange_atD)
    show "vfinite (𝒟 )" unfolding dom by auto
  qed (simp_all add: 𝒵_Limit_αω vsv_axioms)
qed

lemma (in category) cat_category_if_ge_Limit:
  assumes "𝒵 β" and "α  β"
  shows "category β "
  by (rule categoryI)
    (
      auto 
        intro: cat_cs_intros 
        simp: cat_cs_simps assms vfsequence_axioms cat_semicategory_if_ge_Limit 
    )

lemma tiny_category[simp]: "small {. category α }"
proof(cases 𝒵 α)
  case True
  from category.cat_in_Vset[of α] show ?thesis
    by (intro down[of _ Vset (α + ω)])
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{. category α } = {}" by auto
  then show ?thesis by simp
qed

lemma (in 𝒵) categories_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "set {. category α }  Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "set {. category α }  Vset (α + 4)"
  proof(intro vsubsetI)
    fix  assume prems: "  set {. category α }"
    interpret category α  using prems by simp
    show "  Vset (α + 4)"
      unfolding VPow_iff by (rule cat_category_in_Vset_4)
  qed
  from assms(2) show "Vset (α + 4)  Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma category_if_category:
  assumes "category β "
    and "𝒵 α"
    and "Obj  Vset α"
    and "A B.  A  Obj; B  Obj; A  Vset α; B  Vset α  
      (aA. bB. Hom  a b)  Vset α"
  shows "category α "
proof-
  interpret category β  by (rule assms(1))
  interpret α: 𝒵 α by (rule assms(2))
  show ?thesis
  proof(intro categoryI)
    show "vfsequence " by (simp add: vfsequence_axioms)
    show "semicategory α (cat_smc )"
      by (rule semicategory_if_semicategory, unfold slicing_simps)
        (auto intro!: assms(1,3,4) slicing_intros)
  qed (auto intro: cat_cs_intros simp: cat_cs_simps)
qed


text‹Further elementary properties.›

sublocale category  CId: v11 CId
proof(rule vsv.vsv_valeq_v11I, unfold cat_cs_simps)
  fix a b assume prems:
    "a  Obj" "b  Obj" "CIda = CIdb"
  have "CIda : b b" "CIda : a a"  
    by (subst prems(3))
      (cs_concl cs_simp: cat_cs_simps cs_intro: prems(1,2) cat_cs_intros)+
  with prems show "a = b" by auto (*slow*)
qed auto

lemma (in category) cat_CId_vempty_if_Arr_vempty:
  assumes "Arr = 0"
  shows "CId = 0"
  using assms cat_CId_vrange by (auto intro: CId.vsv_vrange_vempty)



subsection‹Opposite category›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-2 in cite"mac_lane_categories_2010".›

definition op_cat :: "V  V"
  where "op_cat  = [Obj, Arr, Cod, Dom, fflip (Comp), CId]"


text‹Components.›

lemma op_cat_components:
  shows [cat_op_simps]: "op_cat Obj = Obj"
    and [cat_op_simps]: "op_cat Arr = Arr"
    and [cat_op_simps]: "op_cat Dom = Cod"
    and [cat_op_simps]: "op_cat Cod = Dom"
    and "op_cat Comp = fflip (Comp)"
    and [cat_op_simps]: "op_cat CId = CId"
  unfolding op_cat_def dg_field_simps by (auto simp: nat_omega_simps)

lemma op_cat_component_intros[cat_op_intros]:
  shows "a  Obj  a  op_cat Obj"
    and "f  Arr  f  op_cat Arr"
  unfolding cat_op_simps by simp_all


text‹Slicing.›

lemma cat_smc_op_cat[slicing_commute]: "op_smc (cat_smc ) = cat_smc (op_cat )"
  unfolding cat_smc_def op_cat_def op_smc_def dg_field_simps
  by (simp add: nat_omega_simps)

lemma (in category) op_smc_op_cat[cat_op_simps]: "op_smc (op_cat ) = cat_smc "
  using Comp.pbinop_fflip_fflip
  unfolding op_smc_def op_cat_def cat_smc_def dg_field_simps
  by (simp add: nat_omega_simps)

lemma op_cat_is_arr[cat_op_simps]: "f : b op_cat a  f : a b"
  unfolding cat_op_simps is_arr_def by auto

lemmas [cat_op_intros] = op_cat_is_arr[THEN iffD2]

lemma op_cat_Hom[cat_op_simps]: "Hom (op_cat ) a b = Hom  b a"
  unfolding cat_op_simps by simp

lemma op_cat_obj_initial[cat_op_simps]: 
  "obj_initial (op_cat ) a  obj_terminal  a"
  unfolding obj_initial_def obj_terminal_def 
  unfolding smc_op_simps cat_op_simps 
  ..

lemmas [cat_op_intros] = op_cat_obj_initial[THEN iffD2]

lemma op_cat_obj_terminal[cat_op_simps]: 
  "obj_terminal (op_cat ) a  obj_initial  a"
  unfolding obj_initial_def obj_terminal_def 
  unfolding smc_op_simps cat_op_simps 
  ..

lemmas [cat_op_intros] = op_cat_obj_terminal[THEN iffD2]

lemma op_cat_obj_null[cat_op_simps]: "obj_null (op_cat ) a  obj_null  a"
  unfolding obj_null_def cat_op_simps by auto

lemmas [cat_op_intros] = op_cat_obj_null[THEN iffD2]

context category
begin

interpretation smc: semicategory α cat_smc  by (rule cat_semicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
  op_cat_Comp_vrange[cat_op_simps] = smc.op_smc_Comp_vrange
  and op_cat_Comp[cat_op_simps] = smc.op_smc_Comp
  and op_cat_is_epic_arr[cat_op_simps] = smc.op_smc_is_epic_arr
  and op_cat_is_monic_arr[cat_op_simps] = smc.op_smc_is_monic_arr
  and op_cat_is_zero_arr[cat_op_simps] = smc.op_smc_is_zero_arr

end

lemmas [cat_op_simps] = 
  category.op_cat_Comp_vrange
  category.op_cat_Comp
  category.op_cat_is_epic_arr
  category.op_cat_is_monic_arr
  category.op_cat_is_zero_arr

context
  fixes  :: V
begin

lemmas_with [
  where=cat_smc , unfolded slicing_simps slicing_commute[symmetric]
  ]:   
  op_cat_Comp_vdomain[cat_op_simps] = op_smc_Comp_vdomain

end


text‹Elementary properties.›

lemma op_cat_vsv[cat_op_intros]: "vsv (op_cat )" unfolding op_cat_def by auto


subsubsection‹Further properties›

lemma (in category) category_op[cat_cs_intros]: "category α (op_cat )"
proof(intro categoryI, unfold cat_op_simps)
  show "vfsequence (op_cat )" unfolding op_cat_def by simp
  show "vcard (op_cat ) = 6" 
    unfolding op_cat_def by (simp add: nat_omega_simps)
next
  fix f a b assume "f : b a"
  with category_axioms show "CIdb Aop_cat f = f"
    by (cs_concl cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
next
  fix f b c assume "f : c b" 
  with category_axioms show "f Aop_cat CIdb = f"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
      )
qed 
  (
    auto simp:
      cat_cs_simps 
      cat_op_simps 
      slicing_commute[symmetric] 
      smc_op_intros 
      cat_cs_intros
      cat_semicategory 
  )

lemmas category_op[cat_op_intros] = category.category_op

lemma (in category) cat_op_cat_op_cat[cat_op_simps]: "op_cat (op_cat ) = "
proof(rule cat_eqI, unfold cat_op_simps op_cat_components)
  show "category α (op_cat (op_cat ))" 
    by (simp add: category.category_op category_op)
  show "fflip (fflip (Comp)) = Comp" by (rule Comp.pbinop_fflip_fflip)
qed (auto simp: cat_cs_intros)

lemmas cat_op_cat_op_cat[cat_op_simps] = category.cat_op_cat_op_cat

lemma eq_op_cat_iff[cat_op_simps]: 
  assumes "category α 𝔄" and "category α 𝔅"
  shows "op_cat 𝔄 = op_cat 𝔅  𝔄 = 𝔅"
proof
  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔅: category α 𝔅 by (rule assms(2))
  assume prems: "op_cat 𝔄 = op_cat 𝔅"
  show "𝔄 = 𝔅"
  proof(rule cat_eqI)
    show 
      "𝔄Obj = 𝔅Obj" 
      "𝔄Arr = 𝔅Arr" 
      "𝔄Dom = 𝔅Dom"
      "𝔄Cod = 𝔅Cod"
      "𝔄Comp = 𝔅Comp"
      "𝔄CId = 𝔅CId"
      by (metis 𝔄.cat_op_cat_op_cat 𝔅.cat_op_cat_op_cat prems)+
  qed (auto intro: cat_cs_intros)
qed auto



subsection‹Monic arrow and epic arrow›

lemma (in category) cat_CId_is_monic_arr[cat_arrow_cs_intros]: 
  assumes "a  Obj" 
  shows "CIda : a mona"
  using assms cat_CId_is_arr' cat_CId_left_left by (force intro!: is_monic_arrI)

lemmas [cat_arrow_cs_intros] = category.cat_CId_is_monic_arr

lemma (in category) cat_CId_is_epic_arr[cat_arrow_cs_intros]: 
  assumes "a  Obj" 
  shows "CIda : a epia"
proof-
  from assms have "a  op_cat Obj" unfolding cat_op_simps .
  from category.cat_CId_is_monic_arr[OF category_op this, unfolded cat_op_simps]
  show ?thesis.
qed

lemmas [cat_arrow_cs_intros] = category.cat_CId_is_epic_arr



subsection‹Right inverse and left inverse of an arrow›


text‹See Chapter I-5 in cite"mac_lane_categories_2010".›

definition is_right_inverse :: "V  V  V  bool"
  where "is_right_inverse  g f = 
    (a b. g : b a  f : a b  f Ag = CIdb)"

definition is_left_inverse :: "V  V  V  bool"
  where "is_left_inverse   is_right_inverse (op_cat )"


text‹Rules.›

lemma is_right_inverseI:
  assumes "g : b a" and "f : a b" and "f Ag = CIdb"
  shows "is_right_inverse  g f"
  using assms unfolding is_right_inverse_def by auto

lemma is_right_inverseD[dest]:
  assumes "is_right_inverse  g f"
  shows "a b. g : b a  f : a b  f Ag = CIdb"
  using assms unfolding is_right_inverse_def by clarsimp

lemma is_right_inverseE[elim]:
  assumes "is_right_inverse  g f"
  obtains a b where "g : b a" 
    and "f : a b" 
    and "f Ag = CIdb"
  using assms by auto

lemma (in category) is_left_inverseI:
  assumes "g : b a" and "f : a b" and "g Af = CIda"
  shows "is_left_inverse  g f"
proof-
  from assms(3) have "f Aop_cat g = CIda"
    unfolding op_cat_Comp[OF assms(1,2)].
  from 
    is_right_inverseI[of op_cat , unfolded cat_op_simps, OF assms(1,2) this]
  show ?thesis
    unfolding is_left_inverse_def .
qed

lemma (in category) is_left_inverseD[dest]:
  assumes "is_left_inverse  g f"
  shows "a b. g : b a  f : a b  g Af = CIda"
proof-
  from is_right_inverseD[OF assms[unfolded is_left_inverse_def]] obtain a b
    where "g : b op_cat a" 
      and "f : a op_cat b" 
      and fg: "f Aop_cat g = op_cat CIdb"
    by clarsimp
  then have g: "g : a b" and f: "f : b a"
    unfolding cat_op_simps by simp_all
  moreover from fg have "g Af = CIdb"
    unfolding op_cat_Comp[OF g f] cat_op_simps by simp
  ultimately show ?thesis by blast  
qed

lemma (in category) is_left_inverseE[elim]:
  assumes "is_left_inverse  g f"
  obtains a b where "g : b a" 
    and "f : a b" 
    and "g Af = CIda"
  using assms by auto


text‹Elementary properties.›

lemma (in category) op_cat_is_left_inverse[cat_op_simps]:
  "is_left_inverse (op_cat ) g f  is_right_inverse  g f"
  unfolding is_left_inverse_def is_right_inverse_def cat_op_simps by simp

lemmas [cat_op_simps] = category.op_cat_is_left_inverse

lemmas [cat_op_intros] = category.op_cat_is_left_inverse[THEN iffD2]

lemma (in category) op_cat_is_right_inverse[cat_op_simps]:
  "is_right_inverse (op_cat ) g f  is_left_inverse  g f"
  unfolding is_left_inverse_def is_right_inverse_def cat_op_simps by simp

lemmas [cat_op_simps] = category.op_cat_is_right_inverse

lemmas [cat_op_intros] = category.op_cat_is_right_inverse[THEN iffD2]



subsection‹Inverse of an arrow›


text‹See Chapter I-5 in cite"mac_lane_categories_2010".›

definition is_inverse :: "V  V  V  bool"
  where "is_inverse  g f =
    (
      a b.
        g : b a 
        f : a b 
        g Af = CIda 
        f Ag = CIdb
    )"


text‹Rules.›

lemma is_inverseI:
  assumes "g : b a"
    and "f : a b"
    and "g Af = CIda"
    and "f Ag = CIdb"
  shows "is_inverse  g f"
  using assms unfolding is_inverse_def by auto

lemma is_inverseD[dest]: 
  assumes "is_inverse  g f"
  shows 
    "(
      a b.
        g : b a 
        f : a b 
        g Af = CIda 
        f Ag = CIdb
    )"
  using assms unfolding is_inverse_def by auto

lemma is_inverseE[elim]:
  assumes "is_inverse  g f"
  obtains a b where "g : b a"
    and "f : a b"
    and "g Af = CIda"
    and "f Ag = CIdb"
  using assms by auto


text‹Elementary properties.›

lemma (in category) op_cat_is_inverse[cat_op_simps]: 
  "is_inverse (op_cat ) g f  is_inverse  g f"
  by (rule iffI; unfold is_inverse_def cat_op_simps) (metis op_cat_Comp)+

lemmas [cat_op_simps] = category.op_cat_is_inverse

lemmas [cat_op_intros] = category.op_cat_is_inverse[THEN iffD2]

lemma is_inverse_sym: "is_inverse  g f  is_inverse  f g"
  unfolding is_inverse_def by auto

lemma (in category) cat_is_inverse_eq:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "is_inverse  h f" and "is_inverse  g f"
  shows "h = g"
  using assms
proof(elim is_inverseE)
  fix a b a' b'
  assume prems: 
    "h : b a" 
    "f : a b" 
    "h Af = CIda"
    "f Ah = CIdb"
    "g : b' a'" 
    "f : a' b'" 
    "g Af = CIda'" 
  then have ab: "a' = a" "b' = b" by auto 
  from prems have gf: "g Af = CIda" and g: "g : b a" 
    unfolding ab by simp_all
  from prems(1) have "h = (g Af) Ah" 
    unfolding gf by (simp add: cat_cs_simps)
  also with category_axioms prems(1,2) g have " = g"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: prems(4) cat_cs_simps cs_intro: cat_cs_intros
      )
  finally show "h = g" by simp
qed

lemma is_inverse_Comp_CId_left:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "is_inverse  g' g" and "g : a b"
  shows "g' Ag = CIda"
  using assms by auto

lemma is_inverse_Comp_CId_right:
  assumes "is_inverse  g' g" and "g : a b"
  shows "g Ag' = CIdb"
  by (metis assms is_arrD(3) is_inverseE)

lemma (in category) cat_is_inverse_Comp:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes gbc[intro]: "g : b c"
    and fab[intro]: "f : a b"
    and g'g[intro]: "is_inverse  g' g"
    and f'f[intro]: "is_inverse  f' f"
  shows "is_inverse  (f' Ag') (g Af)"
proof-
  from g'g gbc f'f fab have g'cb: "g' : c b" and f'ba: "f' : b a"
    by (metis is_arrD(2,3) is_inverseD)+
  with assms have f'g': "f' Ag' : c a" and gf: "g Af : a c" 
    by (auto intro: cat_Comp_is_arr)
  have ff': "is_inverse  f f'" using assms by (simp add: is_inverse_sym)
  note [simp] = 
    cat_Comp_assoc[symmetric, OF f'g' gbc fab] 
    cat_Comp_assoc[OF f'ba g'cb gbc]
    is_inverse_Comp_CId_left[OF g'g gbc]
    cat_Comp_assoc[symmetric, OF gf f'ba g'cb]
    cat_Comp_assoc[OF gbc fab f'ba]
    is_inverse_Comp_CId_left[OF ff' f'ba]
    cat_CId_right_left[OF f'ba]
    cat_CId_right_left[OF gbc]
  show ?thesis 
    by (intro is_inverseI, rule f'g', rule gf) 
      (auto intro: is_inverse_Comp_CId_left is_inverse_Comp_CId_right)
qed

lemma (in category) cat_is_inverse_Comp':
  assumes "g : b c"
    and "f : a b"
    and "is_inverse  g' g"
    and "is_inverse  f' f"
    and "f'g' = f' Ag'"
    and "gf = g Af"
  shows "is_inverse  f'g' gf"
  using assms(1-4) unfolding assms(5,6) by (intro cat_is_inverse_Comp)

lemmas [cat_cs_intros] = category.cat_is_inverse_Comp'

lemma is_inverse_is_right_inverse[dest]:
  assumes "is_inverse  g f" 
  shows "is_right_inverse  g f"
  using assms by (auto intro: is_right_inverseI)

lemma (in category) cat_is_inverse_is_left_inverse[dest]:
  assumes "is_inverse  g f" 
  shows "is_left_inverse  g f"
proof-
  interpret op: category α op_cat  by (auto intro!: cat_cs_intros)
  from assms have "is_inverse (op_cat ) g f" by (simp add: cat_op_simps)
  from is_inverse_is_right_inverse[OF this] show ?thesis
    unfolding is_left_inverse_def .
qed

lemma (in category) cat_is_right_left_inverse_is_inverse:
  assumes "is_right_inverse  g f" "is_left_inverse  g f"
  shows "is_inverse  g f"
  using assms
proof(elim is_right_inverseE is_left_inverseE)
  fix a b c d assume prems:
    "g : b a"
    "f : a b"
    "f Ag = CIdb"
    "g : d c"
    "f : c d"
    "g Af = CIdc"
  then have dbca: "d = b" "c = a" by auto
  note [cat_cs_simps] = prems(3,6)[unfolded dbca]
  from prems(1,2) show "is_inverse  g f"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros is_inverseI
      )
qed



subsection‹Isomorphism›


text‹See Chapter I-5 in cite"mac_lane_categories_2010".›

definition is_iso_arr :: "V  V  V  V  bool"
  where "is_iso_arr  a b f 
    (f : a b  (g. is_inverse  g f))"

syntax "_is_iso_arr" :: "V  V  V  V  bool"
  (‹_ : _ isoı _› [51, 51, 51] 51)
translations "f : a isob"  "CONST is_iso_arr  a b f"


text‹Rules.›

lemma is_iso_arrI:
  assumes "f : a b" and "is_inverse  g f"
  shows "f : a isob"
  using assms unfolding is_iso_arr_def by auto

lemma is_iso_arrD[dest]:
  assumes "f : a isob"
  shows "f : a b" and "g. is_inverse  g f"
  using assms unfolding is_iso_arr_def by auto

lemma is_iso_arrE[elim]:
  assumes "f : a isob"
  obtains g where "f : a b" and "is_inverse  g f"
  using assms by force

lemma is_iso_arrE':
  assumes "f : a isob"
  obtains g where "g : b isoa"
    and "g Af = CIda"
    and "f Ag = CIdb"
proof-
  from assms obtain g where f: "f : a b" "is_inverse  g f" by auto
  then have "g : b a"
    and "f : a b"
    and gf: "g Af = CIda"
    and fg: "f Ag = CIdb"
    by auto
  then have g: "g : b isoa" 
    by (cs_concl cs_shallow cs_intro: is_inverseI is_iso_arrI)
  from that f g gf fg show ?thesis by simp
qed


text‹Elementary properties.›

lemma (in category) op_cat_is_iso_arr[cat_op_simps]:
  "f : b isoop_cat a  f : a isob"
  unfolding is_iso_arr_def cat_op_simps by simp

lemmas [cat_op_simps] = category.op_cat_is_iso_arr

lemmas [cat_op_intros] = category.op_cat_is_iso_arr[THEN iffD2]

lemma (in category) is_iso_arrI':
  assumes "f : a b" 
    and "g : b a"
    and "g Af = CIda"
    and "f Ag = CIdb"
  shows "f : a isob" and "g : b isoa"
proof-
  from assms have gf: "is_inverse  g f" by (auto intro: is_inverseI)
  from assms have fg: "is_inverse  f g" by (auto intro: is_inverseI)
  show "f : a isob" and "g : b isoa"
    by 
      (
        intro 
          is_iso_arrI[OF assms(1) gf]
          is_iso_arrI[OF assms(2) fg]
      )+
qed

lemma (in category) cat_is_inverse_is_iso_arr:
  assumes "f : a b" and "is_inverse  g f"
  shows "g : b isoa"
proof(intro is_iso_arrI is_inverseI) 
  from assms(2) obtain a' b' 
    where g: "g : b' a'"
      and f: "f : a' b'"
      and gf: "g Af = CIda'"
      and fg: "f Ag = CIdb'"
    by auto
  with assms(1) have a'b': "a' = a" "b' = b" by auto
  from g f gf fg show 
    "g : b a"
    "f : a b"
    "g : b a"
    "f Ag = CIdb"
    "g Af = CIda"
    unfolding a'b' by auto
qed

lemma (in category) cat_Comp_is_iso_arr[cat_arrow_cs_intros]:
  assumes "g : b isoc" and "f : a isob"
  shows "g Af : a isoc"
proof-
  from assms have [intro]: "g Af : a c" 
    by (auto intro: cat_cs_intros)
  from assms(1) obtain g' where g'g: "is_inverse  g' g" by force
  with assms(1) have [intro]: "g' : c b" 
    by (elim is_iso_arrE)
      (auto simp: is_iso_arrD cat_is_inverse_is_iso_arr)
  from assms(2) obtain f' where f'f: "is_inverse  f' f" by auto
  with assms(2) have [intro]: "f' : b a"
    by (elim is_iso_arrE)
      (auto simp: is_iso_arrD cat_is_inverse_is_iso_arr)
  have "f' Ag' : c a" by (auto intro: cat_cs_intros)
  from cat_is_inverse_Comp[OF _ _ g'g f'f] assms 
  have "is_inverse  (f' Ag') (g Af)" 
    by (elim is_iso_arrE) simp
  then show ?thesis by (auto intro: is_iso_arrI)
qed

lemmas [cat_arrow_cs_intros] = category.cat_Comp_is_iso_arr

lemma (in category) cat_CId_is_iso_arr: 
  assumes "a  Obj" 
  shows "CIda : a isoa"
  using assms 
  by 
    (
      cs_concl cs_shallow 
        cs_intro: cat_cs_intros is_inverseI cat_is_inverse_is_iso_arr 
        cs_simp: cat_cs_simps
    )

lemma (in category) cat_CId_is_iso_arr'[cat_arrow_cs_intros]:
  assumes "a  Obj"
    and "ℭ' = "
    and "b = a"
    and "c = a"
  shows "CIda : b isoℭ'c"
  using assms(1) 
  unfolding assms(2-4)
  by (rule cat_CId_is_iso_arr)

lemmas [cat_arrow_cs_intros] = category.cat_CId_is_iso_arr'

lemma (in category) cat_is_iso_arr_is_monic_arr[cat_arrow_cs_intros]:
  assumes "f : a isob"
  shows "f : a monb"
proof(intro is_monic_arrI)
  note [cat_cs_intros] = is_iso_arrD(1)
  show "f : a b" by (intro is_iso_arrD(1)[OF assms])
  fix h g c assume prems: 
    "h : c a" "g : c a" "f Ah = f Ag"
  from assms obtain f' 
    where f': "f' : b isoa" 
      and [cat_cs_simps]: "f' Af = CIda" 
    by (auto elim: is_iso_arrE')
  from category_axioms assms prems(1,2) have "h = (f' Af) Ah"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  also from category_axioms assms prems(1,2) f' have " = (f' Af) Ag"
    by (cs_concl cs_simp: prems(3) cat_cs_simps cs_intro: cat_cs_intros)
  also from category_axioms assms prems(1,2) f' have " = g"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  finally show "h = g" by simp
qed

lemmas [cat_arrow_cs_intros] = category.cat_is_iso_arr_is_monic_arr

lemma (in category) cat_is_iso_arr_is_epic_arr:
  assumes "f : a isob"
  shows "f : a epib"
  using assms
  by 
    (
      rule 
        category.cat_is_iso_arr_is_monic_arr[
          OF category_op, unfolded cat_op_simps
          ]
    )

lemmas [cat_arrow_cs_intros] = category.cat_is_iso_arr_is_epic_arr

lemma (in category) cat_is_iso_arr_if_is_monic_arr_is_right_inverse:
  assumes "f : a monb" and "is_right_inverse  g f"
  shows "f : a isob"
proof-
  note f_is_monic_arrD = is_monic_arrD[OF assms(1)]
  from is_right_inverseD[OF assms(2)] f_is_monic_arrD(1) 
  have g: "g : b a" and fg: "f Ag = CIdb"
    by auto
  from f_is_monic_arrD(1) g have gf: "g Af : a a"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from g have CId_a: "CIda : a a" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show ?thesis
  proof
    (
      intro 
        is_iso_arrI 
        cat_is_right_left_inverse_is_inverse 
        is_left_inverseI, 
      rule f_is_monic_arrD(1), 
      rule assms(2),
      rule g,
      rule f_is_monic_arrD(1)
    )
    from f_is_monic_arrD(1) g have "f A(g Af) = f Ag Af"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    also from f_is_monic_arrD(1) g have " = f ACIda"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps fg cs_intro: cat_cs_intros)
    finally have "f A(g Af) = f ACIda" by simp
    from f_is_monic_arrD(2)[OF gf CId_a this] show "g Af = CIda".
  qed
qed

lemma (in category) cat_is_iso_arr_if_is_epic_arr_is_left_inverse:
  assumes "f : a epib" and "is_left_inverse  g f"
  shows "f : a isob"
  using assms
  by 
    (
      rule category.cat_is_iso_arr_if_is_monic_arr_is_right_inverse[
        OF category_op, unfolded cat_op_simps
        ]
    )



subsection‹The inverse arrow›


text‹See Chapter I-5 in cite"mac_lane_categories_2010".›

definition the_inverse :: "V  V  V" ((_¯Cı) [1000] 999)
  where "f¯C= (THE g. is_inverse  g f)"


text‹Elementary properties.›

lemma (in category) cat_is_inverse_is_inverse_the_inverse:
  assumes "is_inverse  g f"
  shows "is_inverse  (f¯C) f"
  unfolding the_inverse_def
proof(rule theI)
  fix g' assume "is_inverse  g' f"
  then show "g' = g" by (meson cat_is_inverse_eq assms)
qed (rule assms)

lemma (in category) cat_is_inverse_eq_the_inverse:
  assumes "is_inverse  g f"
  shows "g = f¯C⇙"
  by (meson assms cat_is_inverse_is_inverse_the_inverse cat_is_inverse_eq)


text‹The inverse arrow is an inverse of an isomorphism.›

lemma (in category) cat_the_inverse_is_inverse:
  assumes "f : a isob"
  shows "is_inverse  (f¯C) f"
proof-
  from assms obtain g where "is_inverse  g f" by auto
  then show "is_inverse  (f¯C) f"
    by (rule cat_is_inverse_is_inverse_the_inverse)
qed

lemma (in category) cat_the_inverse_is_iso_arr:
  assumes "f : a isob"
  shows "f¯C: b isoa"
proof-
  from assms have f: "f : a b" by auto
  have "is_inverse  (f¯C) f" by (rule cat_the_inverse_is_inverse[OF assms])
  from cat_is_inverse_is_iso_arr[OF f this] show ?thesis .
qed

lemma (in category) cat_the_inverse_is_iso_arr':
  assumes "f : a isob" and "ℭ' = "
  shows "f¯C: b isoℭ'a"
  using assms(1) 
  unfolding assms(2)
  by (rule cat_the_inverse_is_iso_arr)

lemmas [cat_cs_intros] = category.cat_the_inverse_is_iso_arr'

lemma (in category) op_cat_the_inverse:
  assumes "f : a isob"
  shows "f¯Cop_cat = f¯C⇙"
proof-
  from assms have "f : b isoop_cat a" unfolding cat_op_simps by simp
  from assms show ?thesis
    by 
      (
        intro 
          category.cat_is_inverse_eq_the_inverse[
            symmetric, OF category_op, unfolded cat_op_simps
            ] 
          cat_the_inverse_is_inverse
      )
qed

lemmas [cat_op_simps] = category.op_cat_the_inverse

lemma (in category) cat_Comp_the_inverse:
  assumes "g : b isoc" and "f : a isob"
  shows "(g Af)¯C= f¯CAg¯C⇙"
proof-
  from assms have "g Af : a isoc" 
    by (cs_concl cs_shallow cs_intro: cat_arrow_cs_intros)
  then have inv_gf: "is_inverse  ((g Af)¯C) (g Af)"
    by (intro cat_the_inverse_is_inverse)
  from assms have "is_inverse  (g¯C) g" "is_inverse  (f¯C) f"
    by (auto intro: cat_the_inverse_is_inverse)
  with category_axioms assms have 
    "is_inverse  (f¯CAg¯C) (g Af)"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_arrow_cs_intros) 
  from inv_gf this show "(g Af)¯C= f¯CAg¯C⇙"
    by (meson cat_is_inverse_eq)
qed

lemmas [cat_cs_simps] = category.cat_Comp_the_inverse

lemma (in category) cat_the_inverse_Comp_CId:
  assumes "f : a isob"
  shows cat_the_inverse_Comp_CId_left: "f¯CAf = CIda"
    and cat_the_inverse_Comp_CId_right: "f Af¯C= CIdb"
proof-
  from assms show "f¯CAf = CIda"
    by 
      (
        cs_concl
          cs_simp: is_inverse_Comp_CId_left
          cs_intro: cat_the_inverse_is_inverse cat_arrow_cs_intros
      )
  from assms show "f Af¯C= CIdb"
    by 
      (
        cs_concl
          cs_simp: is_inverse_Comp_CId_right
          cs_intro: cat_the_inverse_is_inverse cat_arrow_cs_intros
      )
qed

lemmas [cat_cs_simps] = category.cat_the_inverse_Comp_CId

lemma (in category) cat_the_inverse_the_inverse:
  assumes "f : a isob"
  shows "(f¯C)¯C= f"
proof-
  from assms have "(f¯C)¯C= (f¯C)¯CAf¯CAf"
    by (*slow*)
      (
        cs_concl 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_arrow_cs_intros 
      )
  also from assms have " = f"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_arrow_cs_intros
      )
  finally show ?thesis .
qed

lemmas [cat_cs_simps] = category.cat_the_inverse_the_inverse



subsection‹Isomorphic objects›


text‹See Chapter I-5 in cite"mac_lane_categories_2010".›

definition obj_iso :: "V  V  V  bool" 
  where "obj_iso  a b  (f. f : a isob)"

syntax "_obj_iso" :: "V  V  V  bool" ((_/ objı _) [55, 56] 55)
translations "a objb"  "CONST obj_iso  a b"


text‹Rules.›

lemma obj_isoI:
  assumes "f : a isob" 
  shows "a objb"
  using assms unfolding obj_iso_def by auto

lemma obj_isoD[dest]:
  assumes "a objb" 
  shows "f. f : a isob" 
  using assms unfolding obj_iso_def by auto
  
lemma obj_isoE[elim!]:
  assumes "a objb" 
  obtains f where "f : a isob"
  using assms by auto


text‹Elementary properties.›

lemma (in category) op_cat_obj_iso[cat_op_simps]: 
  "a objop_cat b = b obja"
  unfolding obj_iso_def cat_op_simps ..

lemmas [cat_op_simps] = category.op_cat_obj_iso

lemmas [cat_op_intros] = category.op_cat_obj_iso[THEN iffD2]


text‹Equivalence relation.›

lemma (in category) cat_obj_iso_refl:
  assumes "a  Obj" 
  shows "a obja"
  using assms by (auto intro: obj_isoI cat_arrow_cs_intros)

lemma (in category) cat_obj_iso_sym[sym]: 
  assumes "a objb" 
  shows "b obja"
  using assms 
  by (elim obj_isoE is_iso_arrE) 
    (metis obj_iso_def cat_is_inverse_is_iso_arr)

lemma (in category) cat_obj_iso_trans[trans]:
  assumes "a objb" and "b objc" 
  shows "a objc"
  using assms by (auto intro: cat_Comp_is_iso_arr obj_isoI)



subsection‹Terminal object and initial object›

lemma (in category) cat_obj_terminal_CId:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "obj_terminal  a" and "f : a a"
  shows "CIda = f"
  using assms by (elim obj_terminalE) (metis cat_CId_is_arr)

lemma (in category) cat_obj_initial_CId: 
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "obj_initial  a" and "f : a a"
  shows "CIda = f"
  using assms 
  by (rule category.cat_obj_terminal_CId[OF category_op, unfolded cat_op_simps])

lemma (in category) cat_obj_terminal_obj_iso:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "obj_terminal  a" and "obj_terminal  a'"
  shows "a obja'"
proof-
  from assms obtain f where f: "f : a a'" by auto
  from assms obtain f' where f': "f' : a' a" by auto
  from f f' cat_obj_terminal_CId cat_Comp_is_arr 
  have f'f: "is_inverse  f' f"
    by (intro is_inverseI[OF f' f]) (metis assms(1), metis assms(2))
  with f show ?thesis 
    by (cs_concl cs_shallow cs_intro: obj_isoI is_iso_arrI)
qed

lemma (in category) cat_obj_initial_obj_iso:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "obj_initial  a" and "obj_initial  a'"
  shows "a' obja"
proof-
  interpret op: category α op_cat  by (auto intro: cat_cs_intros)
  from assms show ?thesis
    by (rule op.cat_obj_terminal_obj_iso[unfolded cat_op_simps])  
qed                     



subsection‹Null object›

lemma (in category) cat_obj_null_obj_iso:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}.›
  assumes "obj_null  z" and "obj_null  z'"
  shows "z objz'"
  using assms by (simp add: cat_obj_terminal_obj_iso obj_nullD(2))



subsection‹Groupoid›


text‹See Chapter I-5 in cite"mac_lane_categories_2010".›

locale groupoid = category α  for α  +
  assumes grpd_is_iso_arr: "f : a b  f : a isob"


text‹Rules.›

mk_ide rf groupoid_def[unfolded groupoid_axioms_def]
  |intro groupoidI|
  |dest groupoidD[dest]|
  |elim groupoidE[elim]|

text‹\newpage›

end