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 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 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)
syntax_consts "_is_functor" ⇌ is_functor
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)
syntax_consts "_is_cn_cf" ⇌ is_cn_cf
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 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
  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 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙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 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
  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_shallow cs_simp: cat_cs_simps V_cs_simps)
  show "𝒟⇩∘ 𝔊 = 𝒟⇩∘ 𝔉" by (cs_concl cs_shallow 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_shallow 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_shallow 
          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_shallow 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_shallow 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_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma small_cfs[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
  by (rule down[of _ ‹set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}›]) auto


subsubsection‹Further properties›

lemma (in is_functor) cf_ArrMap_is_iso_arr:
  assumes "f : a ↦⇩i⇩s⇩o⇘𝔄⇙ b"
  shows "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
proof-

  note f = is_iso_arrD(1)[OF assms(1)]
  note HomDom.cat_the_inverse_is_iso_arr[OF assms]
  note inv_f = this is_iso_arrD(1)[OF this]

  show ?thesis
  proof(intro is_iso_arrI is_inverseI)
    from inv_f(2) show 𝔉_inv_f: 
      "𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ : 𝔉⦇ObjMap⦈⦇b⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
      by (cs_concl cs_intro: cat_cs_intros)
    note cf_ArrMap_Comp is_functor.cf_ArrMap_Comp[cat_cs_simps del]
    from assms f(1) inv_f show 
      "𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
      "𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇b⦈⦈"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cf_ArrMap_Comp[symmetric] 
            cs_intro: cat_cs_intros
        )+
  qed (intro cf_ArrMap_is_arr[OF f(1)])+

qed

lemma (in is_functor) cf_ArrMap_is_iso_arr'[cat_arrow_cs_intros]:
  assumes "f : a ↦⇩i⇩s⇩o⇘𝔄⇙ b" and "𝔉a = 𝔉⦇ObjMap⦈⦇a⦈" and "𝔉b = 𝔉⦇ObjMap⦈⦇b⦈"
  shows "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉a ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉b"
  using assms(1) unfolding assms(2,3) by (rule cf_ArrMap_is_iso_arr)

lemmas [cat_arrow_cs_intros] = is_functor.cf_ArrMap_is_iso_arr'



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 ‹∘⇩C⇩F› 55)
  where "cf_comp ≡ dghm_comp"


text‹Slicing.›

