Session CZH_Elementary_Categories

Theory CZH_ECAT_Introduction

(* Copyright 2021 (C) Mihails Milehins *)

sectionâ€čIntroductionâ€ș
theory CZH_ECAT_Introduction
  imports CZH_Foundations.CZH_DG_Introduction
begin



subsectionâ€čBackgroundâ€ș


textâ€č
This article provides a 
formalization of the elementary theory of 1-categories without
an additional structure. For further information see 
chapter Introduction in the first installment of 
this work: â€čCategory Theory for ZFC in HOL I: Foundationsâ€ș.
â€ș



subsectionâ€čPreliminariesâ€ș

named_theorems cat_op_simps
named_theorems cat_op_intros

named_theorems cat_cs_simps
named_theorems cat_cs_intros

named_theorems cat_arrow_cs_intros



subsectionâ€čCS setup for foundationsâ€ș

lemmas (in đ’”) [cat_cs_intros] = 
  đ’”_ÎČ
  
textâ€č\newpageâ€ș

end

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 ↩monℭ 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 ↩epicat_smc ℭ b ⟷ f : a ↩epiℭ 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 : ↩idecat_smc ℭ b ⟷ f : ↩ideℭ 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 ↩0cat_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 the previous 
installment of this body of work.
â€ș

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_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_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_simp: cat_cs_simps V_cs_simps)
    show "𝒟∘ 𝔄 = 𝒟∘ 𝔅" by (cs_concl 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_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_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_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⩈ ∘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 ℭ ℭ⩇CId⩈⩇b⩈ = f"
    by (cs_concl 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 ↩monℭ 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 ↩epiℭ 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 ∘Aop_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 ∘Aop_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_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_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_arr_isomorphism :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_arr_isomorphism ℭ a b f ⟷
    (f : a ↩ℭ b ∧ (∃g. is_inverse ℭ g f))"

syntax "_is_arr_isomorphism" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č_ : _ ↩isoı _â€ș [51, 51, 51] 51)
translations "f : a ↩isoℭ b" ⇌ "CONST is_arr_isomorphism ℭ a b f"


textâ€čRules.â€ș

lemma is_arr_isomorphismI:
  assumes "f : a ↩ℭ b" and "is_inverse ℭ g f"
  shows "f : a ↩isoℭ b"
  using assms unfolding is_arr_isomorphism_def by auto

lemma is_arr_isomorphismD[dest]:
  assumes "f : a ↩isoℭ b"
  shows "f : a ↩ℭ b" and "∃g. is_inverse ℭ g f"
  using assms unfolding is_arr_isomorphism_def by auto

lemma is_arr_isomorphismE[elim]:
  assumes "f : a ↩isoℭ b"
  obtains g where "f : a ↩ℭ b" and "is_inverse ℭ g f"
  using assms by force

lemma is_arr_isomorphismE':
  assumes "f : a ↩isoℭ b"
  obtains g where "g : b ↩isoℭ 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 ↩isoℭ a" 
    by (cs_concl cs_intro: is_inverseI is_arr_isomorphismI)
  from that f g gf fg show ?thesis by simp
qed


textâ€čElementary properties.â€ș

lemma (in category) op_cat_is_arr_isomorphism[cat_op_simps]:
  "f : b ↩isoop_cat ℭ a ⟷ f : a ↩isoℭ b"
  unfolding is_arr_isomorphism_def cat_op_simps by simp

lemmas [cat_op_simps] = category.op_cat_is_arr_isomorphism

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

lemma (in category) is_arr_isomorphismI':
  assumes "f : a ↩ℭ b" 
    and "g : b ↩ℭ a"
    and "g ∘Aℭ f = ℭ⩇CId⩈⩇a⩈"
    and "f ∘Aℭ g = ℭ⩇CId⩈⩇b⩈"
  shows "f : a ↩isoℭ b" and "g : b ↩isoℭ 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 ↩isoℭ b" and "g : b ↩isoℭ a"
    by 
      (
        intro 
          is_arr_isomorphismI[OF assms(1) gf]
          is_arr_isomorphismI[OF assms(2) fg]
      )+
qed

lemma (in category) cat_is_inverse_is_arr_isomorphism:
  assumes "f : a ↩ℭ b" and "is_inverse ℭ g f"
  shows "g : b ↩isoℭ a"
proof(intro is_arr_isomorphismI 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_arr_isomorphism[cat_arrow_cs_intros]:
  assumes "g : b ↩isoℭ c" and "f : a ↩isoℭ b"
  shows "g ∘Aℭ f : a ↩isoℭ 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_arr_isomorphismE)
      (auto simp: is_arr_isomorphismD cat_is_inverse_is_arr_isomorphism)
  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_arr_isomorphismE)
      (auto simp: is_arr_isomorphismD cat_is_inverse_is_arr_isomorphism)
  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_arr_isomorphismE) simp
  then show ?thesis by (auto intro: is_arr_isomorphismI)
qed

lemmas [cat_arrow_cs_intros] = category.cat_Comp_is_arr_isomorphism

lemma (in category) cat_CId_is_arr_isomorphism: 
  assumes "a ∈∘ ℭ⩇Obj⩈" 
  shows "ℭ⩇CId⩈⩇a⩈ : a ↩isoℭ a"
  using assms 
  by 
    (
      cs_concl 
        cs_intro: cat_cs_intros is_inverseI cat_is_inverse_is_arr_isomorphism 
        cs_simp: cat_cs_simps
    )

lemma (in category) cat_CId_is_arr_isomorphism'[cat_arrow_cs_intros]:
  assumes "a ∈∘ ℭ⩇Obj⩈"
    and "ℭ' = ℭ"
    and "b = a"
    and "c = a"
  shows "ℭ⩇CId⩈⩇a⩈ : b ↩isoℭ' c"
  using assms(1) 
  unfolding assms(2-4)
  by (rule cat_CId_is_arr_isomorphism)

lemmas [cat_arrow_cs_intros] = category.cat_CId_is_arr_isomorphism'

lemma (in category) cat_is_arr_isomorphism_is_monic_arr[cat_arrow_cs_intros]:
  assumes "f : a ↩isoℭ b"
  shows "f : a ↩monℭ b"
