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 ↦⇩m⇩o⇩n⇘cat_smc ℭ⇙ b ⟷ f : a ↦⇩m⇩o⇩n⇘ℭ⇙ b"
  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 ↦⇩e⇩p⇩i⇘cat_smc ℭ⇙ b ⟷ f : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  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 : ↦⇩i⇩d⇩e⇘cat_smc ℭ⇙ b ⟷ f : ↦⇩i⇩d⇩e⇘ℭ⇙ b"
  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 ↦⇩0⇘cat_smc ℭ⇙ b ⟷ f : a ↦⇩0⇘ℭ⇙ b"
  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⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and cat_CId_left_left[cat_cs_simps]: 
      "f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and cat_CId_right_left[cat_cs_simps]: 
      "f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = 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 "ℭ⦇CId⦈⦇a⦈ : 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 = ℭ⦇CId⦈⦇a⦈"
  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 = ℭ⦇CId⦈⦇a⦈" 
    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 ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
      (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "⋀a. a ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and "⋀a b f. f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and "⋀b c f. f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = f"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. 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 ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
      (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "⋀a. a ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and "⋀a b f. f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and "⋀b c f. f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = f"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. 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 ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
      (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "⋀a. a ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    and "⋀a b f. f : a ↦⇘ℭ⇙ b ⟹ ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f = f"
    and "⋀b c f. f : b ↦⇘ℭ⇙ c ⟹ f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇b⦈ = f"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. 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 ∘⇩A⇘ℭ⇙ f : 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, 
          all‹rewrite 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 α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. 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⦈" "ℭ⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇b⦈"
  have "ℭ⦇CId⦈⦇a⦈ : b ↦⇘ℭ⇙ b" "ℭ⦇CId⦈⦇a⦈ : 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 "ℭ⦇CId⦈⦇b⦈ ∘⇩A⇘op_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 ∘⇩A⇘op_cat ℭ⇙ ℭ⦇CId⦈⦇b⦈ = 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 "ℭ⦇CId⦈⦇a⦈ : a ↦⇩m⇩o⇩n⇘ℭ⇙ a"
  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 "ℭ⦇CId⦈⦇a⦈ : a ↦⇩e⇩p⇩i⇘ℭ⇙ a"
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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈)"

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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
  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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
  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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
  using assms by auto

lemma (in category) is_left_inverseI:
  assumes "g : b ↦⇘ℭ⇙ a" and "f : a ↦⇘ℭ⇙ b" and "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
  shows "is_left_inverse ℭ g f"
proof-
  from assms(3) have "f ∘⇩A⇘op_cat ℭ⇙ g = ℭ⦇CId⦈⦇a⦈"
    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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
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 ∘⇩A⇘op_cat ℭ⇙ g = op_cat ℭ⦇CId⦈⦇b⦈"
    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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇b⦈"
    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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
  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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈ ∧
        f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈
    )"


text‹Rules.›

lemma is_inverseI:
  assumes "g : b ↦⇘ℭ⇙ a"
    and "f : a ↦⇘ℭ⇙ b"
    and "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    and "f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
  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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈ ∧
        f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈
    )"
  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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    and "f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
  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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    "f ∘⇩A⇘ℭ⇙ h = ℭ⦇CId⦈⦇b⦈"
    "g : b' ↦⇘ℭ⇙ a'" 
    "f : a' ↦⇘ℭ⇙ b'" 
    "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a'⦈" 
  then have ab: "a' = a" "b' = b" by auto 
  from prems have gf: "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈" and g: "g : b ↦⇘ℭ⇙ a" 
    unfolding ab by simp_all
  from prems(1) have "h = (g ∘⇩A⇘ℭ⇙ f) ∘⇩A⇘ℭ⇙ h" 
    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' ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇a⦈"
  using assms by auto

lemma is_inverse_Comp_CId_right:
  assumes "is_inverse ℭ g' g" and "g : a ↦⇘ℭ⇙ b"
  shows "g ∘⇩A⇘ℭ⇙ g' = ℭ⦇CId⦈⦇b⦈"
  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' ∘⇩A⇘ℭ⇙ g') (g ∘⇩A⇘ℭ⇙ f)"
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' ∘⇩A⇘ℭ⇙ g' : c ↦⇘ℭ⇙ a" and gf: "g ∘⇩A⇘ℭ⇙ f : 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' ∘⇩A⇘ℭ⇙ g'"
    and "gf = g ∘⇩A⇘ℭ⇙ f"
  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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
    "g : d ↦⇘ℭ⇙ c"
    "f : c ↦⇘ℭ⇙ d"
    "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇c⦈"
  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"
  (‹_ : _ ↦⇩i⇩s⇩oı _› [51, 51, 51] 51)