lemma cf_smcf_smcf_comp[slicing_commute]: 
  "cf_smcf 𝔊 ∘⇩S⇩M⇩C⇩F cf_smcf 𝔉 = cf_smcf (𝔊 ∘⇩C⇩F 𝔉)"
  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 ((𝔊 ∘⇩C⇩F 𝔉)⦇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 "𝒟⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇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 "ℛ⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇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 "(𝔊 ∘⇩C⇩F 𝔉)⦇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 ((𝔊 ∘⇩C⇩F 𝔉)⦇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 "𝒟⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇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 "ℛ⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇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 "(𝔊 ∘⇩C⇩F 𝔉)⦇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 "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩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 (𝔊 ∘⇩C⇩F 𝔉)" by (simp add: dghm_comp_def)
    show "vcard (𝔊 ∘⇩C⇩F 𝔉) = 4⇩ℕ"  
      unfolding dghm_comp_def by (simp add: nat_omega_simps)
    show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 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 "(𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇(𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇c⦈⦈"
      by (cs_concl cs_shallow 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 "(ℌ ∘⇩C⇩F 𝔊) ∘⇩C⇩F 𝔉 = ℌ ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉)"
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 "ℌ ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔇" and "ℌ ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩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 (𝔊 ∘⇩C⇩F 𝔉) = op_cf 𝔊 ∘⇩C⇩F op_cf 𝔉"
  unfolding dghm_comp_def op_cf_def dghm_field_simps
  by (simp add: nat_omega_simps)


text‹Composition helper.›

lemma cf_comp_assoc_helper: 
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "ℌ : ℭ ↦↦⇩C⇘α⇙ 𝔇"
    and "ℌ ∘⇩C⇩F 𝔊 = 𝒬"
  shows "ℌ ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉) = 𝒬 ∘⇩C⇩F 𝔉"
proof-
  interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
  interpret ℌ: is_functor α ℭ 𝔇 ℌ by (rule assms(3))
  show ?thesis
    using assms(1-3) unfolding assms(4)[symmetric]
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed



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 ‹⇩C⇩F∘› 55)
  where "𝔊 ⇩C⇩F∘ 𝔉 =
    [
      𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈,
      𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈,
      op_cat (𝔉⦇HomDom⦈),
      𝔊⦇HomCod⦈
    ]⇩∘"


text‹Components.›

lemma cf_cn_comp_components:
  shows "(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈ = 𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
    and "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈ = 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈"
    and [cat_cn_cs_simps]: "(𝔊 ⇩C⇩F∘ 𝔉)⦇HomDom⦈ = op_cat (𝔉⦇HomDom⦈)"
    and [cat_cn_cs_simps]: "(𝔊 ⇩C⇩F∘ 𝔉)⦇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 𝔊 ⇩S⇩M⇩C⇩F∘ cf_smcf 𝔉 = cf_smcf (𝔊 ⇩C⇩F∘ 𝔉)"
  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 ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "(𝔊 ⇩C⇩F∘ 𝔉)⦇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 ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "(𝔊 ⇩C⇩F∘ 𝔉)⦇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 ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "(𝔊 ⇩C⇩F∘ 𝔉)⦇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 ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇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 "(𝔊 ⇩C⇩F∘ 𝔉)⦇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 "𝔊 ⇩C⇩F∘ 𝔉 : 𝔄 ↦↦⇩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 (𝔊 ⇩C⇩F∘ 𝔉)"
      unfolding cf_cn_comp_def by (simp add: nat_omega_simps)
    show "vcard (𝔊 ⇩C⇩F∘ 𝔉) = 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 (𝔊 ⇩C⇩F∘ 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      unfolding cf_smcf_cf_cn_comp[symmetric] 
      by 
        (
          cs_concl cs_shallow 
            cs_intro: cat_cs_intros slicing_intros smc_cn_cs_intros
        )
    fix c assume "c ∈⇩∘ 𝔄⦇Obj⦈"
    with assms show 
      "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇c⦈⦈"
      by 
        (
          cs_concl cs_shallow
            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 "𝔊 ⇩C⇩F∘ 𝔉 : 𝔄 ⇩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 (𝔊 ⇩C⇩F∘ 𝔉)" unfolding cf_cn_comp_def by simp
    show "vcard (𝔊 ⇩C⇩F∘ 𝔉) = 4⇩ℕ"
      unfolding cf_cn_comp_def by (auto simp: nat_omega_simps)
    from L.cf_is_semifunctor show 
      "cf_smcf 𝔊 ⇩S⇩M⇩C⇩F∘ cf_smcf 𝔉 : op_smc (cat_smc 𝔄) ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
      by 
        (
          cs_concl cs_shallow 
            cs_intro: cat_cs_intros slicing_intros smc_cs_intros
        )
    fix c assume "c ∈⇩∘ 𝔄⦇Obj⦈"
    with assms show "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇(𝔊 ⇩C⇩F∘ 𝔉)⦇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 "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ⇩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 (𝔊 ⇩C⇩F∘ 𝔉) = op_cf 𝔊 ⇩C⇩F∘ 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 ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 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 𝔅 ∘⇩C⇩F 𝔉 = 𝔉"
  ―‹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]: "𝔉 ∘⇩C⇩F 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 ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔇"
      by 
        ( 
          cs_concl cs_shallow
            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_shallow 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 "𝔅 = 𝔇"
    and "f = (𝔇⦇CId⦈⦇a⦈)"
  shows "dghm_const ℭ 𝔇 a f : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
  using assms(1-3) unfolding assms(4-6) by (rule cf_const_is_functor)


subsubsection‹Further properties›

lemma cf_comp_cf_const_right[cat_cs_simps]:
  assumes "category α 𝔄"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)"
proof(rule cf_eqI)

  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))

  from assms(3) show "𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_intro: cat_cs_intros)
  from assms(3) show "cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈) : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(3) have ObjMap_dom_lhs: 
    "𝒟⇩∘ ((𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(3) have ObjMap_dom_rhs: 
    "𝒟⇩∘ (cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ObjMap⦈ = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈"
  proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
    fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
    with assms(3) show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ObjMap⦈⦇a⦈ =
      cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈⦇a⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto intro: assms(3) cat_cs_intros)
  from assms(3) have ArrMap_dom_lhs: 
    "𝒟⇩∘ ((𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(3) have ArrMap_dom_rhs: 
    "𝒟⇩∘ (cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ArrMap⦈ = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
    fix a assume "a ∈⇩∘ 𝔄⦇Arr⦈"
    with assms(3) show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ArrMap⦈⦇a⦈ =
      cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈⦇a⦈"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto intro: assms(3) cat_cs_intros)