proof(intro is_monic_arrI)
  note [cat_cs_intros] = is_arr_isomorphismD(1)
  show "f : a ↩ℭ b" by (intro is_arr_isomorphismD(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 ↩isoℭ a" 
      and [cat_cs_simps]: "f' ∘Aℭ f = ℭ⩇CId⩈⩇a⩈" 
    by (auto elim: is_arr_isomorphismE')
  from category_axioms assms prems(1,2) have "h = (f' ∘Aℭ f) ∘Aℭ h"
    by (cs_concl 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_simp: cat_cs_simps cs_intro: cat_cs_intros)
  finally show "h = g" by simp
qed

lemmas [cat_arrow_cs_intros] = category.cat_is_arr_isomorphism_is_monic_arr

lemma (in category) cat_is_arr_isomorphism_is_epic_arr:
  assumes "f : a ↩isoℭ b"
  shows "f : a ↩epiℭ b"
  using assms
  by 
    (
      rule 
        category.cat_is_arr_isomorphism_is_monic_arr[
          OF category_op, unfolded cat_op_simps
          ]
    )

lemmas [cat_arrow_cs_intros] = category.cat_is_arr_isomorphism_is_epic_arr



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 ↩isoℭ 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_arr_isomorphism:
  assumes "f : a ↩isoℭ b"
  shows "f¯Cℭ : b ↩isoℭ 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_arr_isomorphism[OF f this] show ?thesis .
qed

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

lemmas [cat_cs_intros] = category.cat_the_inverse_is_arr_isomorphism'

lemma (in category) op_cat_the_inverse:
  assumes "f : a ↩isoℭ b"
  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 ↩isoℭ c" and "f : a ↩isoℭ b"
  shows "(g ∘Aℭ f)¯Cℭ = f¯Cℭ ∘Aℭ g¯Cℭ"
proof-
  from assms have "g ∘Aℭ f : a ↩isoℭ c" 
    by (cs_concl 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_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 ↩isoℭ 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 ↩isoℭ 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_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 ↩isoℭ b)"

syntax "_obj_iso" :: "V ⇒ V ⇒ V ⇒ bool" (â€č(_/ ≈objı _)â€ș [55, 56] 55)
translations "a ≈objℭ b" ⇌ "CONST obj_iso ℭ a b"


textâ€čRules.â€ș

lemma obj_isoI:
  assumes "f : a ↩isoℭ b" 
  shows "a ≈objℭ b"
  using assms unfolding obj_iso_def by auto

lemma obj_isoD[dest]:
  assumes "a ≈objℭ b" 
  shows "∃f. f : a ↩isoℭ b" 
  using assms unfolding obj_iso_def by auto
  
lemma obj_isoE[elim!]:
  assumes "a ≈objℭ b" 
  obtains f where "f : a ↩isoℭ b"
  using assms by auto


textâ€čElementary properties.â€ș

lemma (in category) op_cat_obj_iso[cat_op_simps]: 
  "a ≈objop_cat ℭ b = b ≈objℭ 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 ≈objℭ a"
  using assms by (auto intro: obj_isoI cat_arrow_cs_intros)

lemma (in category) cat_obj_iso_sym[sym]: 
  assumes "a ≈objℭ b" 
  shows "b ≈objℭ a"
  using assms 
  by (elim obj_isoE is_arr_isomorphismE) 
    (metis obj_iso_def cat_is_inverse_is_arr_isomorphism)

lemma (in category) cat_obj_iso_trans[trans]:
  assumes "a ≈objℭ b" and "b ≈objℭ c" 
  shows "a ≈objℭ c"
  using assms by (auto intro: cat_Comp_is_arr_isomorphism 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 ≈objℭ 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_intro: obj_isoI is_arr_isomorphismI)
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' ≈objℭ 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 ≈objℭ 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_arr_isomorphism: "f : a ↩ℭ b âŸč f : a ↩isoℭ b"


textâ€čRules.â€ș

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

textâ€č\newpageâ€ș

end

Theory CZH_ECAT_Small_Category

(* Copyright 2021 (C) Mihails Milehins *)

sectionâ€čSmallness for categoriesâ€ș
theory CZH_ECAT_Small_Category
  imports 
    CZH_Foundations.CZH_SMC_Small_Semicategory
    CZH_ECAT_Category
begin



subsectionâ€čBackgroundâ€ș


textâ€č
An explanation of the methodology chosen for the exposition of all
matters related to the size of the categories and associated entities
is given in the first installment of this work.
â€ș

named_theorems cat_small_cs_simps
named_theorems cat_small_cs_intros



subsectionâ€čTiny categoryâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș

locale tiny_category = đ’” α + vfsequence ℭ + CId: vsv â€čℭ⩇CId⊈â€ș for α ℭ +
  assumes tiny_cat_length[cat_cs_simps]: "vcard ℭ = 6ℕ"
    and tiny_cat_tiny_semicategory[slicing_intros]: 
      "tiny_semicategory α (cat_smc ℭ)"
    and tiny_cat_CId_vdomain[cat_cs_simps]: "𝒟∘ (ℭ⩇CId⩈) = ℭ⩇Obj⩈"
    and tiny_cat_CId_is_arr[cat_cs_intros]: 
      "a ∈∘ ℭ⩇Obj⊈ âŸč ℭ⩇CId⩈⩇a⊈ : a ↩ℭ a"
    and tiny_cat_CId_left_left[cat_cs_simps]:
      "f : a ↩ℭ b âŸč ℭ⩇CId⩈⩇b⊈ ∘Aℭ f = f"
    and tiny_cat_CId_right_left[cat_cs_simps]:
      "f : b ↩ℭ c âŸč f ∘Aℭ ℭ⩇CId⩈⩇b⊈ = f"

lemmas [slicing_intros] = tiny_category.tiny_cat_tiny_semicategory


textâ€čRules.â€ș

lemma (in tiny_category) tiny_category_axioms'[cat_small_cs_intros]:
  assumes "α' = α"
  shows "tiny_category α' ℭ"
  unfolding assms by (rule tiny_category_axioms)

mk_ide rf tiny_category_def[unfolded tiny_category_axioms_def]
  |intro tiny_categoryI|
  |dest tiny_categoryD[dest]|
  |elim tiny_categoryE[elim]|

lemma tiny_categoryI':
  assumes "category α ℭ" and "ℭ⩇Obj⊈ ∈∘ Vset α" and "ℭ⩇Arr⊈ ∈∘ Vset α"
  shows "tiny_category α ℭ"
proof-
  interpret category α ℭ by (rule assms(1))
  show ?thesis
  proof(intro tiny_categoryI)
    from assms show "tiny_semicategory α (cat_smc ℭ)"
      by (intro tiny_semicategoryI') (auto simp: slicing_simps)
  qed (auto simp: vfsequence_axioms cat_cs_simps cat_cs_intros)
qed

lemma tiny_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 "ℭ⩇Arr⊈ ∈∘ Vset α"
  shows "tiny_category α ℭ"
  by (intro tiny_categoryI tiny_semicategoryI'', unfold slicing_simps) 
    (simp_all add: cat_smc_def nat_omega_simps assms)


textâ€čSlicing.â€ș

context tiny_category
begin

interpretation smc: tiny_semicategory α â€čcat_smc ℭâ€ș
  by (rule tiny_cat_tiny_semicategory) 

lemmas_with [unfolded slicing_simps]:
  tiny_cat_semicategory = smc.semicategory_axioms
  and tiny_cat_Obj_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Obj_in_Vset
  and tiny_cat_Arr_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Arr_in_Vset
  and tiny_cat_Dom_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Dom_in_Vset
  and tiny_cat_Cod_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Cod_in_Vset
  and tiny_cat_Comp_in_Vset[cat_small_cs_intros] = smc.tiny_smc_Comp_in_Vset

end


textâ€čElementary properties.â€ș

sublocale tiny_category ⊆ category
  by (rule categoryI) 
    (
      auto simp: 
        vfsequence_axioms tiny_cat_semicategory cat_cs_intros cat_cs_simps
    )

lemmas (in tiny_category) tiny_dg_category = category_axioms

lemmas [cat_small_cs_intros] = tiny_category.tiny_dg_category


textâ€čSize.â€ș

lemma (in tiny_category) tiny_cat_CId_in_Vset: "ℭ⩇CId⊈ ∈∘ Vset α"
proof-
  from tiny_cat_Obj_in_Vset have "𝒟∘ (ℭ⩇CId⊈) ∈∘ Vset α"
    by (simp add: tiny_cat_Obj_in_Vset cat_cs_simps)
  moreover from tiny_cat_Arr_in_Vset cat_CId_vrange tiny_cat_Arr_in_Vset have 
    "ℛ∘ (ℭ⩇CId⊈) ∈∘ Vset α"  
    by auto
  ultimately show ?thesis by (blast intro: đ’”_Limit_αω)
qed

lemma (in tiny_category) tiny_cat_in_Vset: "ℭ ∈∘ Vset α"
proof-
  note [cat_cs_intros] = 
    tiny_cat_Obj_in_Vset 
    tiny_cat_Arr_in_Vset
    tiny_cat_Dom_in_Vset
    tiny_cat_Cod_in_Vset
    tiny_cat_Comp_in_Vset
    tiny_cat_CId_in_Vset
  show ?thesis by (subst cat_def) (cs_concl cs_intro: cat_cs_intros V_cs_intros)
qed

lemma tiny_category[simp]: "small {ℭ. tiny_category α ℭ}"
proof(rule down)
  show "{ℭ. tiny_category α ℭ} ⊆ elts (set {ℭ. category α ℭ})" 
    by (auto intro: cat_small_cs_intros)
qed

lemma small_categories_vsubset_Vset: "set {ℭ. tiny_category α ℭ} ⊆∘ Vset α" 
  by (rule vsubsetI) (simp_all add: tiny_category.tiny_cat_in_Vset)

lemma (in category) cat_tiny_category_if_ge_Limit:
  assumes "đ’” ÎČ" and "α ∈∘ ÎČ"
  shows "tiny_category ÎČ â„­"
proof(intro tiny_categoryI)
  show "tiny_semicategory ÎČ (cat_smc ℭ)"
    by 
      (
        rule semicategory.smc_tiny_semicategory_if_ge_Limit, 
        rule cat_semicategory;
        intro assms
      )
qed (auto simp:  assms(1) cat_cs_simps cat_cs_intros vfsequence_axioms)


subsubsectionâ€čOpposite tiny categoryâ€ș

lemma (in tiny_category) tiny_category_op: "tiny_category α (op_cat ℭ)"
  by (intro tiny_categoryI') 
    (auto simp: cat_op_simps cat_cs_intros cat_small_cs_intros)

lemmas tiny_category_op[cat_op_intros] = tiny_category.tiny_category_op



subsectionâ€čFinite categoryâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€č
A definition of a finite category can be found in nLab 
\cite{noauthor_nlab_nodate}\footnote{
\url{https://ncatlab.org/nlab/show/finite+category}
}.
â€ș

(*TODO: implicit redundant assumption*)
locale finite_category = đ’” α + vfsequence ℭ + CId: vsv â€čℭ⩇CId⊈â€ș for α ℭ +
  assumes fin_cat_length[cat_cs_simps]: "vcard ℭ = 6ℕ"
    and fin_cat_finite_semicategory[slicing_intros]: 
      "finite_semicategory α (cat_smc ℭ)"
    and fin_cat_CId_vdomain[cat_cs_simps]: "𝒟∘ (ℭ⩇CId⩈) = ℭ⩇Obj⩈"
    and fin_cat_CId_is_arr[cat_cs_intros]: 
      "a ∈∘ ℭ⩇Obj⊈ âŸč ℭ⩇CId⩈⩇a⊈ : a ↩ℭ a"
    and fin_cat_CId_left_left[cat_cs_simps]:
      "f : a ↩ℭ b âŸč ℭ⩇CId⩈⩇b⊈ ∘Aℭ f = f"
    and fin_cat_CId_right_left[cat_cs_simps]:
      "f : b ↩ℭ c âŸč f ∘Aℭ ℭ⩇CId⩈⩇b⊈ = f"

lemmas [slicing_intros] = finite_category.fin_cat_finite_semicategory


textâ€čRules.â€ș

lemma (in finite_category) fin_category_axioms'[cat_small_cs_intros]:
  assumes "α' = α"
  shows "finite_category α' ℭ"
  unfolding assms by (rule finite_category_axioms)

mk_ide rf finite_category_def[unfolded finite_category_axioms_def]
  |intro finite_categoryI|
  |dest finite_categoryD[dest]|
  |elim finite_categoryE[elim]|

lemma finite_categoryI':
  assumes "category α ℭ"  and "vfinite (ℭ⩇Obj⊈)" and "vfinite (ℭ⩇Arr⊈)"
  shows "finite_category α ℭ"
proof-
  interpret category α ℭ by (rule assms(1))
  show ?thesis
  proof(intro finite_categoryI)
    from assms show "finite_semicategory α (cat_smc ℭ)"
      by (intro finite_semicategoryI') (auto simp: slicing_simps)
  qed (auto simp: vfsequence_axioms cat_cs_simps cat_cs_intros)
qed

lemma finite_categoryI'': 
  assumes "tiny_category α ℭ" and "vfinite (ℭ⩇Obj⊈)" and "vfinite (ℭ⩇Arr⊈)"
  shows "finite_category α ℭ"
  using assms by (intro finite_categoryI') (auto intro: cat_small_cs_intros)


textâ€čSlicing.â€ș

context finite_category
begin

interpretation smc: finite_semicategory α â€čcat_smc ℭâ€ș
  by (rule fin_cat_finite_semicategory) 

lemmas_with [unfolded slicing_simps]:
  fin_cat_tiny_semicategory = smc.tiny_semicategory_axioms
  and fin_smc_Obj_vfinite[cat_small_cs_intros] = smc.fin_smc_Obj_vfinite
  and fin_smc_Arr_vfinite[cat_small_cs_intros] = smc.fin_smc_Arr_vfinite

end


textâ€čElementary properties.â€ș

sublocale finite_category ⊆ tiny_category
  by (rule tiny_categoryI) 
    (
      auto 
        simp: vfsequence_axioms 
        intro:
          cat_cs_intros cat_cs_simps cat_small_cs_intros
          finite_category.fin_cat_tiny_semicategory
    )

lemmas (in finite_category) fin_cat_tiny_category = tiny_category_axioms

lemmas [cat_small_cs_intros] = finite_category.fin_cat_tiny_category

lemma (in finite_category) fin_cat_in_Vset: "ℭ ∈∘ Vset α"
  by (rule tiny_cat_in_Vset)


textâ€čSize.â€ș

lemma small_finite_categories[simp]: "small {ℭ. finite_category α ℭ}"
proof(rule down)
  show "{ℭ. finite_category α ℭ} ⊆ elts (set {ℭ. tiny_category  α ℭ})" 
    by (auto intro: cat_small_cs_intros)
qed

lemma small_finite_categories_vsubset_Vset: 
  "set {ℭ. finite_category α ℭ} ⊆∘ Vset α" 
  by (rule vsubsetI) (simp_all add: finite_category.fin_cat_in_Vset)


subsubsectionâ€čOpposite finite categoryâ€ș

lemma (in finite_category) finite_category_op: "finite_category α (op_cat ℭ)"
  by (intro finite_categoryI', unfold cat_op_simps) 
    (auto simp: cat_cs_intros cat_small_cs_intros)

lemmas finite_category_op[cat_op_intros] = finite_category.finite_category_op

textâ€č\newpageâ€ș

end

Theory CZH_ECAT_Functor

(* Copyright 2021 (C) Mihails Milehins *)

sectionâ€čFunctorâ€ș
theory CZH_ECAT_Functor
  imports 
    CZH_ECAT_Category
    CZH_Foundations.CZH_SMC_Semifunctor
begin



subsectionâ€čBackgroundâ€ș

named_theorems cf_cs_simps
named_theorems cf_cs_intros

named_theorems cat_cn_cs_simps
named_theorems cat_cn_cs_intros

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


subsubsectionâ€čSlicingâ€ș

definition cf_smcf :: "V ⇒ V"
  where "cf_smcf ℭ = 
    [ℭ⩇ObjMap⩈, ℭ⩇ArrMap⩈, cat_smc (ℭ⩇HomDom⩈), cat_smc (ℭ⩇HomCod⩈)]∘"


textâ€čComponents.â€ș

lemma cf_smcf_components:
  shows [slicing_simps]: "cf_smcf 𝔉⩇ObjMap⩈ = 𝔉⩇ObjMap⩈"
    and [slicing_simps]: "cf_smcf 𝔉⩇ArrMap⩈ = 𝔉⩇ArrMap⩈"
    and [slicing_commute]: "cf_smcf 𝔉⩇HomDom⩈ = cat_smc (𝔉⩇HomDom⩈)"
    and [slicing_commute]: "cf_smcf 𝔉⩇HomCod⩈ = cat_smc (𝔉⩇HomCod⩈)"
  unfolding cf_smcf_def dghm_field_simps by (auto simp: nat_omega_simps)



subsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}.â€ș

locale is_functor = 
  đ’” α + vfsequence 𝔉 + HomDom: category α 𝔄 + HomCod: category α 𝔅 
  for α 𝔄 𝔅 𝔉 +
  assumes cf_length[cat_cs_simps]: "vcard 𝔉 = 4ℕ" 
    and cf_is_semifunctor[slicing_intros]: 
      "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMCα cat_smc 𝔅" 
    and cf_HomDom[cat_cs_simps]: "𝔉⩇HomDom⩈ = 𝔄"
    and cf_HomCod[cat_cs_simps]: "𝔉⩇HomCod⩈ = 𝔅"
    and cf_ObjMap_CId[cat_cs_intros]: 
      "c ∈∘ 𝔄⩇Obj⊈ âŸč 𝔉⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⊈⊈ = 𝔅⩇CId⩈⩇𝔉⩇ObjMap⩈⩇c⊈⊈"

syntax "_is_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č(_ :/ _ ↩↩Cı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↩↩Cα 𝔅" ⇌ "CONST is_functor α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_cf :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_cf α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_cat 𝔄 ↩↩Cα 𝔅"

syntax "_is_cn_cf" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č(_ :/ _ C↊↊ı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 C↊↊α 𝔅" ⇀ "CONST is_cn_cf α 𝔄 𝔅 𝔉"

abbreviation all_cfs :: "V ⇒ V"
  where "all_cfs α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩Cα 𝔅}"

abbreviation cfs :: "V ⇒ V ⇒ V ⇒ V"
  where "cfs α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↩↩Cα 𝔅}"

lemmas [cat_cs_simps] =
  is_functor.cf_length
  is_functor.cf_HomDom
  is_functor.cf_HomCod
  is_functor.cf_ObjMap_CId

lemma cn_cf_ObjMap_CId[cat_cn_cs_simps]: 
  assumes "𝔉 : 𝔄 C↊↊α 𝔅" and "c ∈∘ 𝔄⩇Obj⊈"
  shows "𝔉⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⩈⩈ = 𝔅⩇CId⩈⩇𝔉⩇ObjMap⩈⩇c⩈⩈"
proof-
  interpret is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(1))
  from assms(2) have c: "c ∈∘ op_cat 𝔄⩇Obj⩈" unfolding cat_op_simps by simp
  show ?thesis by (rule cf_ObjMap_CId[OF c, unfolded cat_op_simps])
qed

lemma (in is_functor) cf_is_semifunctor':
  assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMCα 𝔅'"
  unfolding assms by (rule cf_is_semifunctor)

lemmas [slicing_intros] = is_functor.cf_is_semifunctor'

lemma cn_smcf_comp_is_semifunctor: 
  assumes "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "cf_smcf 𝔉 : cat_smc 𝔄 SMC↊↊αcat_smc 𝔅"
  using assms 
  unfolding slicing_simps slicing_commute
  by (rule is_functor.cf_is_semifunctor)

lemma cn_smcf_comp_is_semifunctor'[slicing_intros]: 
  assumes "𝔉 : 𝔄 C↊↊α 𝔅" 
    and "𝔄' = op_smc (cat_smc 𝔄)"
    and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMCα 𝔅'"
  using assms(1) unfolding assms(2,3) by (rule cn_smcf_comp_is_semifunctor)


textâ€čRules.â€ș

lemma (in is_functor) is_functor_axioms'[cat_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↩↩Cα' 𝔅'"
  unfolding assms by (rule is_functor_axioms)

mk_ide rf is_functor_def[unfolded is_functor_axioms_def]
  |intro is_functorI|
  |dest is_functorD[dest]|
  |elim is_functorE[elim]|

lemmas [cat_cs_intros] = is_functorD(3,4)

lemma is_functorI':
  assumes "đ’” α"
    and "vfsequence 𝔉"
    and "category α 𝔄"
    and "category α 𝔅"
    and "vcard 𝔉 = 4ℕ"
    and "𝔉⩇HomDom⩈ = 𝔄"
    and "𝔉⩇HomCod⩈ = 𝔅"
    and "vsv (𝔉⩇ObjMap⩈)"
    and "vsv (𝔉⩇ArrMap⩈)"
    and "𝒟∘ (𝔉⩇ObjMap⩈) = 𝔄⩇Obj⩈"
    and "ℛ∘ (𝔉⩇ObjMap⩈) ⊆∘ 𝔅⩇Obj⩈"
    and "𝒟∘ (𝔉⩇ArrMap⩈) = 𝔄⩇Arr⩈"
    and "⋀a b f. f : a ↩𝔄 b âŸč
      𝔉⩇ArrMap⩈⩇f⩈ : 𝔉⩇ObjMap⩈⩇a⩈ ↩𝔅 𝔉⩇ObjMap⩈⩇b⩈"
    and "⋀b c g a f. ⟩ g : b ↩𝔄 c; f : a ↩𝔄 b ⟧ âŸč
      𝔉⩇ArrMap⩈⩇g ∘A𝔄 f⩈ = 𝔉⩇ArrMap⩈⩇g⩈ ∘A𝔅 𝔉⩇ArrMap⩈⩇f⩈"
    and "(⋀c. c ∈∘ 𝔄⩇Obj⊈ âŸč 𝔉⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⊈⊈ = 𝔅⩇CId⩈⩇𝔉⩇ObjMap⩈⩇c⊈⊈)"
  shows "𝔉 : 𝔄 ↩↩Cα 𝔅"
  by 
    (
      intro is_functorI is_semifunctorI', 
      unfold cf_smcf_components slicing_simps
    )
    (simp_all add: assms cf_smcf_def nat_omega_simps category.cat_semicategory)

lemma is_functorD':
  assumes "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "đ’” α"
    and "vfsequence 𝔉"
    and "category α 𝔄"
    and "category α 𝔅"
    and "vcard 𝔉 = 4ℕ"
    and "𝔉⩇HomDom⩈ = 𝔄"
    and "𝔉⩇HomCod⩈ = 𝔅"
    and "vsv (𝔉⩇ObjMap⩈)"
    and "vsv (𝔉⩇ArrMap⩈)"
    and "𝒟∘ (𝔉⩇ObjMap⩈) = 𝔄⩇Obj⩈"
    and "ℛ∘ (𝔉⩇ObjMap⩈) ⊆∘ 𝔅⩇Obj⩈"
    and "𝒟∘ (𝔉⩇ArrMap⩈) = 𝔄⩇Arr⩈"
    and "⋀a b f. f : a ↩𝔄 b âŸč
      𝔉⩇ArrMap⩈⩇f⩈ : 𝔉⩇ObjMap⩈⩇a⩈ ↩𝔅 𝔉⩇ObjMap⩈⩇b⩈"
    and "⋀b c g a f. ⟩ g : b ↩𝔄 c; f : a ↩𝔄 b ⟧ âŸč
      𝔉⩇ArrMap⩈⩇g ∘A𝔄 f⩈ = 𝔉⩇ArrMap⩈⩇g⩈ ∘A𝔅 𝔉⩇ArrMap⩈⩇f⩈"
    and "(⋀c. c ∈∘ 𝔄⩇Obj⊈ âŸč 𝔉⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⊈⊈ = 𝔅⩇CId⩈⩇𝔉⩇ObjMap⩈⩇c⊈⊈)"
  by 
    (
      simp_all add: 
        is_functorD(2-9)[OF assms] 
        is_semifunctorD'[OF is_functorD(6)[OF assms], unfolded slicing_simps]
    )

lemma is_functorE':
  assumes "𝔉 : 𝔄 ↩↩Cα 𝔅"
  obtains "đ’” α"
    and "vfsequence 𝔉"
    and "category α 𝔄"
    and "category α 𝔅"
    and "vcard 𝔉 = 4ℕ"
    and "𝔉⩇HomDom⩈ = 𝔄"
    and "𝔉⩇HomCod⩈ = 𝔅"
    and "vsv (𝔉⩇ObjMap⩈)"
    and "vsv (𝔉⩇ArrMap⩈)"
    and "𝒟∘ (𝔉⩇ObjMap⩈) = 𝔄⩇Obj⩈"
    and "ℛ∘ (𝔉⩇ObjMap⩈) ⊆∘ 𝔅⩇Obj⩈"
    and "𝒟∘ (𝔉⩇ArrMap⩈) = 𝔄⩇Arr⩈"
    and "⋀a b f. f : a ↩𝔄 b âŸč
      𝔉⩇ArrMap⩈⩇f⩈ : 𝔉⩇ObjMap⩈⩇a⩈ ↩𝔅 𝔉⩇ObjMap⩈⩇b⩈"
    and "⋀b c g a f. ⟩ g : b ↩𝔄 c; f : a ↩𝔄 b ⟧ âŸč
      𝔉⩇ArrMap⩈⩇g ∘A𝔄 f⩈ = 𝔉⩇ArrMap⩈⩇g⩈ ∘A𝔅 𝔉⩇ArrMap⩈⩇f⩈"
    and "(⋀c. c ∈∘ 𝔄⩇Obj⊈ âŸč 𝔉⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⊈⊈ = 𝔅⩇CId⩈⩇𝔉⩇ObjMap⩈⩇c⊈⊈)"
  using assms by (simp add: is_functorD')


textâ€čA functor is a semifunctor.â€ș

context is_functor
begin

interpretation smcf: is_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
  by (rule cf_is_semifunctor)

sublocale ObjMap: vsv â€č𝔉⩇ObjMap⊈â€ș
  by (rule smcf.ObjMap.vsv_axioms[unfolded slicing_simps])
sublocale ArrMap: vsv â€č𝔉⩇ArrMap⊈â€ș
  by (rule smcf.ArrMap.vsv_axioms[unfolded slicing_simps])

lemmas_with [unfolded slicing_simps]:
  cf_ObjMap_vsv = smcf.smcf_ObjMap_vsv
  and cf_ArrMap_vsv = smcf.smcf_ArrMap_vsv
  and cf_ObjMap_vdomain[cat_cs_simps] = smcf.smcf_ObjMap_vdomain
  and cf_ObjMap_vrange = smcf.smcf_ObjMap_vrange
  and cf_ArrMap_vdomain[cat_cs_simps] = smcf.smcf_ArrMap_vdomain
  and cf_ArrMap_is_arr = smcf.smcf_ArrMap_is_arr
  and cf_ArrMap_is_arr''[cat_cs_intros] = smcf.smcf_ArrMap_is_arr''
  and cf_ArrMap_is_arr'[cat_cs_intros] = smcf.smcf_ArrMap_is_arr'
  and cf_ObjMap_app_in_HomCod_Obj[cat_cs_intros] = 
    smcf.smcf_ObjMap_app_in_HomCod_Obj
  and cf_ArrMap_vrange = smcf.smcf_ArrMap_vrange
  and cf_ArrMap_app_in_HomCod_Arr[cat_cs_intros] = 
    smcf.smcf_ArrMap_app_in_HomCod_Arr
  and cf_ObjMap_vsubset_Vset = smcf.smcf_ObjMap_vsubset_Vset
  and cf_ArrMap_vsubset_Vset = smcf.smcf_ArrMap_vsubset_Vset
  and cf_ObjMap_in_Vset = smcf.smcf_ObjMap_in_Vset
  and cf_ArrMap_in_Vset = smcf.smcf_ArrMap_in_Vset
  and cf_is_semifunctor_if_ge_Limit = smcf.smcf_is_semifunctor_if_ge_Limit
  and cf_is_arr_HomCod = smcf.smcf_is_arr_HomCod
  and cf_vimage_dghm_ArrMap_vsubset_Hom = 
    smcf.smcf_vimage_dghm_ArrMap_vsubset_Hom

lemmas_with [unfolded slicing_simps]: 
  cf_ArrMap_Comp = smcf.smcf_ArrMap_Comp

end

lemmas [cat_cs_simps] = 
  is_functor.cf_ObjMap_vdomain
  is_functor.cf_ArrMap_vdomain
  is_functor.cf_ArrMap_Comp

lemmas [cat_cs_intros] =
  is_functor.cf_ObjMap_app_in_HomCod_Obj
  is_functor.cf_ArrMap_app_in_HomCod_Arr
  is_functor.cf_ArrMap_is_arr'


textâ€čElementary properties.â€ș

lemma cn_cf_ArrMap_Comp[cat_cn_cs_simps]: 
  assumes "category α 𝔄" 
    and "𝔉 : 𝔄 C↊↊α 𝔅"
    and "g : c ↩𝔄 b"
    and "f : b ↩𝔄 a" 
  shows "𝔉⩇ArrMap⩈⩇f ∘A𝔄 g⩈ = 𝔉⩇ArrMap⩈⩇g⩈ ∘A𝔅 𝔉⩇ArrMap⩈⩇f⩈"
proof-
  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔉: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule cn_smcf_ArrMap_Comp
          [
            OF 
              𝔄.cat_semicategory 
              𝔉.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_simps,
            OF assms(3,4)
          ]
      )
qed

lemma cf_eqI:
  assumes "𝔊 : 𝔄 ↩↩Cα 𝔅" 
    and "𝔉 : ℭ ↩↩Cα 𝔇"
    and "𝔊⩇ObjMap⩈ = 𝔉⩇ObjMap⩈"
    and "𝔊⩇ArrMap⩈ = 𝔉⩇ArrMap⩈"
    and "𝔄 = ℭ"
    and "𝔅 = 𝔇"
  shows "𝔊 = 𝔉"
proof(rule vsv_eqI)
  interpret L: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret R: is_functor α ℭ 𝔇 𝔉 by (rule assms(2))
  from assms(1) show "vsv 𝔊" by auto
  from assms(2) show "vsv 𝔉" by auto
  have dom: "𝒟∘ 𝔊 = 4ℕ" by (cs_concl cs_simp: cat_cs_simps V_cs_simps)
  show "𝒟∘ 𝔊 = 𝒟∘ 𝔉" by (cs_concl cs_simp: cat_cs_simps V_cs_simps)
  from assms(5,6) have sup: "𝔊⩇HomDom⩈ = 𝔉⩇HomDom⩈" "𝔊⩇HomCod⩈ = 𝔉⩇HomCod⩈" 
    by (simp_all add: cat_cs_simps)
  show "a ∈∘ 𝒟∘ 𝔊 âŸč 𝔊⩇a⊈ = 𝔉⩇a⊈" for a 
    by (unfold dom, elim_in_numeral, insert assms(3,4) sup)
      (auto simp: dghm_field_simps)
qed

lemma cf_smcf_eqI:
  assumes "𝔊 : 𝔄 ↩↩Cα 𝔅"
    and "𝔉 : ℭ ↩↩Cα 𝔇"
    and "𝔄 = ℭ"
    and "𝔅 = 𝔇"
    and "cf_smcf 𝔊 = cf_smcf 𝔉"
  shows "𝔊 = 𝔉"
proof(rule cf_eqI)
  from assms(5) have 
    "cf_smcf 𝔊⩇ObjMap⩈ = cf_smcf 𝔉⩇ObjMap⩈"
    "cf_smcf 𝔊⩇ArrMap⩈ = cf_smcf 𝔉⩇ArrMap⩈"
    by simp_all
  then show "𝔊⩇ObjMap⩈ = 𝔉⩇ObjMap⩈" "𝔊⩇ArrMap⩈ = 𝔉⩇ArrMap⩈"
    unfolding slicing_simps by simp_all
qed (auto intro: assms(1,2) simp: assms(3-5))

lemma (in is_functor) cf_def: "𝔉 = [𝔉⩇ObjMap⩈, 𝔉⩇ArrMap⩈, 𝔉⩇HomDom⩈, 𝔉⩇HomCod⩈]∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟∘ 𝔉 = 4ℕ" by (cs_concl cs_simp: cat_cs_simps V_cs_simps)
  have dom_rhs: "𝒟∘ [𝔉⩇Obj⩈, 𝔉⩇Arr⩈, 𝔉⩇Dom⩈, 𝔉⩇Cod⩈]∘ = 4ℕ"
    by (simp add: nat_omega_simps)
  then show "𝒟∘ 𝔉 = 𝒟∘ [𝔉⩇ObjMap⩈, 𝔉⩇ArrMap⩈, 𝔉⩇HomDom⩈, 𝔉⩇HomCod⩈]∘"
    unfolding dom_lhs dom_rhs by (simp add: nat_omega_simps)
  show "a ∈∘ 𝒟∘ 𝔉 âŸč 𝔉⩇a⊈ = [𝔉⩇ObjMap⊈, 𝔉⩇ArrMap⊈, 𝔉⩇HomDom⊈, 𝔉⩇HomCod⊈]∘⩇a⊈" 
    for a
    by (unfold dom_lhs, elim_in_numeral, unfold dghm_field_simps)
      (simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)


textâ€čSize.â€ș

lemma (in is_functor) cf_in_Vset: 
  assumes "đ’” ÎČ" and "α ∈∘ ÎČ"  
  shows "𝔉 ∈∘ Vset ÎČ"
proof-
  interpret ÎČ: đ’” ÎČ by (rule assms(1))
  note [cat_cs_intros] = 
    cf_ObjMap_in_Vset 
    cf_ArrMap_in_Vset 
    HomDom.cat_in_Vset 
    HomCod.cat_in_Vset
  from assms(2) show ?thesis
    by (subst cf_def) 
      (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros)
qed

lemma (in is_functor) cf_is_functor_if_ge_Limit:
  assumes "đ’” ÎČ" and "α ∈∘ ÎČ"
  shows "𝔉 : 𝔄 ↩↩CÎČ đ”…"
  by (rule is_functorI)
    (
      auto simp:
        cat_cs_simps
        assms 
        vfsequence_axioms
        cf_is_semifunctor_if_ge_Limit
        HomDom.cat_category_if_ge_Limit
        HomCod.cat_category_if_ge_Limit
        intro: cat_cs_intros 
    )

lemma small_all_cfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩Cα 𝔅}"
proof(cases â€čđ’” αâ€ș)
  case True
  from is_functor.cf_in_Vset show ?thesis
    by (intro down[of _ â€čVset (α + ω)â€ș])
      (auto simp: True đ’”.đ’”_Limit_αω đ’”.đ’”_ω_αω đ’”.intro đ’”.đ’”_α_αω)
next
  case False
  then have "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩Cα 𝔅} = {}" by auto
  then show ?thesis by simp
qed

lemma (in is_functor) cf_in_Vset_7: "𝔉 ∈∘ Vset (α + 7ℕ)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
    cf_ObjMap_vsubset_Vset 
    cf_ArrMap_vsubset_Vset
  from HomDom.cat_category_in_Vset_4 have [cat_cs_intros]:
    "𝔄 ∈∘ Vset (succ (succ (succ (succ α))))"
    by (succ_of_numeral) (cs_prems cs_simp: plus_V_succ_right V_cs_simps)
  from HomCod.cat_category_in_Vset_4 have [cat_cs_intros]:
    "𝔅 ∈∘ Vset (succ (succ (succ (succ α))))"
    by (succ_of_numeral) (cs_prems cs_simp: plus_V_succ_right V_cs_simps)
  show ?thesis
    by (subst cf_def, succ_of_numeral)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps cat_cs_simps 
          cs_intro: cat_cs_intros V_cs_intros
      )
qed

lemma (in đ’”) all_cfs_in_Vset: 
  assumes "đ’” ÎČ" and "α ∈∘ ÎČ"
  shows "all_cfs α ∈∘ Vset ÎČ"
proof(rule vsubset_in_VsetI)
  interpret ÎČ: đ’” ÎČ by (rule assms(1))
  show "all_cfs α ⊆∘ Vset (α + 7ℕ)"
  proof(intro vsubsetI)
    fix 𝔉 assume "𝔉 ∈∘ all_cfs α"
    then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↩↩Cα 𝔅" by clarsimp
    interpret is_functor α 𝔄 𝔅 𝔉 using 𝔉 by simp
    show "𝔉 ∈∘ Vset (α + 7ℕ)" by (rule cf_in_Vset_7)
  qed
  from assms(2) show "Vset (α + 7ℕ) ∈∘ Vset ÎČ"
    by (cs_concl cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma small_cfs[simp]: "small {𝔉. 𝔉 : 𝔄 ↩↩Cα 𝔅}"
  by (rule down[of _ â€čset {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩Cα 𝔅}â€ș]) auto



subsectionâ€čOpposite functorâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter II-2 in \cite{mac_lane_categories_2010}.â€ș

definition op_cf :: "V ⇒ V"
  where "op_cf 𝔉 =
    [𝔉⩇ObjMap⩈, 𝔉⩇ArrMap⩈, op_cat (𝔉⩇HomDom⩈), op_cat (𝔉⩇HomCod⩈)]∘"


textâ€čComponents.â€ș

lemma op_cf_components[cat_op_simps]:
  shows "op_cf 𝔉⩇ObjMap⩈ = 𝔉⩇ObjMap⩈"
    and "op_cf 𝔉⩇ArrMap⩈ = 𝔉⩇ArrMap⩈"
    and "op_cf 𝔉⩇HomDom⩈ = op_cat (𝔉⩇HomDom⩈)"
    and "op_cf 𝔉⩇HomCod⩈ = op_cat (𝔉⩇HomCod⩈)"
  unfolding op_cf_def dghm_field_simps by (auto simp: nat_omega_simps)


textâ€čSlicing.â€ș

lemma cf_smcf_op_cf[slicing_commute]: "op_smcf (cf_smcf 𝔉) = cf_smcf (op_cf 𝔉)"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟∘ (op_smcf (cf_smcf 𝔉)) = 4ℕ"
    unfolding op_smcf_def by (auto simp: nat_omega_simps)
  have dom_rhs: "𝒟∘ (cf_smcf (op_cf 𝔉)) = 4ℕ"
    unfolding cf_smcf_def by (auto simp: nat_omega_simps)
  show "𝒟∘ (op_smcf (cf_smcf 𝔉)) = 𝒟∘ (cf_smcf (op_cf 𝔉))"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ (op_smcf (cf_smcf 𝔉)) âŸč 
    op_smcf (cf_smcf 𝔉)⩇a⩈ = cf_smcf (op_cf 𝔉)⩇a⩈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold cf_smcf_def op_cf_def op_smcf_def dghm_field_simps
      )
      (auto simp: nat_omega_simps slicing_commute)
qed (auto simp: cf_smcf_def op_smcf_def)


textâ€čElementary properties.â€ș

lemma op_cf_vsv[cat_op_intros]: "vsv (op_cf 𝔉)" unfolding op_cf_def by auto


subsubsectionâ€čFurther propertiesâ€ș

lemma (in is_functor) is_functor_op: "op_cf 𝔉 : op_cat 𝔄 ↩↩Cα op_cat 𝔅"
proof(intro is_functorI, unfold cat_op_simps)
  show "vfsequence (op_cf 𝔉)" unfolding op_cf_def by simp
  show "vcard (op_cf 𝔉) = 4ℕ" 
    unfolding op_cf_def by (auto simp: nat_omega_simps)
  fix c assume "c ∈∘ 𝔄⩇Obj⩈"
  then show "𝔉⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⩈⩈ = 𝔅⩇CId⩈⩇𝔉⩇ObjMap⩈⩇c⩈⩈"
    unfolding cat_op_simps by (auto intro: cat_cs_intros)
qed 
  (
    auto simp: 
      cat_cs_simps
      slicing_commute[symmetric]
      is_semifunctor.is_semifunctor_op 
      cf_is_semifunctor
      HomCod.category_op 
      HomDom.category_op
  )

lemma (in is_functor) is_functor_op'[cat_op_intros]: 
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅"
  shows "op_cf 𝔉 : 𝔄' ↩↩Cα 𝔅'"
  unfolding assms(1,2) by (rule is_functor_op)

lemmas is_functor_op[cat_op_intros] = is_functor.is_functor_op'

lemma (in is_functor) cf_op_cf_op_cf[cat_op_simps]: "op_cf (op_cf 𝔉) = 𝔉" 
proof(rule cf_eqI[of α 𝔄 𝔅 _ 𝔄 𝔅], unfold cat_op_simps)
  show "op_cf (op_cf 𝔉) : 𝔄 ↩↩Cα 𝔅"
    by 
      (
        metis 
          HomCod.cat_op_cat_op_cat 
          HomDom.cat_op_cat_op_cat 
          is_functor.is_functor_op 
          is_functor_op
      )
qed (auto simp: cat_cs_intros)

lemmas cf_op_cf_op_cf[cat_op_simps] = is_functor.cf_op_cf_op_cf

lemma eq_op_cf_iff[cat_op_simps]: 
  assumes "𝔊 : 𝔄 ↩↩Cα 𝔅" and "𝔉 : ℭ ↩↩Cα 𝔇"
  shows "op_cf 𝔊 = op_cf 𝔉 ⟷ 𝔊 = 𝔉"
proof
  interpret L: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret R: is_functor α ℭ 𝔇 𝔉 by (rule assms(2))
  assume prems: "op_cf 𝔊 = op_cf 𝔉"
  show "𝔊 = 𝔉"
  proof(rule cf_eqI[OF assms])
    from prems R.cf_op_cf_op_cf L.cf_op_cf_op_cf show 
      "𝔊⩇ObjMap⩈ = 𝔉⩇ObjMap⩈" "𝔊⩇ArrMap⩈ = 𝔉⩇ArrMap⩈"
      by metis+
    from prems R.cf_op_cf_op_cf L.cf_op_cf_op_cf have 
      "𝔊⩇HomDom⩈ = 𝔉⩇HomDom⩈" "𝔊⩇HomCod⩈ = 𝔉⩇HomCod⩈"
      by auto
    then show "𝔄 = ℭ" "𝔅 = 𝔇" by (simp_all add: cat_cs_simps)
  qed
qed auto



subsectionâ€čComposition of covariant functorsâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș

abbreviation (input) cf_comp :: "V ⇒ V ⇒ V" (infixl "∘CF" 55)
  where "cf_comp ≡ dghm_comp"


textâ€čSlicing.â€ș

lemma cf_smcf_smcf_comp[slicing_commute]: 
  "cf_smcf 𝔊 ∘SMCF cf_smcf 𝔉 = cf_smcf (𝔊 ∘CF 𝔉)"
  unfolding dghm_comp_def cf_smcf_def dghm_field_simps 
  by (simp add: nat_omega_simps)


subsubsectionâ€čObject mapâ€ș

lemma cf_comp_ObjMap_vsv[cat_cs_intros]: 
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "vsv ((𝔊 ∘CF 𝔉)⩇ObjMap⩈)"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_comp_ObjMap_vsv
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma cf_comp_ObjMap_vdomain[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "𝒟∘ ((𝔊 ∘CF 𝔉)⩇ObjMap⩈) = 𝔄⩇Obj⩈"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_comp_ObjMap_vdomain
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma cf_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "ℛ∘ ((𝔊 ∘CF 𝔉)⩇ObjMap⩈) ⊆∘ ℭ⩇Obj⩈"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_comp_ObjMap_vrange
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma cf_comp_ObjMap_app[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅" and [simp]: "a ∈∘ 𝔄⩇Obj⊈"
  shows "(𝔊 ∘CF 𝔉)⩇ObjMap⩈⩇a⩈ = 𝔊⩇ObjMap⩈⩇𝔉⩇ObjMap⩈⩇a⩈⩈"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_comp_ObjMap_app
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute, 
            OF assms(3)
          ]
      )
qed


subsubsectionâ€čArrow mapâ€ș

lemma cf_comp_ArrMap_vsv[cat_cs_intros]: 
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "vsv ((𝔊 ∘CF 𝔉)⩇ArrMap⩈)"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by 
      (
        rule smcf_comp_ArrMap_vsv
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma cf_comp_ArrMap_vdomain[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "𝒟∘ ((𝔊 ∘CF 𝔉)⩇ArrMap⩈) = 𝔄⩇Arr⩈"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by 
      (
        rule smcf_comp_ArrMap_vdomain
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma cf_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "ℛ∘ ((𝔊 ∘CF 𝔉)⩇ArrMap⩈) ⊆∘ ℭ⩇Arr⩈"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_comp_ArrMap_vrange
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma cf_comp_ArrMap_app[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅" and [simp]: "f ∈∘ 𝔄⩇Arr⊈"
  shows "(𝔊 ∘CF 𝔉)⩇ArrMap⩈⩇f⩈ = 𝔊⩇ArrMap⩈⩇𝔉⩇ArrMap⩈⩇f⩈⩈"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_comp_ArrMap_app
          [
            OF L.cf_is_semifunctor R.cf_is_semifunctor, 
            unfolded slicing_simps slicing_commute,
            OF assms(3)
          ]
      )
qed


subsubsectionâ€čFurther propertiesâ€ș

lemma cf_comp_is_functorI[cat_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "𝔊 ∘CF 𝔉 : 𝔄 ↩↩Cα ℭ"
proof-
  interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
  proof(rule is_functorI, unfold dghm_comp_components(3,4))
    show "vfsequence (𝔊 ∘CF 𝔉)" by (simp add: dghm_comp_def)
    show "vcard (𝔊 ∘CF 𝔉) = 4ℕ"  
      unfolding dghm_comp_def by (simp add: nat_omega_simps)
    show "cf_smcf (𝔊 ∘CF 𝔉) : cat_smc 𝔄 ↩↩SMCα cat_smc ℭ"
      unfolding cf_smcf_smcf_comp[symmetric] 
      by (cs_concl cs_intro: smc_cs_intros slicing_intros cat_cs_intros)
    fix c assume "c ∈∘ 𝔄⩇Obj⩈"
    with assms show 
      "(𝔊 ∘CF 𝔉)⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⩈⩈ = ℭ⩇CId⩈⩇(𝔊 ∘CF 𝔉)⩇ObjMap⩈⩇c⩈⩈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: cat_cs_simps intro: cat_cs_intros)
qed

lemma cf_comp_assoc[cat_cs_simps]:
  assumes "ℌ : ℭ ↩↩Cα 𝔇" and "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "(ℌ ∘CF 𝔊) ∘CF 𝔉 = ℌ ∘CF (𝔊 ∘CF 𝔉)"
proof(rule cf_eqI[of α 𝔄 𝔇 _ 𝔄 𝔇])
  interpret ℌ: is_functor α ℭ 𝔇 ℌ by (rule assms(1)) 
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2)) 
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(3)) 
  from 𝔉.is_functor_axioms 𝔊.is_functor_axioms ℌ.is_functor_axioms 
  show "ℌ ∘CF (𝔊 ∘CF 𝔉) : 𝔄 ↩↩Cα 𝔇" and "ℌ ∘CF 𝔊 ∘CF 𝔉 : 𝔄 ↩↩Cα 𝔇"  
    by (auto simp: cat_cs_simps intro: cat_cs_intros)
qed (simp_all add: dghm_comp_components vcomp_assoc)


textâ€čThe opposite of the covariant composition of functors.â€ș

lemma op_cf_cf_comp[cat_op_simps]: "op_cf (𝔊 ∘CF 𝔉) = op_cf 𝔊 ∘CF op_cf 𝔉"
  unfolding dghm_comp_def op_cf_def dghm_field_simps
  by (simp add: nat_omega_simps)



subsectionâ€čComposition of contravariant functorsâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee section 1.2 in \cite{bodo_categories_1970}.â€ș

definition cf_cn_comp :: "V ⇒ V ⇒ V" (infixl "CF∘" 55)
  where "𝔊 CF∘ 𝔉 =
    [
      𝔊⩇ObjMap⩈ ∘∘ 𝔉⩇ObjMap⩈,
      𝔊⩇ArrMap⩈ ∘∘ 𝔉⩇ArrMap⩈,
      op_cat (𝔉⩇HomDom⩈),
      𝔊⩇HomCod⩈
    ]∘"


textâ€čComponents.â€ș

lemma cf_cn_comp_components:
  shows "(𝔊 CF∘ 𝔉)⩇ObjMap⩈ = 𝔊⩇ObjMap⩈ ∘∘ 𝔉⩇ObjMap⩈"
    and "(𝔊 CF∘ 𝔉)⩇ArrMap⩈ = 𝔊⩇ArrMap⩈ ∘∘ 𝔉⩇ArrMap⩈"
    and [cat_cn_cs_simps]: "(𝔊 CF∘ 𝔉)⩇HomDom⩈ = op_cat (𝔉⩇HomDom⩈)"
    and [cat_cn_cs_simps]: "(𝔊 CF∘ 𝔉)⩇HomCod⩈ = 𝔊⩇HomCod⩈"
  unfolding cf_cn_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)


textâ€čSlicing.â€ș

lemma cf_smcf_cf_cn_comp[slicing_commute]: 
  "cf_smcf 𝔊 SMCF∘ cf_smcf 𝔉 = cf_smcf (𝔊 CF∘ 𝔉)"
  unfolding smcf_cn_comp_def cf_cn_comp_def cf_smcf_def  
  by (simp add: nat_omega_simps slicing_commute dghm_field_simps)


subsubsectionâ€čObject map: two contravariant functorsâ€ș

lemma cf_cn_comp_ObjMap_vsv[cat_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "vsv ((𝔊 CF∘ 𝔉)⩇ObjMap⩈)"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_vsv
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ObjMap_vdomain[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "𝒟∘ ((𝔊 CF∘ 𝔉)⩇ObjMap⩈) = 𝔄⩇Obj⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ObjMap_vdomain
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "ℛ∘ ((𝔊 CF∘ 𝔉)⩇ObjMap⩈) ⊆∘ ℭ⩇Obj⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ObjMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ObjMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅" and "a ∈∘ 𝔄⩇Obj⊈"
  shows "(𝔊 CF∘ 𝔉)⩇ObjMap⩈⩇a⩈ = 𝔊⩇ObjMap⩈⩇𝔉⩇ObjMap⩈⩇a⩈⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ObjMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps, 
            OF assms(3)
          ]
      )
qed


subsubsectionâ€čArrow map: two contravariant functorsâ€ș

lemma cf_cn_comp_ArrMap_vsv[cat_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "vsv ((𝔊 CF∘ 𝔉)⩇ArrMap⩈)"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_vsv
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ArrMap_vdomain[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "𝒟∘ ((𝔊 CF∘ 𝔉)⩇ArrMap⩈) = 𝔄⩇Arr⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ArrMap_vdomain
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "ℛ∘ ((𝔊 CF∘ 𝔉)⩇ArrMap⩈) ⊆∘ ℭ⩇Arr⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ArrMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ArrMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅" and "a ∈∘ 𝔄⩇Arr⊈"
  shows "(𝔊 CF∘ 𝔉)⩇ArrMap⩈⩇a⩈ = 𝔊⩇ArrMap⩈⩇𝔉⩇ArrMap⩈⩇a⩈⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ArrMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsectionâ€čObject map: contravariant and covariant functorâ€ș

lemma cf_cn_cov_comp_ObjMap_vsv[cat_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "vsv ((𝔊 CF∘ 𝔉)⩇ObjMap⩈)"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_vsv
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ObjMap_vdomain[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "𝒟∘ ((𝔊 CF∘ 𝔉)⩇ObjMap⩈) = 𝔄⩇Obj⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_vdomain
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "ℛ∘ ((𝔊 CF∘ 𝔉)⩇ObjMap⩈) ⊆∘ ℭ⩇Obj⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ObjMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅" and "a ∈∘ 𝔄⩇Obj⊈"
  shows "(𝔊 CF∘ 𝔉)⩇ObjMap⩈⩇a⩈ = 𝔊⩇ObjMap⩈⩇𝔉⩇ObjMap⩈⩇a⩈⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsectionâ€čArrow map: contravariant and covariant functorsâ€ș

lemma cf_cn_cov_comp_ArrMap_vsv[cat_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "vsv ((𝔊 CF∘ 𝔉)⩇ArrMap⩈)"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_vsv
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ArrMap_vdomain[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "𝒟∘ ((𝔊 CF∘ 𝔉)⩇ArrMap⩈) = 𝔄⩇Arr⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_vdomain
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "ℛ∘ ((𝔊 CF∘ 𝔉)⩇ArrMap⩈) ⊆∘ ℭ⩇Arr⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ArrMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅" and "a ∈∘ 𝔄⩇Arr⊈"
  shows "(𝔊 CF∘ 𝔉)⩇ArrMap⩈⩇a⩈ = 𝔊⩇ArrMap⩈⩇𝔉⩇ArrMap⩈⩇a⩈⩈"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsectionâ€čFurther propertiesâ€ș

lemma cf_cn_comp_is_functorI[cat_cn_cs_intros]:
  assumes "category α 𝔄" and "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "𝔊 CF∘ 𝔉 : 𝔄 ↩↩Cα ℭ"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(2))
  interpret R: is_functor α â€čop_cat 𝔄â€ș 𝔅 𝔉 by (rule assms(3))
  interpret 𝔄: category α 𝔄 by (rule assms(1))
  show ?thesis
  proof(rule is_functorI, unfold cf_cn_comp_components(3,4) cat_op_simps)
    show "vfsequence (𝔊 CF∘ 𝔉)"
      unfolding cf_cn_comp_def by (simp add: nat_omega_simps)
    show "vcard (𝔊 CF∘ 𝔉) = 4ℕ"
      unfolding cf_cn_comp_def by (simp add: nat_omega_simps)
    from assms(1) L.cf_is_semifunctor R.cf_is_semifunctor show 
      "cf_smcf (𝔊 CF∘ 𝔉) : cat_smc 𝔄 ↩↩SMCα cat_smc ℭ"
      unfolding cf_smcf_cf_cn_comp[symmetric] 
      by 
        (
          cs_concl cs_intro: 
            cat_cs_intros slicing_intros smc_cn_cs_intros
        )
    fix c assume "c ∈∘ 𝔄⩇Obj⩈"
    with assms show 
      "(𝔊 CF∘ 𝔉)⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⩈⩈ = ℭ⩇CId⩈⩇(𝔊 CF∘ 𝔉)⩇ObjMap⩈⩇c⩈⩈"
      by 
        (
          cs_concl 
            cs_simp: cat_op_simps cat_cn_cs_simps cs_intro: cat_cs_intros
        )
  qed (auto simp: cat_cs_simps cat_cs_intros cat_op_simps)
qed


textâ€čSee section 1.2 in \cite{bodo_categories_1970}).â€ș

lemma cf_cn_cov_comp_is_functor[cat_cn_cs_intros]:
  assumes "𝔊 : 𝔅 C↊↊α ℭ" and "𝔉 : 𝔄 ↩↩Cα 𝔅"
  shows "𝔊 CF∘ 𝔉 : 𝔄 C↊↊α ℭ"
proof-
  interpret L: is_functor α â€čop_cat 𝔅â€ș ℭ 𝔊 by (rule assms(1))
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
  proof
    (
      rule is_functorI, 
      unfold cf_cn_comp_components(3,4) cat_op_simps slicing_commute[symmetric]
    )
    show "vfsequence (𝔊 CF∘ 𝔉)" unfolding cf_cn_comp_def by simp
    show "vcard (𝔊 CF∘ 𝔉) = 4ℕ"
      unfolding cf_cn_comp_def by (auto simp: nat_omega_simps)
    from L.cf_is_semifunctor show 
      "cf_smcf 𝔊 SMCF∘ cf_smcf 𝔉 : op_smc (cat_smc 𝔄) ↩↩SMCα cat_smc ℭ"
      by (cs_concl cs_intro: cat_cs_intros slicing_intros smc_cs_intros)
    fix c assume "c ∈∘ 𝔄⩇Obj⩈"
    with assms show "(𝔊 CF∘ 𝔉)⩇ArrMap⩈⩇𝔄⩇CId⩈⩇c⩈⩈ = ℭ⩇CId⩈⩇(𝔊 CF∘ 𝔉)⩇ObjMap⩈⩇c⩈⩈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_cn_cs_simps 
            cs_intro: cat_cs_intros
        )
  qed (auto simp: cat_cs_simps cat_cs_intros)
qed


textâ€čSee section 1.2 in \cite{bodo_categories_1970}.â€ș

lemma cf_cov_cn_comp_is_functor[cat_cn_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩Cα ℭ" and "𝔉 : 𝔄 C↊↊α 𝔅"
  shows "𝔊 ∘CF 𝔉 : 𝔄 C↊↊α ℭ"
  using assms by (rule cf_comp_is_functorI)


textâ€čThe opposite of the contravariant composition of functors.â€ș

lemma op_cf_cf_cn_comp[cat_op_simps]: "op_cf (𝔊 CF∘ 𝔉) = op_cf 𝔊 CF∘ op_cf 𝔉"
  unfolding op_cf_def cf_cn_comp_def dghm_field_simps 
  by (auto simp: nat_omega_simps)



subsectionâ€čIdentity functorâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}.â€ș

abbreviation (input) cf_id :: "V ⇒ V" where "cf_id ≡ dghm_id"


textâ€čSlicing.â€ș

lemma cf_smcf_cf_id[slicing_commute]: "smcf_id (cat_smc ℭ) = cf_smcf (cf_id ℭ)"
  unfolding dghm_id_def cat_smc_def cf_smcf_def dghm_field_simps dg_field_simps
  by (simp add: nat_omega_simps)

context category
begin

interpretation smc: semicategory α â€čcat_smc ℭâ€ș by (rule cat_semicategory)

lemmas_with [unfolded slicing_simps]:
  cat_smcf_id_is_semifunctor = smc.smc_smcf_id_is_semifunctor

end


subsubsectionâ€čObject mapâ€ș

lemmas [cat_cs_simps] = dghm_id_ObjMap_app


subsubsectionâ€čArrow mapâ€ș

lemmas [cat_cs_simps] = dghm_id_ArrMap_app


subsubsectionâ€čOpposite of an identity functor.â€ș

lemma op_cf_cf_id[cat_op_simps]: "op_cf (cf_id ℭ) = cf_id (op_cat ℭ)"
  unfolding dghm_id_def op_cat_def op_cf_def dghm_field_simps dg_field_simps
  by (auto simp: nat_omega_simps)


subsubsectionâ€čAn identity functor is a functorâ€ș

lemma (in category) cat_cf_id_is_functor: "cf_id ℭ : ℭ ↩↩Cα ℭ"
proof(rule is_functorI, unfold dghm_id_components)
  from cat_smcf_id_is_semifunctor show 
    "cf_smcf (cf_id ℭ) : cat_smc ℭ ↩↩SMCα cat_smc ℭ"
    by (simp add: slicing_commute)
  from cat_CId_is_arr show 
    "c ∈∘ ℭ⩇Obj⊈ âŸč vid_on (ℭ⩇Arr⊈)⩇ℭ⩇CId⩈⩇c⊈⊈ = ℭ⩇CId⩈⩇vid_on (ℭ⩇Obj⊈)⩇c⊈⊈"
    for c
    by auto
qed (auto simp: dghm_id_def nat_omega_simps cat_cs_intros)

lemma (in category) cat_cf_id_is_functor': 
  assumes "𝔄 = ℭ" and "𝔅 = ℭ"
  shows "cf_id ℭ : 𝔄 ↩↩Cα 𝔅"
  unfolding assms by (rule cat_cf_id_is_functor)

lemmas [cat_cs_intros] = category.cat_cf_id_is_functor'


subsubsectionâ€čFurther propertiesâ€ș

lemma (in is_functor) cf_cf_comp_cf_id_left[cat_cs_simps]: "cf_id 𝔅 ∘CF 𝔉 = 𝔉"
  ―â€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș
  by 
    (
      rule cf_eqI,
      unfold dghm_id_components dghm_comp_components dghm_id_components
    )
    (auto intro: cat_cs_intros simp: cf_ArrMap_vrange cf_ObjMap_vrange)

lemmas [cat_cs_simps] = is_functor.cf_cf_comp_cf_id_left

lemma (in is_functor) cf_cf_comp_cf_id_right[cat_cs_simps]: "𝔉 ∘CF cf_id 𝔄 = 𝔉"
  ―â€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș
  by 
    (
      rule cf_eqI, 
      unfold dghm_id_components dghm_comp_components dghm_id_components
    )
    (
      auto 
        intro: cat_cs_intros 
        simp: cat_cs_simps cf_ArrMap_vrange cf_ObjMap_vrange 
    )

lemmas [cat_cs_simps] = is_functor.cf_cf_comp_cf_id_right



subsectionâ€čConstant functorâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter III-3 in \cite{mac_lane_categories_2010}.â€ș

abbreviation cf_const :: "V ⇒ V ⇒ V ⇒ V"
  where "cf_const ℭ 𝔇 a ≡ smcf_const ℭ 𝔇 a (𝔇⩇CId⩈⩇a⩈)"


textâ€čSlicing.â€ș

lemma cf_smcf_cf_const[slicing_commute]: 
  "smcf_const (cat_smc ℭ) (cat_smc 𝔇) a (𝔇⩇CId⩈⩇a⩈) = cf_smcf (cf_const ℭ 𝔇 a)"
  unfolding 
    dghm_const_def cat_smc_def cf_smcf_def dghm_field_simps dg_field_simps
  by (simp add: nat_omega_simps)


subsubsectionâ€čObject map and arrow mapâ€ș

context
  fixes 𝔇 a :: V
begin

lemmas_with [where 𝔇=𝔇 and a=a and f=â€č𝔇⩇CId⩈⩇a⊈â€ș, cat_cs_simps]: 
  dghm_const_ObjMap_app
  dghm_const_ArrMap_app

end


subsubsectionâ€čOpposite constant functorâ€ș

lemma op_cf_cf_const[cat_op_simps]:
  "op_cf (cf_const ℭ 𝔇 a) = cf_const (op_cat ℭ) (op_cat 𝔇) a"
  unfolding dghm_const_def op_cat_def op_cf_def dghm_field_simps dg_field_simps
  by (auto simp: nat_omega_simps)


subsubsectionâ€čA constant functor is a functorâ€ș

lemma cf_const_is_functor: 
  assumes "category α ℭ" and "category α 𝔇" and "a ∈∘ 𝔇⩇Obj⊈" 
  shows "cf_const ℭ 𝔇 a : ℭ ↩↩Cα 𝔇"
proof-
  interpret ℭ: category α ℭ by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  show ?thesis
  proof(intro is_functorI, tacticâ€čdistinct_subgoals_tacâ€ș)
    show "vfsequence (dghm_const ℭ 𝔇 a (𝔇⩇CId⩈⩇a⩈))"
      unfolding dghm_const_def by simp
    show "vcard (cf_const ℭ 𝔇 a) = 4ℕ"
      unfolding dghm_const_def by (simp add: nat_omega_simps)
    from assms show "cf_smcf (cf_const ℭ 𝔇 a) : cat_smc ℭ ↩↩SMCα cat_smc 𝔇"
      by 
        ( 
          cs_concl
            cs_simp: cat_cs_simps slicing_simps slicing_commute[symmetric] 
            cs_intro: smc_cs_intros cat_cs_intros slicing_intros
        )
    fix c assume "c ∈∘ ℭ⩇Obj⩈"
    with assms show 
      "cf_const ℭ 𝔇 a⩇ArrMap⩈⩇ℭ⩇CId⩈⩇c⩈⩈ = 𝔇⩇CId⩈⩇cf_const ℭ 𝔇 a⩇ObjMap⩈⩇c⩈⩈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: dghm_const_components assms)
qed 

lemma cf_const_is_functor'[cat_cs_intros]: 
  assumes "category α ℭ" 
    and "category α 𝔇" 
    and "a ∈∘ 𝔇⩇Obj⩈" 
    and "𝔄 = ℭ"
    and "𝔅 = 𝔇"
  shows "cf_const ℭ 𝔇 a : 𝔄 ↩↩Cα 𝔅"
  using assms(1-3) unfolding assms(4,5) by (rule cf_const_is_functor)



subsectionâ€čFaithful functorâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș

locale is_ft_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes ft_cf_is_ft_semifunctor[slicing_intros]: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.faithfulα cat_smc 𝔅"

syntax "_is_ft_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č(_ :/ _ ↩↩C.faithfulı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↩↩C.faithfulα 𝔅" ⇌ "CONST is_ft_functor α 𝔄 𝔅 𝔉"

lemma (in is_ft_functor) ft_cf_is_ft_functor':
  assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMC.faithfulα 𝔅'"
  unfolding assms by (rule ft_cf_is_ft_semifunctor)

lemmas [slicing_intros] = is_ft_functor.ft_cf_is_ft_functor'


textâ€čRules.â€ș

lemma (in is_ft_functor) is_ft_functor_axioms'[cf_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↩↩C.faithfulα' 𝔅'"
  unfolding assms by (rule is_ft_functor_axioms)

mk_ide rf is_ft_functor_def[unfolded is_ft_functor_axioms_def]
  |intro is_ft_functorI|
  |dest is_ft_functorD[dest]|
  |elim is_ft_functorE[elim]|

lemmas [cf_cs_intros] = is_ft_functorD(1)

lemma is_ft_functorI':
  assumes "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "⋀a b. ⟩ a ∈∘ 𝔄⩇Obj⊈; b ∈∘ 𝔄⩇Obj⊈ ⟧ âŸč v11 (𝔉⩇ArrMap⊈ ↟l∘ Hom 𝔄 a b)"
  shows "𝔉 : 𝔄 ↩↩C.faithfulα 𝔅"
  using assms
  by (intro is_ft_functorI)
    (
      simp_all add: 
        assms(1) 
        is_ft_semifunctorI'[OF is_functorD(6)[
          OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_ft_functorD':
  assumes "𝔉 : 𝔄 ↩↩C.faithfulα 𝔅"
  shows "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "⋀a b. ⟩ a ∈∘ 𝔄⩇Obj⊈; b ∈∘ 𝔄⩇Obj⊈ ⟧ âŸč v11 (𝔉⩇ArrMap⊈ ↟l∘ Hom 𝔄 a b)"
  by 
    (
      simp_all add: 
        is_ft_functorD[OF assms(1)] 
        is_ft_semifunctorD'(2)[
          OF is_ft_functorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_ft_functorE':
  assumes "𝔉 : 𝔄 ↩↩C.faithfulα 𝔅"
  obtains "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "⋀a b. ⟩ a ∈∘ 𝔄⩇Obj⊈; b ∈∘ 𝔄⩇Obj⊈ ⟧ âŸč v11 (𝔉⩇ArrMap⊈ ↟l∘ Hom 𝔄 a b)"
  using assms by (simp_all add: is_ft_functorD')


textâ€čElementary properties.â€ș

context is_ft_functor
begin

interpretation smcf: is_ft_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
  by (rule ft_cf_is_ft_semifunctor) 

lemmas_with [unfolded slicing_simps]:
  ft_cf_v11_on_Hom = smcf.ft_smcf_v11_on_Hom

end


subsubsectionâ€čOpposite faithful functor.â€ș

lemma (in is_ft_functor) is_ft_functor_op': 
  "op_cf 𝔉 : op_cat 𝔄 ↩↩C.faithfulα op_cat 𝔅"   
  by (rule is_ft_functorI, unfold slicing_commute[symmetric])
    (
      simp_all add: 
        is_functor_op is_ft_semifunctor.is_ft_semifunctor_op 
        ft_cf_is_ft_semifunctor
    )

lemma (in is_ft_functor) is_ft_functor_op: 
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅"
  shows "op_cf 𝔉 : op_cat 𝔄 ↩↩C.faithfulα op_cat 𝔅"   
  unfolding assms by (rule is_ft_functor_op')

lemmas is_ft_functor_op[cat_op_intros] = is_ft_functor.is_ft_functor_op'


subsubsectionâ€čThe composition of faithful functors is a faithful functorâ€ș

lemma cf_comp_is_ft_functor[cf_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩C.faithfulα ℭ" and "𝔉 : 𝔄 ↩↩C.faithfulα 𝔅"
  shows "𝔊 ∘CF 𝔉 : 𝔄 ↩↩C.faithfulα ℭ"
proof(intro is_ft_functorI)
  interpret 𝔊: is_ft_functor α 𝔅 ℭ 𝔊 by (simp add: assms(1))
  interpret 𝔉: is_ft_functor α 𝔄 𝔅 𝔉 by (simp add: assms(2))
  from 𝔉.is_functor_axioms 𝔊.is_functor_axioms show "𝔊 ∘CF 𝔉 : 𝔄 ↩↩Cα ℭ"
    by (cs_concl cs_intro: cat_cs_intros)
  then interpret is_functor α 𝔄 ℭ â€č𝔊 ∘CF 𝔉â€ș .
  show "cf_smcf (𝔊 ∘CF 𝔉) : cat_smc 𝔄 ↩↩SMC.faithfulα cat_smc ℭ" 
    by 
      ( 
        cs_concl 
          cs_simp: slicing_commute[symmetric] 
          cs_intro: cf_cs_intros smcf_cs_intros slicing_intros
      )
qed



subsectionâ€čFull functorâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș

locale is_fl_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes fl_cf_is_fl_semifunctor:
    "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.fullα cat_smc 𝔅"

syntax "_is_fl_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č(_ :/ _ ↩↩C.fullı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↩↩C.fullα 𝔅" ⇌ "CONST is_fl_functor α 𝔄 𝔅 𝔉"

lemma (in is_fl_functor) fl_cf_is_fl_functor'[slicing_intros]:
  assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMC.fullα 𝔅'"
  unfolding assms by (rule fl_cf_is_fl_semifunctor)

lemmas [slicing_intros] = is_fl_functor.fl_cf_is_fl_semifunctor


textâ€čRules.â€ș

lemma (in is_fl_functor) is_fl_functor_axioms'[cf_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↩↩C.fullα' 𝔅'"
  unfolding assms by (rule is_fl_functor_axioms)

mk_ide rf is_fl_functor_def[unfolded is_fl_functor_axioms_def]
  |intro is_fl_functorI|
  |dest is_fl_functorD[dest]|
  |elim is_fl_functorE[elim]|

lemmas [cf_cs_intros] = is_fl_functorD(1)

lemma is_fl_functorI':
  assumes "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "⋀a b. ⟩ a ∈∘ 𝔄⩇Obj⊈; b ∈∘ 𝔄⩇Obj⊈ ⟧ âŸč
    𝔉⩇ArrMap⩈ `∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⩇ObjMap⩈⩇a⩈) (𝔉⩇ObjMap⩈⩇b⩈)"
  shows "𝔉 : 𝔄 ↩↩C.fullα 𝔅"
  using assms
  by (intro is_fl_functorI)
    (
      simp_all add: 
        assms(1) 
        is_fl_semifunctorI'[
          OF is_functorD(6)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_fl_functorD':
  assumes "𝔉 : 𝔄 ↩↩C.fullα 𝔅"
  shows "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "⋀a b. ⟩ a ∈∘ 𝔄⩇Obj⊈; b ∈∘ 𝔄⩇Obj⊈ ⟧ âŸč
    𝔉⩇ArrMap⩈ `∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⩇ObjMap⩈⩇a⩈) (𝔉⩇ObjMap⩈⩇b⩈)"
  by 
    (
      simp_all add: 
        is_fl_functorD[OF assms(1)] 
        is_fl_semifunctorD'(2)[
          OF is_fl_functorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_fl_functorE':
  assumes "𝔉 : 𝔄 ↩↩C.fullα 𝔅"
  obtains "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "⋀a b. ⟩ a ∈∘ 𝔄⩇Obj⊈; b ∈∘ 𝔄⩇Obj⊈ ⟧ âŸč 
    𝔉⩇ArrMap⩈ `∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⩇ObjMap⩈⩇a⩈) (𝔉⩇ObjMap⩈⩇b⩈)"
  using assms by (simp_all add: is_fl_functorD')


textâ€čElementary properties.â€ș

context is_fl_functor
begin

interpretation smcf: is_fl_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
  by (rule fl_cf_is_fl_semifunctor) 

lemmas_with [unfolded slicing_simps]:
  fl_cf_surj_on_Hom = smcf.fl_smcf_surj_on_Hom

end


subsubsectionâ€čOpposite full functorâ€ș

lemma (in is_fl_functor) is_fl_functor_op[cat_op_intros]: 
  "op_cf 𝔉 : op_cat 𝔄 ↩↩C.fullα op_cat 𝔅"    
  by (rule is_fl_functorI, unfold slicing_commute[symmetric])
    (simp_all add: cat_op_intros smc_op_intros slicing_intros)

lemmas is_fl_functor_op[cat_op_intros] = is_fl_functor.is_fl_functor_op


subsubsectionâ€čThe composition of full functor is a full functorâ€ș

lemma cf_comp_is_fl_functor[cf_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩C.fullα ℭ" and "𝔉 : 𝔄 ↩↩C.fullα 𝔅" 
  shows "𝔊 ∘CF 𝔉 : 𝔄 ↩↩C.fullα ℭ"
proof(intro is_fl_functorI)
  interpret 𝔉: is_fl_functor α 𝔄 𝔅 𝔉 using assms(2) by simp
  interpret 𝔊: is_fl_functor α 𝔅 ℭ 𝔊 using assms(1) by simp
  from 𝔉.is_functor_axioms 𝔊.is_functor_axioms show "𝔊 ∘CF 𝔉 : 𝔄 ↩↩Cα ℭ" 
    by (cs_concl cs_intro: cat_cs_intros)
  show "cf_smcf (𝔊 ∘CF 𝔉) : cat_smc 𝔄 ↩↩SMC.fullα cat_smc ℭ" 
    by 
      (
        cs_concl 
          cs_simp: slicing_commute[symmetric] 
          cs_intro: cf_cs_intros smcf_cs_intros slicing_intros
      )
qed



subsectionâ€čFully faithful functorâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș

locale is_ff_functor = is_ft_functor α 𝔄 𝔅 𝔉 + is_fl_functor α 𝔄 𝔅 𝔉
  for α 𝔄 𝔅 𝔉

syntax "_is_ff_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č(_ :/ _ ↩↩C.ffı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↩↩C.ffα 𝔅" ⇌ "CONST is_ff_functor α 𝔄 𝔅 𝔉"


textâ€čRules.â€ș

mk_ide rf is_ff_functor_def
  |intro is_ff_functorI|
  |dest is_ff_functorD[dest]|
  |elim is_ff_functorE[elim]|

lemmas [cf_cs_intros] = is_ff_functorD


textâ€čElementary properties.â€ș

lemma (in is_ff_functor) ff_cf_is_ff_semifunctor:
  "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.ffα cat_smc 𝔅"
  by (rule is_ff_semifunctorI) (auto intro: slicing_intros)

lemma (in is_ff_functor) ff_cf_is_ff_semifunctor'[slicing_intros]:
  assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMC.ffα 𝔅'"
  unfolding assms by (rule ff_cf_is_ff_semifunctor)

lemmas [slicing_intros] = is_ff_functor.ff_cf_is_ff_semifunctor'


subsubsectionâ€čOpposite fully faithful functorâ€ș

lemma (in is_ff_functor) is_ff_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↩↩C.ffα op_cat 𝔅"    
  by (rule is_ff_functorI) (auto simp: is_fl_functor_op is_ft_functor_op)

lemma (in is_ff_functor) is_ff_functor_op'[cat_op_intros]: 
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅"
  shows "op_cf 𝔉 : 𝔄' ↩↩C.ffα 𝔅'"
  unfolding assms by (rule is_ff_functor_op)

lemmas is_ff_functor_op[cat_op_intros] = is_ff_functor.is_ff_functor_op


subsubsectionâ€č
The composition of fully faithful functors is a fully faithful functor
â€ș

lemma cf_comp_is_ff_functor[cf_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩C.ffα ℭ" and "𝔉 : 𝔄 ↩↩C.ffα 𝔅"
  shows "𝔊 ∘CF 𝔉 : 𝔄 ↩↩C.ffα ℭ"
  using assms 
  by (intro is_ff_functorI, elim is_ff_functorE) (auto simp: cf_cs_intros)



subsectionâ€čIsomorphism of categoriesâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș

locale is_iso_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes iso_cf_is_iso_semifunctor: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.isoα cat_smc 𝔅"

syntax "_is_iso_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (â€č(_ :/ _ ↩↩C.isoı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↩↩C.isoα 𝔅" ⇌ "CONST is_iso_functor α 𝔄 𝔅 𝔉"

lemma (in is_iso_functor) iso_cf_is_iso_semifunctor'[slicing_intros]:
  assumes "𝔄' = cat_smc 𝔄" "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMC.isoα 𝔅'"
  unfolding assms by (rule iso_cf_is_iso_semifunctor)

lemmas [slicing_intros] = is_iso_semifunctor.iso_smcf_is_iso_dghm'


textâ€čRules.â€ș

lemma (in is_iso_functor) is_iso_functor_axioms'[cf_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↩↩C.isoα' 𝔅'"
  unfolding assms by (rule is_iso_functor_axioms)

mk_ide rf is_iso_functor_def[unfolded is_iso_functor_axioms_def]
  |intro is_iso_functorI|
  |dest is_iso_functorD[dest]|
  |elim is_iso_functorE[elim]|

lemma is_iso_functorI':
  assumes "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "v11 (𝔉⩇ObjMap⩈)"
    and "v11 (𝔉⩇ArrMap⩈)"
    and "ℛ∘ (𝔉⩇ObjMap⩈) = 𝔅⩇Obj⩈"
    and "ℛ∘ (𝔉⩇ArrMap⩈) = 𝔅⩇Arr⩈"
  shows "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
  using assms
  by (intro is_iso_functorI)
    (
      simp_all add: 
        assms(1) 
        is_iso_semifunctorI'[
          OF is_functorD(6)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_iso_functorD':
  assumes "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
  shows "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "v11 (𝔉⩇ObjMap⩈)"
    and "v11 (𝔉⩇ArrMap⩈)"
    and "ℛ∘ (𝔉⩇ObjMap⩈) = 𝔅⩇Obj⩈"
    and "ℛ∘ (𝔉⩇ArrMap⩈) = 𝔅⩇Arr⩈"
  by 
    (
      simp_all add: 
        is_iso_functorD[OF assms(1)] 
        is_iso_semifunctorD'(2-5)[
          OF is_iso_functorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_iso_functorE':
  assumes "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
  obtains "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "v11 (𝔉⩇ObjMap⩈)"
    and "v11 (𝔉⩇ArrMap⩈)"
    and "ℛ∘ (𝔉⩇ObjMap⩈) = 𝔅⩇Obj⩈"
    and "ℛ∘ (𝔉⩇ArrMap⩈) = 𝔅⩇Arr⩈"
  using assms by (simp_all add: is_iso_functorD')


textâ€čElementary properties.â€ș

context is_iso_functor
begin

interpretation smcf: is_iso_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
  by (rule iso_cf_is_iso_semifunctor) 

lemmas_with [unfolded slicing_simps]:
  iso_cf_ObjMap_vrange[simp] = smcf.iso_smcf_ObjMap_vrange
  and iso_cf_ArrMap_vrange[simp] = smcf.iso_smcf_ArrMap_vrange

sublocale ObjMap: v11 â€č𝔉⩇ObjMap⊈â€ș
  rewrites "𝒟∘ (𝔉⩇ObjMap⩈) = 𝔄⩇Obj⩈" and "ℛ∘ (𝔉⩇ObjMap⩈) = 𝔅⩇Obj⩈"
  by (rule smcf.ObjMap.v11_axioms[unfolded slicing_simps]) 
    (simp_all add: cat_cs_simps cf_cs_simps)
  
sublocale ArrMap: v11 â€č𝔉⩇ArrMap⊈â€ș
  rewrites "𝒟∘ (𝔉⩇ArrMap⩈) = 𝔄⩇Arr⩈" and "ℛ∘ (𝔉⩇ArrMap⩈) = 𝔅⩇Arr⩈"
  by (rule smcf.ArrMap.v11_axioms[unfolded slicing_simps])
    (simp_all add: cat_cs_simps smcf_cs_simps)

lemmas_with [unfolded slicing_simps]:
  iso_cf_Obj_HomDom_if_Obj_HomCod[elim] = 
    smcf.iso_smcf_Obj_HomDom_if_Obj_HomCod
  and iso_cf_Arr_HomDom_if_Arr_HomCod[elim] = 
    smcf.iso_smcf_Arr_HomDom_if_Arr_HomCod
  and iso_cf_ObjMap_eqE[elim] = smcf.iso_smcf_ObjMap_eqE
  and iso_cf_ArrMap_eqE[elim] = smcf.iso_smcf_ArrMap_eqE

end

sublocale is_iso_functor ⊆ is_ff_functor 
proof(intro is_ff_functorI)
  interpret is_iso_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
    by (rule iso_cf_is_iso_semifunctor)
  show "𝔉 : 𝔄 ↩↩C.faithfulα 𝔅" by unfold_locales
  show "𝔉 : 𝔄 ↩↩C.fullα 𝔅" by unfold_locales
qed

lemmas (in is_iso_functor) iso_cf_is_ff_functor = is_ff_functor_axioms
lemmas [cf_cs_intros] = is_iso_functor.iso_cf_is_ff_functor


subsubsectionâ€čOpposite isomorphism of categoriesâ€ș
 
lemma (in is_iso_functor) is_iso_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↩↩C.isoα op_cat 𝔅"   
  by (rule is_iso_functorI, unfold slicing_simps slicing_commute[symmetric]) 
   (simp_all add: cat_op_intros smc_op_intros slicing_intros)

lemma (in is_iso_functor) is_iso_functor_op': 
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅"
  shows "op_cf 𝔉 : op_cat 𝔄 ↩↩C.isoα op_cat 𝔅"   
  unfolding assms by (rule is_iso_functor_op)

lemmas is_iso_functor_op[cat_op_intros] = 
  is_iso_functor.is_iso_functor_op'


subsubsectionâ€č
The composition of isomorphisms of categories is an isomorphism of categories
â€ș

lemma cf_comp_is_iso_functor[cf_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩C.isoα ℭ" and "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
  shows "𝔊 ∘CF 𝔉 : 𝔄 ↩↩C.isoα ℭ"
proof(intro is_iso_functorI)
  interpret 𝔉: is_iso_functor α 𝔄 𝔅 𝔉 using assms by auto
  interpret 𝔊: is_iso_functor α 𝔅 ℭ 𝔊 using assms by auto
  from 𝔉.is_functor_axioms 𝔊.is_functor_axioms show "𝔊 ∘CF 𝔉 : 𝔄 ↩↩Cα ℭ" 
    by (cs_concl cs_intro: cat_cs_intros)
  show "cf_smcf (𝔊 ∘CF 𝔉) : cat_smc 𝔄 ↩↩SMC.isoα cat_smc ℭ"
    unfolding slicing_commute[symmetric] 
    by (cs_concl cs_intro: smcf_cs_intros slicing_intros)
qed



subsectionâ€čInverse functorâ€ș

abbreviation (input) inv_cf :: "V ⇒ V"
  where "inv_cf ≡ inv_dghm"


textâ€čSlicing.â€ș

lemma dghm_inv_semifunctor[slicing_commute]: 
  "inv_smcf (cf_smcf 𝔉) = cf_smcf (inv_cf 𝔉)"
  unfolding cf_smcf_def inv_dghm_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)

context is_iso_functor
begin

interpretation smcf: is_iso_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
  by (rule iso_cf_is_iso_semifunctor) 

lemmas_with [unfolded slicing_simps slicing_commute]:
  inv_cf_ObjMap_v11 = smcf.inv_smcf_ObjMap_v11
  and inv_cf_ObjMap_vdomain = smcf.inv_smcf_ObjMap_vdomain
  and inv_cf_ObjMap_app = smcf.inv_smcf_ObjMap_app
  and inv_cf_ObjMap_vrange = smcf.inv_smcf_ObjMap_vrange
  and inv_cf_ArrMap_v11 = smcf.inv_smcf_ArrMap_v11
  and inv_cf_ArrMap_vdomain = smcf.inv_smcf_ArrMap_vdomain
  and inv_cf_ArrMap_app = smcf.inv_smcf_ArrMap_app
  and inv_cf_ArrMap_vrange = smcf.inv_smcf_ArrMap_vrange
  and iso_cf_ObjMap_inv_cf_ObjMap_app =
    smcf.iso_smcf_ObjMap_inv_smcf_ObjMap_app
  and iso_cf_ArrMap_inv_cf_ArrMap_app = 
    smcf.iso_smcf_ArrMap_inv_smcf_ArrMap_app
  and iso_cf_HomDom_is_arr_conv = smcf.iso_smcf_HomDom_is_arr_conv
  and iso_cf_HomCod_is_arr_conv = smcf.iso_smcf_HomCod_is_arr_conv

end



subsectionâ€čAn isomorphism of categories is an isomorphism in the category â€čCATâ€șâ€ș

lemma is_arr_isomorphism_is_iso_functor:
  ―â€čSee Chapter I-3 in \cite{mac_lane_categories_2010}.â€ș
  assumes "𝔉 : 𝔄 ↩↩Cα 𝔅"
    and "𝔊 : 𝔅 ↩↩Cα 𝔄"
    and "𝔊 ∘CF 𝔉 = cf_id 𝔄"
    and "𝔉 ∘CF 𝔊 = cf_id 𝔅"
  shows "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
proof-
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 𝔄 𝔊 by (rule assms(2))
  show ?thesis
  proof(rule is_iso_functorI)
    have 𝔊𝔉𝔄: "cf_smcf 𝔊 ∘SMCF cf_smcf 𝔉 = smcf_id (cat_smc 𝔄)"
      by (simp add: assms(3) cf_smcf_cf_id cf_smcf_smcf_comp)
    have 𝔉𝔊𝔅: "cf_smcf 𝔉 ∘SMCF cf_smcf 𝔊 = smcf_id (cat_smc 𝔅)"
      by (simp add: assms(4) cf_smcf_cf_id cf_smcf_smcf_comp)
    from 𝔉.cf_is_semifunctor 𝔊.cf_is_semifunctor 𝔊𝔉𝔄 𝔉𝔊𝔅 show 
      "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.isoα cat_smc 𝔅" 
      by (rule is_arr_isomorphism_is_iso_semifunctor)
  qed (auto simp: cat_cs_intros)
qed

lemma is_iso_functor_is_arr_isomorphism:
  assumes "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
  shows [cf_cs_intros]: "inv_cf 𝔉 : 𝔅 ↩↩C.isoα 𝔄"
    and "inv_cf 𝔉 ∘CF 𝔉 = cf_id 𝔄"
    and "𝔉 ∘CF inv_cf 𝔉 = cf_id 𝔅"
proof-

  let ?𝔊 = "inv_cf 𝔉"

  interpret is_iso_functor α 𝔄 𝔅 𝔉 by (rule assms(1))

  show 𝔊: "?𝔊 : 𝔅 ↩↩C.isoα 𝔄"
  proof(intro is_iso_functorI is_functorI, unfold inv_dghm_components)
    show "vfsequence ?𝔊" by (simp add: inv_dghm_def)
    show "vcard ?𝔊 = 4ℕ"
      unfolding inv_dghm_def by (simp add: nat_omega_simps)
    show "cf_smcf ?𝔊 : cat_smc 𝔅 ↩↩SMCα cat_smc 𝔄"
      by 
        (
          metis 
            dghm_inv_semifunctor 
            iso_cf_is_iso_semifunctor 
            is_iso_semifunctor_def 
            is_iso_semifunctor_is_arr_isomorphism(1)
        ) 
    show "cf_smcf ?𝔊 : cat_smc 𝔅 ↩↩SMC.isoα cat_smc 𝔄"
      by 
        (
          metis 
            dghm_inv_semifunctor 
            iso_cf_is_iso_semifunctor 
            is_iso_semifunctor_is_arr_isomorphism(1)
        )
    fix c assume prems: "c ∈∘ 𝔅⩇Obj⩈"
    from prems show "(𝔉⩇ArrMap⩈)¯∘⩇𝔅⩇CId⩈⩇c⩈⩈ = 𝔄⩇CId⩈⩇(𝔉⩇ObjMap⩈)¯∘⩇c⩈⩈"
      by (intro v11.v11_vconverse_app)
        (
           cs_concl 
            cs_intro: cat_cs_intros V_cs_intros
            cs_simp: V_cs_simps cat_cs_simps
         )+
  qed (simp_all add: cat_cs_simps cat_cs_intros)

  show "?𝔊 ∘CF 𝔉 = cf_id 𝔄"
  proof(rule cf_eqI, unfold dghm_comp_components inv_dghm_components)
    from 𝔊 is_functor_axioms show "?𝔊 ∘CF 𝔉 : 𝔄 ↩↩Cα 𝔄" 
      by (blast intro: cat_cs_intros)
  qed 
    (
      simp_all add: 
        HomDom.cat_cf_id_is_functor
        ObjMap.v11_vcomp_vconverse 
        ArrMap.v11_vcomp_vconverse 
        dghm_id_components
    )

  show "𝔉 ∘CF ?𝔊 = cf_id 𝔅"
  proof(rule cf_eqI, unfold dghm_comp_components inv_dghm_components)
    from 𝔊 is_functor_axioms show "𝔉 ∘CF ?𝔊 : 𝔅 ↩↩Cα 𝔅" 
      by (blast intro: cat_cs_intros)
    show "cf_id 𝔅 : 𝔅 ↩↩Cα 𝔅" by (simp add: HomCod.cat_cf_id_is_functor)
  qed 
    (
      simp_all add:
        ObjMap.v11_vcomp_vconverse' 
        ArrMap.v11_vcomp_vconverse' 
        dghm_id_components
    )

qed


subsubsectionâ€čAn identity functor is an isomorphism of categoriesâ€ș

lemma (in category) cat_cf_id_is_iso_functor: "cf_id ℭ : ℭ ↩↩C.isoα ℭ"
  by (rule is_iso_functorI, unfold slicing_commute[symmetric])
    (
      simp_all add: 
        cat_cf_id_is_functor
        semicategory.smc_smcf_id_is_iso_semifunctor
        cat_semicategory
    )



subsectionâ€čIsomorphic categoriesâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș


textâ€čSee Chapter I-3 in \cite{mac_lane_categories_2010}).â€ș

locale iso_category = L: category α 𝔄 + R: category α 𝔅 for α 𝔄 𝔅 +
  assumes iso_cat_is_iso_functor: "∃𝔉. 𝔉 : 𝔄 ↩↩C.isoα 𝔅"

notation iso_category (infixl "≈Cı" 50)


textâ€čRules.â€ș

lemma iso_categoryI:
  assumes "𝔉 : 𝔄 ↩↩C.isoα 𝔅" 
  shows "𝔄 ≈Cα 𝔅"
  using assms unfolding iso_category_def iso_category_axioms_def by auto

lemma iso_categoryD[dest]:
  assumes "𝔄 ≈Cα 𝔅" 
  shows "∃𝔉. 𝔉 : 𝔄 ↩↩C.isoα 𝔅" 
  using assms unfolding iso_category_def iso_category_axioms_def by simp_all

lemma iso_categoryE[elim]:
  assumes "𝔄 ≈Cα 𝔅" 
  obtains 𝔉 where "𝔉 : 𝔄 ↩↩C.isoα 𝔅"
  using assms by auto


textâ€čIsomorphic categories are isomorphic semicategories.â€ș

lemma (in iso_category) iso_cat_iso_semicategory: 
  "cat_smc 𝔄 ≈SMCα cat_smc 𝔅"
  using iso_cat_is_iso_functor 
  by (auto intro: slicing_intros iso_semicategoryI)


subsubsectionâ€čA category isomorphism is an equivalence relationâ€ș

lemma iso_category_refl: 
  assumes "category α 𝔄" 
  shows "𝔄 ≈Cα 𝔄"
proof(rule iso_categoryI[of _ _ _ â€čcf_id 𝔄â€ș])
  interpret category α 𝔄 by (rule assms)
  show "cf_id 𝔄 : 𝔄 ↩↩C.isoα 𝔄" by (simp add: cat_cf_id_is_iso_functor)
qed                                        

lemma iso_category_sym[sym]:
  assumes "𝔄 ≈Cα 𝔅" 
  shows "𝔅 ≈Cα 𝔄"
proof-
  interpret iso_category α 𝔄 𝔅 by (rule assms)
  from iso_cat_is_iso_functor obtain 𝔉 where "𝔉 : 𝔄 ↩↩C.isoα 𝔅" by clarsimp
  from is_iso_functor_is_arr_isomorphism(1)[OF this] show ?thesis 
    by (auto intro: iso_categoryI)
qed

lemma iso_category_trans[trans]:
  assumes "𝔄 ≈Cα 𝔅" and "𝔅 ≈Cα ℭ" 
  shows "𝔄 ≈Cα ℭ"
proof-
  interpret L: iso_category α 𝔄 𝔅 by (rule assms(1))
  interpret R: iso_category α 𝔅 ℭ by (rule assms(2))
  from L.iso_cat_is_iso_functor R.iso_cat_is_iso_functor show ?thesis 
    by (auto intro: iso_categoryI is_iso_functorI cf_comp_is_iso_functor)
qed

textâ€č\newpageâ€ș

end

Theory CZH_ECAT_Small_Functor

(* Copyright 2021 (C) Mihails Milehins *)

sectionâ€čSmallness for functorsâ€ș
theory CZH_ECAT_Small_Functor
  imports 
    CZH_Foundations.CZH_SMC_Small_Semifunctor
    CZH_ECAT_Functor
    CZH_ECAT_Small_Category
begin



subsectionâ€čFunctor with tiny mapsâ€ș


subsubsectionâ€čDefinition and elementary propertiesâ€ș

locale is_tm_functor = is_functor α 𝔄 𝔅 𝔉  for α 𝔄 𝔅 𝔉 +
  assumes tm_cf_is_semifunctor[slicing_intros]: 
    "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.tmα cat_smc 𝔅" 

syntax "_is_tm_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (â€č(_ :/ _ ↩↩C.tmı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↩↩C.tmα 𝔅" ⇌ "CONST is_tm_functor α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_tm_functor :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_tm_functor α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_dg 𝔄 ↩↩C.tmα 𝔅"

syntax "_is_cn_tm_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (â€č(_ :/ _ C.tm↊↊ı _)â€ș [51, 51, 51] 51)
translations "𝔉 : 𝔄 C.tm↊↊α 𝔅" ⇀ "CONST is_cn_tm_functor α 𝔄 𝔅 𝔉"

abbreviation all_tm_cfs :: "V ⇒ V"
  where "all_tm_cfs α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩C.tmα 𝔅}"

abbreviation small_tm_cfs :: "V ⇒ V ⇒ V ⇒ V"
  where "small_tm_cfs α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↩↩C.tmα 𝔅}"

lemma (in is_tm_functor) tm_cf_is_semifunctor':
  assumes "α' = α"
    and "𝔄' = cat_smc 𝔄"
    and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↩↩SMC.tmα' 𝔅'"
  unfolding assms by (rule tm_cf_is_semifunctor)

lemmas [slicing_intros] = is_tm_functor.tm_cf_is_semifunctor'


textâ€čRules.â€ș

lemma (in is_tm_functor) is_tm_functor_axioms'[cat_small_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↩↩C.tmα' 𝔅'"
  unfolding assms by (rule is_tm_functor_axioms)

mk_ide rf is_tm_functor_def[unfolded is_tm_functor_axioms_def]
  |intro is_tm_functorI|
  |dest is_tm_functorD[dest]|
  |elim is_tm_functorE[elim]|

lemmas [cat_small_cs_intros] = is_tm_functorD(1)


textâ€čSlicing.â€ș

context is_tm_functor
begin

interpretation smcf: is_tm_semifunctor α â€čcat_smc 𝔄â€ș â€čcat_smc 𝔅â€ș â€čcf_smcf 𝔉â€ș
  by (rule tm_cf_is_semifunctor)

lemmas_with [unfolded slicing_simps]:
  tm_cf_ObjMap_in_Vset[cat_cs_intros] = smcf.tm_smcf_ObjMap_in_Vset
  and tm_cf_ArrMap_in_Vset[cat_cs_intros] = smcf.tm_smcf_ArrMap_in_Vset

end

sublocale is_tm_functor ⊆ HomDom: tiny_category α 𝔄
proof(rule tiny_categoryI')
  show "𝔄⩇Obj⊈ ∈∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_cf_ObjMap_in_Vset, unfolded cat_cs_simps])
  show "𝔄⩇Arr⊈ ∈∘ Vset α"
    by (rule vdomain_in_VsetI[OF tm_cf_ArrMap_in_Vset, unfolded cat_cs_simps])
qed (simp add: cat_cs_intros)


textâ€čFurther rules.â€ș

lemma is_tm_functorI':
  assumes [simp]: "𝔉 : 𝔄 ↩↩Cα 𝔅" 
    and [simp]: "𝔉⩇ObjMap⊈ ∈∘ Vset α"
    and [simp]: "𝔉⩇ArrMap⊈ ∈∘ Vset α"
  shows "𝔉 : 𝔄 ↩↩C.tmα 𝔅"
proof(intro is_tm_functorI)
  interpret is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  show "cf_smcf 𝔉 : cat_smc 𝔄 ↩↩SMC.tmα cat_smc 𝔅"
    by (intro is_tm_semifunctorI', unfold slicing_simps) 
      (auto simp: slicing_intros)
qed simp_all

lemma is_tm_functorD':
  assumes "𝔉 : 𝔄 ↩↩C.tmα 𝔅"
  shows "𝔉 : 𝔄 ↩↩Cα 𝔅" 
    and "𝔉⩇ObjMap⊈ ∈∘ Vset α"
    and "𝔉⩇ArrMap⊈ ∈∘ Vset α"
proof-
  interpret is_tm_functor α 𝔄 𝔅 𝔉 by (rule assms(1))    
  show "𝔉 : 𝔄 ↩↩Cα 𝔅" 
    and "𝔉⩇ObjMap⊈ ∈∘ Vset α"
    and "𝔉⩇ArrMap⊈ ∈∘ Vset α"
    by (auto intro: cat_cs_intros)
qed

lemmas [cat_small_cs_intros] = is_tm_functorD'(1)

lemma is_tm_functorE':
  assumes "𝔉 : 𝔄 ↩↩C.tmα 𝔅"
  obtains "𝔉 : 𝔄 ↩↩Cα 𝔅" 
    and "𝔉⩇ObjMap⊈ ∈∘ Vset α"
    and "𝔉⩇ArrMap⊈ ∈∘ Vset α"
  using is_tm_functorD'[OF assms] by simp


textâ€čSize.â€ș

lemma small_all_tm_cfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩C.tmα 𝔅}"
proof(rule down)
  show 
    "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩C.tmα 𝔅} ⊆
      elts (set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩Cα 𝔅})"
  proof
    (
      simp only: elts_of_set small_all_cfs if_True, 
      rule subsetI, 
      unfold mem_Collect_eq
    )
    fix 𝔉 assume "∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩C.tmα 𝔅"
    then obtain 𝔄 𝔅 where "𝔉 : 𝔄 ↩↩C.tmα 𝔅" by clarsimp
    then interpret is_tm_functor α 𝔄 𝔅 𝔉 .
    show "∃𝔄 𝔅. 𝔉 : 𝔄 ↩↩Cα 𝔅" by (blast intro: is_functor_axioms')
  qed
qed


subsubsectionâ€čOpposite functor with tiny mapsâ€ș

lemma (in is_tm_functor) is_tm_functor_op: 
  "op_cf 𝔉 : op_cat 𝔄 ↩↩C.tmα op_cat 𝔅"
  by (intro is_tm_functorI', unfold cat_op_simps)
    (cs_concl cs_intro: cat_cs_intros cat_op_intros)

lemma (in is_tm_functor) is_tm_functor_op'[cat_op_intros]:  
  assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅" and "α' = α"
  shows "op_cf 𝔉 : 𝔄' ↩↩C.tmα' 𝔅'"
  unfolding assms by (rule is_tm_functor_op)

lemmas is_tm_functor_op[cat_op_intros] = is_tm_functor.is_tm_functor_op'


subsubsectionâ€čComposition of functors with tiny mapsâ€ș

lemma cf_comp_is_tm_functor[cat_small_cs_intros]:
  assumes "𝔊 : 𝔅 ↩↩C.tmα ℭ" and "𝔉 : 𝔄 ↩↩C.tmα 𝔅"
  shows "𝔊 ∘CF 𝔉 : 𝔄 ↩↩