translations "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b" ⇌ "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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  using assms unfolding is_iso_arr_def by auto

lemma is_iso_arrD[dest]:
  assumes "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  obtains g where "f : a ↦⇘ℭ⇙ b" and "is_inverse ℭ g f"
  using assms by force

lemma is_iso_arrE':
  assumes "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  obtains g where "g : b ↦⇩i⇩s⇩o⇘ℭ⇙ a"
    and "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    and "f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    and fg: "f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
    by auto
  then have g: "g : b ↦⇩i⇩s⇩o⇘ℭ⇙ a" 
    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 ↦⇩i⇩s⇩o⇘op_cat ℭ⇙ a ⟷ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    and "f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
  shows "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b" and "g : b ↦⇩i⇩s⇩o⇘ℭ⇙ a"
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 ↦⇩i⇩s⇩o⇘ℭ⇙ b" and "g : b ↦⇩i⇩s⇩o⇘ℭ⇙ a"
    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 ↦⇩i⇩s⇩o⇘ℭ⇙ a"
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 ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a'⦈"
      and fg: "f ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b'⦈"
    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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
    "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    unfolding a'b' by auto
qed

lemma (in category) cat_Comp_is_iso_arr[cat_arrow_cs_intros]:
  assumes "g : b ↦⇩i⇩s⇩o⇘ℭ⇙ c" and "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "g ∘⇩A⇘ℭ⇙ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ c"
proof-
  from assms have [intro]: "g ∘⇩A⇘ℭ⇙ f : 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' ∘⇩A⇘ℭ⇙ g' : c ↦⇘ℭ⇙ a" by (auto intro: cat_cs_intros)
  from cat_is_inverse_Comp[OF _ _ g'g f'f] assms 
  have "is_inverse ℭ (f' ∘⇩A⇘ℭ⇙ g') (g ∘⇩A⇘ℭ⇙ f)" 
    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 "ℭ⦇CId⦈⦇a⦈ : a ↦⇩i⇩s⇩o⇘ℭ⇙ a"
  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 "ℭ⦇CId⦈⦇a⦈ : b ↦⇩i⇩s⇩o⇘ℭ'⇙ 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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "f : a ↦⇩m⇩o⇩n⇘ℭ⇙ b"
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 ∘⇩A⇘ℭ⇙ h = f ∘⇩A⇘ℭ⇙ g"
  from assms obtain f' 
    where f': "f' : b ↦⇩i⇩s⇩o⇘ℭ⇙ a" 
      and [cat_cs_simps]: "f' ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈" 
    by (auto elim: is_iso_arrE')
  from category_axioms assms prems(1,2) have "h = (f' ∘⇩A⇘ℭ⇙ f) ∘⇩A⇘ℭ⇙ h"
    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' ∘⇩A⇘ℭ⇙ f) ∘⇩A⇘ℭ⇙ g"
    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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "f : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  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 ↦⇩m⇩o⇩n⇘ℭ⇙ b" and "is_right_inverse ℭ g f"
  shows "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
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 ∘⇩A⇘ℭ⇙ g = ℭ⦇CId⦈⦇b⦈"
    by auto
  from f_is_monic_arrD(1) g have gf: "g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ a"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from g have CId_a: "ℭ⦇CId⦈⦇a⦈ : 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 ∘⇩A⇘ℭ⇙ f) = f ∘⇩A⇘ℭ⇙ g ∘⇩A⇘ℭ⇙ f"
      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 ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇a⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps fg cs_intro: cat_cs_intros)
    finally have "f ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f) = f ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇a⦈" by simp
    from f_is_monic_arrD(2)[OF gf CId_a this] show "g ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈".
  qed
qed

lemma (in category) cat_is_iso_arr_if_is_epic_arr_is_left_inverse:
  assumes "f : a ↦⇩e⇩p⇩i⇘ℭ⇙ b" and "is_left_inverse ℭ g f"
  shows "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "f¯⇩C⇘ℭ⇙ : b ↦⇩i⇩s⇩o⇘ℭ⇙ a"
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 ↦⇩i⇩s⇩o⇘ℭ⇙ b" and "ℭ' = ℭ"
  shows "f¯⇩C⇘ℭ⇙ : b ↦⇩i⇩s⇩o⇘ℭ'⇙ 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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "f¯⇩C⇘op_cat ℭ⇙ = f¯⇩C⇘ℭ⇙"