qed simp_all

lemma cf_comp_cf_const_right'[cat_cs_simps]:
  assumes "category α 𝔄"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
    and "f = 𝔅⦇CId⦈⦇b⦈"
  shows "𝔊 ∘⇩C⇩F dghm_const 𝔄 𝔅 b f = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)"
  using assms(1-3) unfolding assms(4) by (rule cf_comp_cf_const_right)

lemma (in is_functor) cf_comp_cf_const_left[cat_cs_simps]:
  assumes "category α ℭ" and "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "cf_const 𝔅 ℭ a ∘⇩C⇩F 𝔉 = cf_const 𝔄 ℭ a"
proof(rule cf_smcf_eqI)
  interpret ℭ: category α ℭ by (rule assms(1))
  from assms(2) show "cf_const 𝔅 ℭ a ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms(2) show "cf_const 𝔄 ℭ a : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms(2) have CId_a: "ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms(2) have CId_CId_a: "ℭ⦇CId⦈⦇a⦈ ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇a⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from 
    is_semifunctor.smcf_smcf_comp_smcf_const
      [
        OF cf_is_semifunctor ℭ.cat_semicategory, 
        unfolded slicing_simps, 
        OF CId_a CId_CId_a
      ]
  show "cf_smcf (cf_const 𝔅 ℭ a ∘⇩D⇩G⇩H⇩M 𝔉) = cf_smcf (cf_const 𝔄 ℭ a)"
    by (cs_prems cs_shallow cs_simp: slicing_simps slicing_commute)
qed simp_all

lemma (in is_functor) cf_comp_cf_const_left'[cat_cs_simps]:
  assumes "category α ℭ" 
    and "a ∈⇩∘ ℭ⦇Obj⦈"
    and "f = ℭ⦇CId⦈⦇a⦈"
  shows "dghm_const 𝔅 ℭ a f ∘⇩C⇩F 𝔉 = cf_const 𝔄 ℭ a"
  using assms(1,2) unfolding assms(3) by (rule cf_comp_cf_const_left)

lemmas [cat_cs_simps] = is_functor.cf_comp_cf_const_left'



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 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ cat_smc 𝔅"

syntax "_is_ft_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩lı _)› [51, 51, 51] 51)
syntax_consts "_is_ft_functor" ⇌ is_ft_functor
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅" ⇌ "CONST is_ft_functor α 𝔄 𝔅 𝔉"