proof-
  from assms have "f : b ↦⇩i⇩s⇩o⇘op_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 ↦⇩i⇩s⇩o⇘ℭ⇙ c" and "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "(g ∘⇩A⇘ℭ⇙ f)¯⇩C⇘ℭ⇙ = f¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ g¯⇩C⇘ℭ⇙"
proof-
  from assms have "g ∘⇩A⇘ℭ⇙ f : a ↦⇩i⇩s⇩o⇘ℭ⇙ c" 
    by (cs_concl cs_shallow cs_intro: cat_arrow_cs_intros)
  then have inv_gf: "is_inverse ℭ ((g ∘⇩A⇘ℭ⇙ f)¯⇩C⇘ℭ⇙) (g ∘⇩A⇘ℭ⇙ f)"
    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¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ g¯⇩C⇘ℭ⇙) (g ∘⇩A⇘ℭ⇙ f)"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_arrow_cs_intros) 
  from inv_gf this show "(g ∘⇩A⇘ℭ⇙ f)¯⇩C⇘ℭ⇙ = f¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ g¯⇩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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows cat_the_inverse_Comp_CId_left: "f¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    and cat_the_inverse_Comp_CId_right: "f ∘⇩A⇘ℭ⇙ f¯⇩C⇘ℭ⇙ = ℭ⦇CId⦈⦇b⦈"
proof-
  from assms show "f¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ f = ℭ⦇CId⦈⦇a⦈"
    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 ∘⇩A⇘ℭ⇙ f¯⇩C⇘ℭ⇙ = ℭ⦇CId⦈⦇b⦈"
    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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  shows "(f¯⇩C⇘ℭ⇙)¯⇩C⇘ℭ⇙ = f"
proof-
  from assms have "(f¯⇩C⇘ℭ⇙)¯⇩C⇘ℭ⇙ = (f¯⇩C⇘ℭ⇙)¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ f¯⇩C⇘ℭ⇙ ∘⇩A⇘ℭ⇙ f"
    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 ↦⇩i⇩s⇩o⇘ℭ⇙ b)"

syntax "_obj_iso" :: "V ⇒ V ⇒ V ⇒ bool" (‹(_/ ≈⇩o⇩b⇩jı _)› [55, 56] 55)
translations "a ≈⇩o⇩b⇩j⇘ℭ⇙ b" ⇌ "CONST obj_iso ℭ a b"


text‹Rules.›

lemma obj_isoI:
  assumes "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b" 
  shows "a ≈⇩o⇩b⇩j⇘ℭ⇙ b"
  using assms unfolding obj_iso_def by auto

lemma obj_isoD[dest]:
  assumes "a ≈⇩o⇩b⇩j⇘ℭ⇙ b" 
  shows "∃f. f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b" 
  using assms unfolding obj_iso_def by auto
  
lemma obj_isoE[elim!]:
  assumes "a ≈⇩o⇩b⇩j⇘ℭ⇙ b" 
  obtains f where "f : a ↦⇩i⇩s⇩o⇘ℭ⇙ b"
  using assms by auto


text‹Elementary properties.›

lemma (in category) op_cat_obj_iso[cat_op_simps]: 
  "a ≈⇩o⇩b⇩j⇘op_cat ℭ⇙ b = b ≈⇩o⇩b⇩j⇘ℭ⇙ a"
  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 ≈⇩o⇩b⇩j⇘ℭ⇙ a"
  using assms by (auto intro: obj_isoI cat_arrow_cs_intros)

lemma (in category) cat_obj_iso_sym[sym]: 
  assumes "a ≈⇩o⇩b⇩j⇘ℭ⇙ b" 
  shows "b ≈⇩o⇩b⇩j⇘ℭ⇙ a"
  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 ≈⇩o⇩b⇩j⇘ℭ⇙ b" and "b ≈⇩o⇩b⇩j⇘ℭ⇙ c" 
  shows "a ≈⇩o⇩b⇩j⇘ℭ⇙ c"
  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 "ℭ⦇CId⦈⦇a⦈ = 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 "ℭ⦇CId⦈⦇a⦈ = 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 ≈⇩o⇩b⇩j⇘ℭ⇙ a'"
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' ≈⇩o⇩b⇩j⇘ℭ⇙ a"
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 ≈⇩o⇩b⇩j⇘ℭ⇙ z'"
  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 ↦⇩i⇩s⇩o⇘ℭ⇙ b"


text‹Rules.›

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

text‹\newpage›

end