lemma (in is_ft_functor) ft_cf_is_ft_functor':
  assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
  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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α'⇙ 𝔅'"
  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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
  using assms by (simp_all add: is_ft_functorD')

lemma is_ft_functorI'':
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "⋀a b g f.
      ⟦ g : a ↦⇘𝔄⇙ b; f : a ↦⇘𝔄⇙ b; 𝔉⦇ArrMap⦈⦇g⦈ = 𝔉⦇ArrMap⦈⦇f⦈ ⟧ ⟹ g = f"
  shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  by 
    (
      intro is_ft_functorI assms,
      rule is_ft_semifunctorI'', 
      unfold slicing_simps, 
      rule is_functor.cf_is_semifunctor[OF assms(1)], 
      rule assms(2)
    )


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
  and ft_cf_ArrMap_eqD = smcf.ft_smcf_ArrMap_eqD

end


subsubsection‹Opposite faithful functor.›

lemma (in is_ft_functor) is_ft_functor_op': 
  "op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ"
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 "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  then interpret is_functor α 𝔄 ℭ ‹𝔊 ∘⇩C⇩F 𝔉› .
  show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 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 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ cat_smc 𝔅"

syntax "_is_fl_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦↦⇩C⇩.⇩f⇩u⇩l⇩lı _)› [51, 51, 51] 51)
syntax_consts "_is_fl_functor" ⇌ is_fl_functor
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" ⇌ "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 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅'"
  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⇩.⇩f⇩u⇩l⇩l⇘α'⇙ 𝔅'"
  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⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
  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⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
  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⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
  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⇩.⇩f⇩u⇩l⇩l⇘α⇙ 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⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" 
  shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ"
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 "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 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⇩.⇩f⇩fı _)› [51, 51, 51] 51)
syntax_consts "_is_ff_functor" ⇌ is_ff_functor
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩f⇘α⇙ 𝔅" ⇌ "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 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 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 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅'"
  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⇩.⇩f⇩f⇘α⇙ 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⇩.⇩f⇩f⇘α⇙ 𝔅'"
  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⇩.⇩f⇩f⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩f⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩f⇘α⇙ ℭ"
  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 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ cat_smc 𝔅"

syntax "_is_iso_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦↦⇩C⇩.⇩i⇩s⇩oı _)› [51, 51, 51] 51)
syntax_consts "_is_iso_functor" ⇌ is_iso_functor
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" ⇌ "CONST is_iso_functor α 𝔄 𝔅 𝔉"

lemma (in is_iso_functor) iso_cf_is_iso_semifunctor'[slicing_intros]:
  assumes "𝔄' = cat_smc 𝔄" "𝔅' = cat_smc 𝔅"
  shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅'"
  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⇩.⇩i⇩s⇩o⇘α'⇙ 𝔅'"
  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⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  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⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  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⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  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⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅" by unfold_locales
  show "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" 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⇩.⇩i⇩s⇩o⇘α⇙ 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⇩.⇩i⇩s⇩o⇘α⇙ 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⇩.⇩i⇩s⇩o⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
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 "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ cat_smc ℭ"
    unfolding slicing_commute[symmetric] 
    by (cs_concl cs_shallow 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[cf_cs_simps] =
    smcf.iso_smcf_ObjMap_inv_smcf_ObjMap_app
  and iso_cf_ArrMap_inv_cf_ArrMap_app[cf_cs_simps] = 
    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
  and iso_inv_cf_ObjMap_cf_ObjMap_app[cf_cs_simps] =
    smcf.iso_inv_smcf_ObjMap_smcf_ObjMap_app
  and iso_inv_cf_ArrMap_cf_ArrMap_app[cf_cs_simps] =
    smcf.iso_inv_smcf_ArrMap_smcf_ArrMap_app

end

lemmas [cf_cs_intros] = 
  is_iso_functor.inv_cf_ObjMap_v11
  is_iso_functor.inv_cf_ArrMap_v11

lemmas [cf_cs_simps] = 
  is_iso_functor.inv_cf_ObjMap_vdomain
  is_iso_functor.inv_cf_ObjMap_app
  is_iso_functor.inv_cf_ObjMap_vrange
  is_iso_functor.inv_cf_ArrMap_vdomain
  is_iso_functor.inv_cf_ArrMap_app
  is_iso_functor.inv_cf_ArrMap_vrange
  is_iso_functor.iso_cf_ObjMap_inv_cf_ObjMap_app
  is_iso_functor.iso_cf_ArrMap_inv_cf_ArrMap_app
  is_iso_functor.iso_inv_cf_ObjMap_cf_ObjMap_app
  is_iso_functor.iso_inv_cf_ArrMap_cf_ArrMap_app



subsection‹An isomorphism of categories is an isomorphism in the category ‹CAT››

lemma is_iso_arr_is_iso_functor:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}.›
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
    and "𝔊 ∘⇩C⇩F 𝔉 = cf_id 𝔄"
    and "𝔉 ∘⇩C⇩F 𝔊 = cf_id 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
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 𝔊 ∘⇩S⇩M⇩C⇩F cf_smcf 𝔉 = smcf_id (cat_smc 𝔄)"
      by (simp add: assms(3) cf_smcf_cf_id cf_smcf_smcf_comp)
    have 𝔉𝔊𝔅: "cf_smcf 𝔉 ∘⇩S⇩M⇩C⇩F 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 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ cat_smc 𝔅" 
      by (rule is_iso_arr_is_iso_semifunctor)
  qed (auto simp: cat_cs_intros)
qed

lemma is_iso_functor_is_iso_arr:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows [cf_cs_intros]: "inv_cf 𝔉 : 𝔅 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
    and [cf_cs_simps]: "inv_cf 𝔉 ∘⇩C⇩F 𝔉 = cf_id 𝔄"
    and [cf_cs_simps]: "𝔉 ∘⇩C⇩F inv_cf 𝔉 = cf_id 𝔅"
proof-

  let ?𝔊 = "inv_cf 𝔉"

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

  show 𝔊: "?𝔊 : 𝔅 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
  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 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔄"
      by 
        (
          metis 
            dghm_inv_semifunctor 
            iso_cf_is_iso_semifunctor 
            is_iso_semifunctor_def 
            is_iso_semifunctor_is_iso_arr(1)
        ) 
    show "cf_smcf ?𝔊 : cat_smc 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ cat_smc 𝔄"
      by 
        (
          metis 
            dghm_inv_semifunctor 
            iso_cf_is_iso_semifunctor 
            is_iso_semifunctor_is_iso_arr(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_shallow
            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 "?𝔊 ∘⇩C⇩F 𝔉 = cf_id 𝔄"
  proof(rule cf_eqI, unfold dghm_comp_components inv_dghm_components)
    from 𝔊 is_functor_axioms show "?𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩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 "𝔉 ∘⇩C⇩F ?𝔊 = cf_id 𝔅"
  proof(rule cf_eqI, unfold dghm_comp_components inv_dghm_components)
    from 𝔊 is_functor_axioms show "𝔉 ∘⇩C⇩F ?𝔊 : 𝔅 ↦↦⇩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⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
  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⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"

notation iso_category (infixl ‹≈⇩Cı› 50)


text‹Rules.›

lemma iso_categoryI:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" 
  shows "𝔄 ≈⇩C⇘α⇙ 𝔅"
  using assms unfolding iso_category_def iso_category_axioms_def by auto

lemma iso_categoryD[dest]:
  assumes "𝔄 ≈⇩C⇘α⇙ 𝔅" 
  shows "∃𝔉. 𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" 
  using assms unfolding iso_category_def iso_category_axioms_def by simp_all

lemma iso_categoryE[elim]:
  assumes "𝔄 ≈⇩C⇘α⇙ 𝔅" 
  obtains 𝔉 where "𝔉 : 𝔄 ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using assms by auto


text‹Isomorphic categories are isomorphic semicategories.›

lemma (in iso_category) iso_cat_iso_semicategory: 
  "cat_smc 𝔄 ≈⇩S⇩M⇩C⇘α⇙ 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⇩.⇩i⇩s⇩o⇘α⇙ 𝔄" 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⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" by clarsimp
  from is_iso_functor_is_iso_arr(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