Theory CZH_SMC_Semifunctor

(* Copyright 2021 (C) Mihails Milehins *)

section‹Semifunctor›
theory CZH_SMC_Semifunctor
  imports 
    CZH_DG_DGHM
    CZH_SMC_Semicategory
begin



subsection‹Background›

named_theorems smcf_cs_simps
named_theorems smcf_cs_intros

named_theorems smc_cn_cs_simps
named_theorems smc_cn_cs_intros

lemmas [smc_cs_simps] = dg_shared_cs_simps
lemmas [smc_cs_intros] = dg_shared_cs_intros


subsubsection‹Slicing›

definition smcf_dghm :: "V ⇒ V"
  where "smcf_dghm ℭ = 
    [ℭ⦇ObjMap⦈, ℭ⦇ArrMap⦈, smc_dg (ℭ⦇HomDom⦈), smc_dg (ℭ⦇HomCod⦈)]⇩∘"


text‹Components.›

lemma smcf_dghm_components:
  shows [slicing_simps]: "smcf_dghm 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    and [slicing_simps]: "smcf_dghm 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    and [slicing_commute]: "smcf_dghm 𝔉⦇HomDom⦈ = smc_dg (𝔉⦇HomDom⦈)"
    and [slicing_commute]: "smcf_dghm 𝔉⦇HomCod⦈ = smc_dg (𝔉⦇HomCod⦈)"
  unfolding smcf_dghm_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"› and the description
of the concept of a digraph homomorphism in the previous chapter.
›

locale is_semifunctor = 
  𝒵 α +
  vfsequence 𝔉 + 
  HomDom: semicategory α 𝔄 + 
  HomCod: semicategory α 𝔅 
  for α 𝔄 𝔅 𝔉 +
  assumes smcf_length[smc_cs_simps]: "vcard 𝔉 = 4⇩ℕ" 
    and smcf_is_dghm[slicing_intros]: 
      "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔅" 
    and smcf_HomDom[smc_cs_simps]: "𝔉⦇HomDom⦈ = 𝔄"
    and smcf_HomCod[smc_cs_simps]: "𝔉⦇HomCod⦈ = 𝔅"
    and smcf_ArrMap_Comp[smc_cs_simps]: "⟦ g : b ↦⇘𝔄⇙ c; f : a ↦⇘𝔄⇙ b ⟧ ⟹
      𝔉⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"

syntax "_is_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦↦⇩S⇩M⇩Cı _)› [51, 51, 51] 51)
syntax_consts "_is_semifunctor" ⇌ is_semifunctor
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" ⇌ "CONST is_semifunctor α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_semifunctor :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_cn_semifunctor α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"

syntax "_is_cn_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" 
  (‹(_ :/ _ ⇩S⇩M⇩C↦↦ı _)› [51, 51, 51] 51)
syntax_consts "_is_cn_semifunctor" ⇌ is_cn_semifunctor
translations "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_semifunctor α 𝔄 𝔅 𝔉"

abbreviation all_smcfs :: "V ⇒ V"
  where "all_smcfs α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"

abbreviation smcfs :: "V ⇒ V ⇒ V ⇒ V"
  where "smcfs α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"

lemmas [smc_cs_simps] =
  is_semifunctor.smcf_HomDom
  is_semifunctor.smcf_HomCod
  is_semifunctor.smcf_ArrMap_Comp

lemma smcf_is_dghm'[slicing_intros]:
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔄' = smc_dg 𝔄"
    and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
  using assms(1) unfolding assms(2,3) by (rule is_semifunctor.smcf_is_dghm)

lemma cn_dghm_comp_is_dghm: 
  assumes "𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "smcf_dghm 𝔉 : op_dg (smc_dg 𝔄) ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔅"
  using assms 
  unfolding slicing_simps slicing_commute
  by (cs_concl cs_shallow cs_intro: slicing_intros)

lemma cn_dghm_comp_is_dghm'[slicing_intros]: 
  assumes "𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔄' = op_dg (smc_dg 𝔄)"
    and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
  using assms(1) unfolding assms(2,3) by (rule cn_dghm_comp_is_dghm)


text‹Rules.›

lemma (in is_semifunctor) is_semifunctor_axioms'[smc_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_semifunctor_axioms)

mk_ide rf is_semifunctor_def[unfolded is_semifunctor_axioms_def]
  |intro is_semifunctorI|
  |dest is_semifunctorD[dest]|
  |elim is_semifunctorE[elim]|

lemmas [smc_cs_intros] =
  is_semifunctorD(3,4)

lemma is_semifunctorI':
  assumes "𝒵 α" 
    and "vfsequence 𝔉" 
    and "semicategory α 𝔄"
    and "semicategory α 𝔅" 
    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⦈"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  by (intro is_semifunctorI is_dghmI, unfold smcf_dghm_components slicing_simps)
    (simp_all add: assms smcf_dghm_def nat_omega_simps semicategory.smc_digraph)

lemma is_semifunctorD':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒵 α" 
    and "vfsequence 𝔉" 
    and "semicategory α 𝔄"
    and "semicategory α 𝔅" 
    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⦈"
  by
    (
      simp_all add: 
        is_semifunctorD(2-9)[OF assms] 
        is_dghmD[OF is_semifunctorD(6)[OF assms], unfolded slicing_simps]
    )

lemma is_semifunctorE':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  obtains "𝒵 α" 
    and "vfsequence 𝔉" 
    and "semicategory α 𝔄"
    and "semicategory α 𝔅" 
    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⦈"
  using assms by (simp add: is_semifunctorD')


text‹Slicing.›

context is_semifunctor
begin

interpretation dghm: is_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
  by (rule smcf_is_dghm)

sublocale ObjMap: vsv ‹𝔉⦇ObjMap⦈›
  by (rule dghm.ObjMap.vsv_axioms[unfolded slicing_simps])
sublocale ArrMap: vsv ‹𝔉⦇ArrMap⦈›
  by (rule dghm.ArrMap.vsv_axioms[unfolded slicing_simps])

lemmas_with [unfolded slicing_simps]:
  smcf_ObjMap_vsv = dghm.dghm_ObjMap_vsv
  and smcf_ArrMap_vsv = dghm.dghm_ArrMap_vsv
  and smcf_ObjMap_vdomain[smc_cs_simps] = dghm.dghm_ObjMap_vdomain
  and smcf_ObjMap_vrange = dghm.dghm_ObjMap_vrange
  and smcf_ArrMap_vdomain[smc_cs_simps] = dghm.dghm_ArrMap_vdomain
  and smcf_ArrMap_is_arr = dghm.dghm_ArrMap_is_arr
  and smcf_ArrMap_is_arr''[smc_cs_intros] = dghm.dghm_ArrMap_is_arr''
  and smcf_ArrMap_is_arr'[smc_cs_intros] = dghm.dghm_ArrMap_is_arr'
  and smcf_ObjMap_app_in_HomCod_Obj[smc_cs_intros] = 
    dghm.dghm_ObjMap_app_in_HomCod_Obj
  and smcf_ArrMap_vrange = dghm.dghm_ArrMap_vrange
  and smcf_ArrMap_app_in_HomCod_Arr[smc_cs_intros] = 
    dghm.dghm_ArrMap_app_in_HomCod_Arr
  and smcf_ObjMap_vsubset_Vset = dghm.dghm_ObjMap_vsubset_Vset
  and smcf_ArrMap_vsubset_Vset = dghm.dghm_ArrMap_vsubset_Vset
  and smcf_ObjMap_in_Vset = dghm.dghm_ObjMap_in_Vset
  and smcf_ArrMap_in_Vset = dghm.dghm_ArrMap_in_Vset
  and smcf_is_dghm_if_ge_Limit = dghm.dghm_is_dghm_if_ge_Limit
  and smcf_is_arr_HomCod = dghm.dghm_is_arr_HomCod
  and smcf_vimage_dghm_ArrMap_vsubset_Hom = 
    dghm.dghm_vimage_dghm_ArrMap_vsubset_Hom

end

lemmas [smc_cs_simps] =
  is_semifunctor.smcf_ObjMap_vdomain
  is_semifunctor.smcf_ArrMap_vdomain

lemmas [smc_cs_intros] =
  is_semifunctor.smcf_ObjMap_app_in_HomCod_Obj
  is_semifunctor.smcf_ArrMap_app_in_HomCod_Arr
  is_semifunctor.smcf_ArrMap_is_arr'


text‹Elementary properties.›

lemma cn_smcf_ArrMap_Comp[smc_cs_simps]:
  assumes "semicategory α 𝔄"
    and "𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "g : c ↦⇘𝔄⇙ b"
    and "f : b ↦⇘𝔄⇙ a"
  shows "𝔉⦇ArrMap⦈⦇f ∘⇩A⇘𝔄⇙ g⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
proof-
  from assms(3,4) have gf:
    "𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘op_smc 𝔄⇙ f⦈"
    by
      (
        force
          intro: is_semifunctor.smcf_ArrMap_Comp[OF assms(2), symmetric]
          simp: slicing_simps smc_op_simps
      )
  from assms show ?thesis
    unfolding gf by (cs_concl cs_shallow cs_simp: smc_op_simps) 
qed

lemma smcf_eqI:
  assumes "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" 
    and "𝔉 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    and "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    and "𝔄 = ℭ"
    and "𝔅 = 𝔇"
  shows "𝔊 = 𝔉"
proof-
  interpret L: is_semifunctor α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret R: is_semifunctor α ℭ 𝔇 𝔉 by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟⇩∘ 𝔊 = 4⇩ℕ" 
      by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
    show "𝒟⇩∘ 𝔊 = 𝒟⇩∘ 𝔉" 
      by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
    from assms(5,6) have sup: "𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈" 
      by (simp_all add: smc_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 auto
qed

lemma smcf_dghm_eqI:
  assumes "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔉 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
    and "𝔄 = ℭ"
    and "𝔅 = 𝔇"
    and "smcf_dghm 𝔊 = smcf_dghm 𝔉"
  shows "𝔊 = 𝔉"
proof(rule smcf_eqI)
  from assms(5) have 
    "smcf_dghm 𝔊⦇ObjMap⦈ = smcf_dghm 𝔉⦇ObjMap⦈"
    "smcf_dghm 𝔊⦇ArrMap⦈ = smcf_dghm 𝔉⦇ArrMap⦈"
    by simp_all
  then show "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    unfolding slicing_simps by simp_all
qed (auto intro: assms(1,2) simp: assms)

lemma (in is_semifunctor) smcf_def: 
  "𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ 𝔉 = 4⇩ℕ" 
    by (cs_concl cs_shallow cs_simp: smc_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)

lemma (in is_semifunctor) smcf_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔉 ∈⇩∘ Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [smc_cs_intros] = 
    smcf_ObjMap_in_Vset 
    smcf_ArrMap_in_Vset 
    HomDom.smc_in_Vset 
    HomCod.smc_in_Vset
  from assms(2) show ?thesis
    by (subst smcf_def) 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps cs_intro: smc_cs_intros V_cs_intros
      )
qed

lemma (in is_semifunctor) smcf_is_semifunctor_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘β⇙ 𝔅"
  by (rule is_semifunctorI)
    (
      simp_all add: 
        assms 
        vfsequence_axioms
        smcf_is_dghm_if_ge_Limit
        HomDom.smc_semicategory_if_ge_Limit
        HomCod.smc_semicategory_if_ge_Limit
        smc_cs_simps
    )

lemma small_all_smcfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
  case True
  from is_semifunctor.smcf_in_Vset show ?thesis
    by (intro down[of _ ‹Vset (α + ω)›]) 
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅} = {}" by auto
  then show ?thesis by simp
qed

lemma (in is_semifunctor) smcf_in_Vset_7: "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], smc_cs_intros] =
    smcf_ObjMap_vsubset_Vset 
    smcf_ArrMap_vsubset_Vset
  from HomDom.smc_semicategory_in_Vset_4 have [smc_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.smc_semicategory_in_Vset_4 have [smc_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 smcf_def, succ_of_numeral)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps smc_cs_simps 
          cs_intro: smc_cs_intros V_cs_intros
      )
qed

lemma (in 𝒵) all_smcfs_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "all_smcfs α ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "all_smcfs α ⊆⇩∘ Vset (α + 7⇩ℕ)"
  proof(intro vsubsetI)
    fix 𝔉 assume "𝔉 ∈⇩∘ all_smcfs α"
    then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" by clarsimp
    then interpret is_semifunctor α 𝔄 𝔅 𝔉 .
    show "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)" by (rule smcf_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_smcfs[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"
  by (rule down[of _ ‹set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}›]) auto



subsection‹Opposite semifunctor›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition op_smcf :: "V ⇒ V"
  where "op_smcf 𝔉 =
    [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, op_smc (𝔉⦇HomDom⦈), op_smc (𝔉⦇HomCod⦈)]⇩∘"


text‹Components.›

lemma op_smcf_components[smc_op_simps]:
  shows "op_smcf 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
    and "op_smcf 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
    and "op_smcf 𝔉⦇HomDom⦈ = op_smc (𝔉⦇HomDom⦈)"
    and "op_smcf 𝔉⦇HomCod⦈ = op_smc (𝔉⦇HomCod⦈)"
  unfolding op_smcf_def dghm_field_simps by (auto simp: nat_omega_simps)


text‹Slicing.›

lemma op_dghm_smcf_dghm[slicing_commute]: 
  "op_dghm (smcf_dghm 𝔉) = smcf_dghm (op_smcf 𝔉)"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ (op_dghm (smcf_dghm 𝔉)) = 4⇩ℕ"
    unfolding op_dghm_def by (auto simp: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smcf_dghm (op_smcf 𝔉)) = 4⇩ℕ"
    unfolding smcf_dghm_def by (auto simp: nat_omega_simps)
  show "𝒟⇩∘ (op_dghm (smcf_dghm 𝔉)) = 𝒟⇩∘ (smcf_dghm (op_smcf 𝔉))"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ (op_dghm (smcf_dghm 𝔉)) ⟹
    op_dghm (smcf_dghm 𝔉)⦇a⦈ = smcf_dghm (op_smcf 𝔉)⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold smcf_dghm_def op_smcf_def op_dghm_def dghm_field_simps
      ) 
      (auto simp: nat_omega_simps slicing_simps slicing_commute)
qed (auto simp: smcf_dghm_def op_dghm_def)


subsubsection‹Further properties›

lemma (in is_semifunctor) is_semifunctor_op:
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc 𝔅"
proof(intro is_semifunctorI)
  show "vfsequence (op_smcf 𝔉)" unfolding op_smcf_def by simp
  show "vcard (op_smcf 𝔉) = 4⇩ℕ" 
    unfolding op_smcf_def by (auto simp: nat_omega_simps)
  fix g b c f a assume "g : b ↦⇘op_smc 𝔄⇙ c" "f : a ↦⇘op_smc 𝔄⇙ b"
  then have "g : c ↦⇘𝔄⇙ b" and "f : b ↦⇘𝔄⇙ a"  
    unfolding smc_op_simps by simp_all
  with is_semifunctor_axioms show 
    "op_smcf 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘op_smc 𝔄⇙ f⦈ =
      op_smcf 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘op_smc 𝔅⇙ op_smcf 𝔉⦇ArrMap⦈⦇f⦈"
    by 
      (
        cs_concl 
          cs_simp: smc_op_simps smc_cs_simps 
          cs_intro: smc_op_intros smc_cs_intros
      )
qed 
  (
    auto simp: 
      smc_cs_simps
      smc_op_simps
      slicing_simps
      slicing_commute[symmetric]
      is_dghm.is_dghm_op 
      smcf_is_dghm
      HomCod.semicategory_op 
      HomDom.semicategory_op
  )

lemma (in is_semifunctor) is_semifunctor_op':  
  assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅" and "α' = α"
  shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_semifunctor_op)

lemmas is_semifunctor_op'[smc_op_intros] = is_semifunctor.is_semifunctor_op'

lemma (in is_semifunctor) smcf_op_smcf_op_smcf[smc_op_simps]: 
  "op_smcf (op_smcf 𝔉) = 𝔉" 
proof(rule smcf_eqI, unfold smc_op_simps)
  show "op_smcf (op_smcf 𝔉) : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    by 
      (
        metis 
          HomCod.smc_op_smc_op_smc 
          HomDom.smc_op_smc_op_smc 
          is_semifunctor.is_semifunctor_op 
          is_semifunctor_op
      )
qed (simp_all add: is_semifunctor_axioms)

lemmas smcf_op_smcf_op_smcf[smc_op_simps] = is_semifunctor.smcf_op_smcf_op_smcf

lemma eq_op_smcf_iff[smc_op_simps]: 
  assumes "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and "𝔉 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
  shows "op_smcf 𝔊 = op_smcf 𝔉 ⟷ 𝔊 = 𝔉"
proof
  interpret L: is_semifunctor α 𝔄 𝔅 𝔊 by (rule assms(1))
  interpret R: is_semifunctor α ℭ 𝔇 𝔉 by (rule assms(2))
  assume prems: "op_smcf 𝔊 = op_smcf 𝔉"
  show "𝔊 = 𝔉"
  proof(rule smcf_eqI[OF assms])
    from prems R.smcf_op_smcf_op_smcf L.smcf_op_smcf_op_smcf show 
      "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
      by metis+
    from prems R.smcf_op_smcf_op_smcf L.smcf_op_smcf_op_smcf have 
      "𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
      by auto
    then show "𝔄 = ℭ" "𝔅 = 𝔇" by (simp_all add: smc_cs_simps)
  qed
qed auto



subsection‹Composition of covariant semifunctors›


subsubsection‹Definition and elementary properties›

abbreviation (input) smcf_comp :: "V ⇒ V ⇒ V" (infixl ‹∘⇩S⇩M⇩C⇩F› 55)
  where "smcf_comp ≡ dghm_comp"


text‹Slicing.›

lemma smcf_dghm_smcf_comp[slicing_commute]: 
  "smcf_dghm 𝔊 ∘⇩D⇩G⇩H⇩M smcf_dghm 𝔉 = smcf_dghm (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)"
  unfolding dghm_comp_def smcf_dghm_def dghm_field_simps 
  by (simp add: nat_omega_simps)


subsubsection‹Object map›

lemma smcf_comp_ObjMap_vsv[smc_cs_intros]: 
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "vsv ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈)"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ObjMap_vsv
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma smcf_comp_ObjMap_vdomain[smc_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ObjMap_vdomain
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma smcf_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ObjMap_vrange
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma smcf_comp_ObjMap_app[smc_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and [simp]: "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ObjMap_app
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute, 
            OF assms(3)
          ]
      )
qed


subsubsection‹Arrow map›

lemma smcf_comp_ArrMap_vsv[smc_cs_intros]: 
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "vsv ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈)"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis 
    by 
      (
        rule dghm_comp_ArrMap_vsv
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma smcf_comp_ArrMap_vdomain[smc_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ArrMap_vdomain
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma smcf_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ArrMap_vrange
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute
          ]
      )
qed

lemma smcf_comp_ArrMap_app[smc_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and [simp]: "f ∈⇩∘ 𝔄⦇Arr⦈"
  shows "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_comp_ArrMap_app
          [
            OF L.smcf_is_dghm R.smcf_is_dghm, 
            unfolded slicing_simps slicing_commute,
            OF assms(3)
          ]
      )
qed


subsubsection‹Further properties›

lemma smcf_comp_is_semifunctor[smc_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
  proof(rule is_semifunctorI, unfold dghm_comp_components(3,4))
    show "vfsequence (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)" by (simp add: dghm_comp_def)
    show "vcard (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) = 4⇩ℕ"  
      unfolding dghm_comp_def by (simp add: nat_omega_simps)
    fix g b c f a assume "g : b ↦⇘𝔄⇙ c" "f : a ↦⇘𝔄⇙ b"
    with assms show "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 
      (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈"
      by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  qed 
    (
      auto 
        simp: slicing_commute[symmetric] smc_cs_simps smc_cs_intros 
        intro: dg_cs_intros slicing_intros
    )
qed 

lemma smcf_comp_assoc[smc_cs_simps]:
  assumes "ℌ : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇" 
    and "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "(ℌ ∘⇩S⇩M⇩C⇩F 𝔊) ∘⇩S⇩M⇩C⇩F 𝔉 = ℌ ∘⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)"
proof(rule smcf_eqI[of α 𝔄 𝔇 _ 𝔄 𝔇])
  interpret ℌ: is_semifunctor α ℭ 𝔇 ℌ by (rule assms(1)) 
  interpret 𝔊: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(2)) 
  interpret 𝔉: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(3)) 
  from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms ℌ.is_semifunctor_axioms 
  show "ℌ ∘⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇" 
    and "ℌ ∘⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"  
    by (auto intro: smc_cs_intros)
qed (simp_all add: dghm_comp_components vcomp_assoc)

lemma op_smcf_smcf_comp[smc_op_simps]: 
  "op_smcf (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) = op_smcf 𝔊 ∘⇩S⇩M⇩C⇩F op_smcf 𝔉"
  unfolding dghm_comp_def op_smcf_def dghm_field_simps 
  by (simp add: nat_omega_simps)



subsection‹Composition of contravariant semifunctors›


subsubsection‹Definition and elementary properties›


text‹See section 1.2 in \<^cite>‹"bodo_categories_1970"›.›

definition smcf_cn_comp :: "V ⇒ V ⇒ V" (infixl ‹⇩S⇩M⇩C⇩F∘› 55)
  where "𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉 =
    [
      𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈, 
      𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈, 
      op_smc (𝔉⦇HomDom⦈), 
      𝔊⦇HomCod⦈
    ]⇩∘"


text‹Components.›

lemma smcf_cn_comp_components:
  shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈ = 𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
    and "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈ = 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈"
    and [smc_cn_cs_simps]: "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇HomDom⦈ = op_smc (𝔉⦇HomDom⦈)"
    and [smc_cn_cs_simps]: "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇HomCod⦈ = 𝔊⦇HomCod⦈"
  unfolding smcf_cn_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smcf_dghm_smcf_cn_comp[slicing_commute]: 
  "smcf_dghm 𝔊 ⇩D⇩G⇩H⇩M∘ smcf_dghm 𝔉 = smcf_dghm (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)"
  unfolding dghm_cn_comp_def smcf_cn_comp_def smcf_dghm_def  
  by (simp add: nat_omega_simps slicing_commute dghm_field_simps)


subsubsection‹Object map: two contravariant semifunctors›

lemma smcf_cn_comp_ObjMap_vsv[smc_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈)"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ObjMap_vsv
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_comp_ObjMap_vdomain[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_comp_ObjMap_vdomain
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_comp_ObjMap_vrange
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_comp_ObjMap_app[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_comp_ObjMap_app
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps, 
            OF assms(3)
          ]
      )
qed


subsubsection‹Arrow map: two contravariant semifunctors›

lemma smcf_cn_comp_ArrMap_vsv[smc_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈)"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ArrMap_vsv
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_comp_ArrMap_vdomain[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_comp_ArrMap_vdomain
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_comp_ArrMap_vrange
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_comp_ArrMap_app[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Arr⦈"
  shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_comp_ArrMap_app
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsection‹Object map: contravariant and covariant semifunctors›

lemma smcf_cn_cov_comp_ObjMap_vsv[smc_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈)"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ObjMap_vsv
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_cov_comp_ObjMap_vdomain[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ObjMap_vdomain
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_cov_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ObjMap_vrange
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_cov_comp_ObjMap_app[smc_cn_cs_simps]:
    assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
  shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ObjMap_app
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm,
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsection‹Arrow map: contravariant and covariant semifunctors›

lemma smcf_cn_cov_comp_ArrMap_vsv[smc_cn_cs_intros]: 
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈)"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ArrMap_vsv
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
              R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_cov_comp_ArrMap_vdomain[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ArrMap_vdomain
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_cov_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ArrMap_vrange
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma smcf_cn_cov_comp_ArrMap_app[smc_cn_cs_simps]:
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and "f ∈⇩∘ 𝔄⦇Arr⦈"
  shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1)) 
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule dghm_cn_cov_comp_ArrMap_app
          [
            OF 
              L.smcf_is_dghm[unfolded slicing_commute[symmetric]] 
              R.smcf_is_dghm,
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsection‹Opposite of the contravariant composition of semifunctors›

lemma op_smcf_smcf_cn_comp[smc_op_simps]: 
  "op_smcf (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) = op_smcf 𝔊 ⇩S⇩M⇩C⇩F∘ op_smcf 𝔉"
  unfolding op_smcf_def smcf_cn_comp_def dghm_field_simps
  by (auto simp: nat_omega_simps)


subsubsection‹Further properties›

lemma smcf_cn_comp_is_semifunctor[smc_cn_cs_intros]:
  ―‹See section 1.2 in \cite{bodo_categories_1970}.›
  assumes "semicategory α 𝔄" and "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 
    rewrites "f : b ↦⇘op_smc ℭ'⇙ a = f : a ↦⇘ℭ'⇙ b" for ℭ' f b a 
    by (rule assms(2)) (simp_all add: smc_op_simps)
  interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 
    rewrites "f : b ↦⇘op_smc ℭ'⇙ a = f : a ↦⇘ℭ'⇙ b" for ℭ' f b a
    by (rule assms(3)) (simp_all add: smc_op_simps)
  interpret 𝔄: semicategory α 𝔄 by (rule assms(1))
  show ?thesis
  proof(rule is_semifunctorI, unfold smcf_cn_comp_components(3,4) smc_op_simps)
    from assms show "smcf_dghm (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
      by 
        (
          cs_concl cs_shallow
            cs_simp: slicing_commute[symmetric] 
            cs_intro: dg_cn_cs_intros slicing_intros
        )
    fix g b c f a assume "g : b ↦⇘𝔄⇙ c" "f : a ↦⇘𝔄⇙ b"
    with assms show "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 
      (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f⦈"
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_cn_cs_simps smc_op_simps 
            cs_intro: smc_cs_intros
        )
  qed 
    (
      auto simp: 
        smcf_cn_comp_def 
        nat_omega_simps 
        smc_cs_simps
        smc_op_simps 
        smc_cs_intros
    )
qed

lemma smcf_cn_cov_comp_is_semifunctor[smc_cs_intros]:
  ―‹See section 1.2 in \cite{bodo_categories_1970}.›
  assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  shows "𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ"
proof-
  interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 
    rewrites "f : b ↦⇘op_smc ℭ'⇙ a = f : a ↦⇘ℭ'⇙ b" for ℭ' f b a 
    by (rule assms(1)) (simp_all add: smc_op_simps)
  interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
  proof(rule is_semifunctorI, unfold smcf_cn_comp_components(3,4) smc_op_simps)
    from assms show 
      "smcf_dghm (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) : smc_dg (op_smc 𝔄) ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: slicing_commute[symmetric]
            cs_intro: dg_cn_cs_intros slicing_intros
        )
    show "vfsequence (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)" unfolding smcf_cn_comp_def by simp
    show "vcard (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) = 4⇩ℕ"
      unfolding smcf_cn_comp_def by (auto simp: nat_omega_simps)
    show "op_smc (𝔉⦇HomDom⦈) = op_smc 𝔄" by (simp add: smc_cs_simps)
    show "𝔊⦇HomCod⦈ = ℭ" by (simp add: smc_cs_simps)
    fix g b c f a assume "g : c ↦⇘𝔄⇙ b" "f : b ↦⇘𝔄⇙ a"
    with assms show 
      "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f ∘⇩A⇘𝔄⇙ g⦈ = 
        (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f⦈"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: smc_cs_simps smc_cn_cs_simps smc_op_simps 
            cs_intro: smc_cs_intros
        )
  qed (auto intro: smc_cs_intros smc_op_intros)
qed

lemma smcf_cov_cn_comp_is_semifunctor[smc_cn_cs_intros]:
  ―‹See section 1.2 in \cite{bodo_categories_1970}.›
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ"
  using assms by (rule smcf_comp_is_semifunctor)



subsection‹Identity semifunctor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›

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


text‹Slicing.›

lemma smcf_dghm_smcf_id[slicing_commute]: 
  "dghm_id (smc_dg ℭ) = smcf_dghm (smcf_id ℭ)"
  unfolding dghm_id_def smc_dg_def smcf_dghm_def dghm_field_simps dg_field_simps
  by (simp add: nat_omega_simps)

context semicategory
begin

interpretation dg: digraph α ‹smc_dg ℭ› by (rule smc_digraph)

lemmas_with [unfolded slicing_simps]:
  smc_dghm_id_is_dghm = dg.dg_dghm_id_is_dghm

end


subsubsection‹Object map›

lemmas [smc_cs_simps] = dghm_id_ObjMap_app


subsubsection‹Arrow map›

lemmas [smc_cs_simps] = dghm_id_ArrMap_app


subsubsection‹Opposite identity semifunctor›

lemma op_smcf_smcf_id[smc_op_simps]: "op_smcf (smcf_id ℭ) = smcf_id (op_smc ℭ)"
  unfolding dghm_id_def op_smc_def op_smcf_def dghm_field_simps dg_field_simps
  by (auto simp: nat_omega_simps)


subsubsection‹An identity semifunctor is a semifunctor›

lemma (in semicategory) smc_smcf_id_is_semifunctor: "smcf_id ℭ : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof(rule is_semifunctorI, unfold dghm_id_components)
  from smc_dghm_id_is_dghm show 
    "smcf_dghm (smcf_id ℭ) : smc_dg ℭ ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
    by (auto simp: slicing_simps slicing_commute)
  fix g b c f a assume "g : b ↦⇘ℭ⇙ c" "f : a ↦⇘ℭ⇙ b"
  then show "vid_on (ℭ⦇Arr⦈)⦇g ∘⇩A⇘ℭ⇙ f⦈ = 
    vid_on (ℭ⦇Arr⦈)⦇g⦈ ∘⇩A⇘ℭ⇙ vid_on (ℭ⦇Arr⦈)⦇f⦈"
    by (metis smc_is_arrD(1) smc_Comp_is_arr vid_on_eq_atI)
qed (auto simp: semicategory_axioms dghm_id_def nat_omega_simps)

lemma (in semicategory) smc_smcf_id_is_semifunctor': 
  assumes "𝔄 = ℭ" and "𝔅 = ℭ"
  shows "smcf_id ℭ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  unfolding assms by (rule smc_smcf_id_is_semifunctor)

lemmas [smc_cs_intros] = semicategory.smc_smcf_id_is_semifunctor'


subsubsection‹Further properties›

lemma (in is_semifunctor) smcf_smcf_comp_smcf_id_left[smc_cs_simps]:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}).›
  "smcf_id 𝔅 ∘⇩S⇩M⇩C⇩F 𝔉 = 𝔉"
  by (rule smcf_eqI, unfold dghm_id_components dghm_comp_components)
    (auto simp: smcf_ObjMap_vrange smcf_ArrMap_vrange intro: smc_cs_intros)

lemmas [smc_cs_simps] = is_semifunctor.smcf_smcf_comp_smcf_id_left

lemma (in is_semifunctor) smcf_smcf_comp_smcf_id_right[smc_cs_simps]: 
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}).›
  "𝔉 ∘⇩S⇩M⇩C⇩F smcf_id 𝔄 = 𝔉"
  by (rule smcf_eqI, unfold dghm_id_components dghm_comp_components)
    (
      auto 
        simp: smcf_ObjMap_vrange smcf_ArrMap_vrange smc_cs_simps
        intro: smc_cs_intros
    )

lemmas [smc_cs_simps] = is_semifunctor.smcf_smcf_comp_smcf_id_right



subsection‹Constant semifunctor›


subsubsection‹Definition and elementary properties›


text‹See Chapter III-3 in \<^cite>‹"mac_lane_categories_2010"›.›

abbreviation (input) smcf_const :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "smcf_const ≡ dghm_const"


text‹Slicing.›

lemma smcf_dghm_smcf_const[slicing_commute]: 
  "dghm_const (smc_dg ℭ) (smc_dg 𝔇) a f = smcf_dghm (smcf_const ℭ 𝔇 a f)"
  unfolding 
    dghm_const_def smc_dg_def smcf_dghm_def dghm_field_simps dg_field_simps
  by (simp add: nat_omega_simps)


subsubsection‹Object map›

lemmas [smc_cs_simps] = 
  dghm_const_ObjMap_app 


subsubsection‹Arrow map›

lemmas [smc_cs_simps] = 
  dghm_const_ArrMap_app


subsubsection‹Opposite constant semifunctor›

lemma op_smcf_smcf_const[smc_op_simps]:
  "op_smcf (smcf_const ℭ 𝔇 a f) = smcf_const (op_smc ℭ) (op_smc 𝔇) a f"
  unfolding dghm_const_def op_smc_def op_smcf_def dghm_field_simps dg_field_simps
  by (auto simp: nat_omega_simps)


subsubsection‹A constant semifunctor is a semifunctor›

lemma smcf_const_is_semifunctor: 
  assumes "semicategory α ℭ"
    and "semicategory α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a" 
    and [simp]: "f ∘⇩A⇘𝔇⇙ f = f"
  shows "smcf_const ℭ 𝔇 a f : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
proof-
  interpret ℭ: semicategory α ℭ by (rule assms(1))
  interpret 𝔇: semicategory α 𝔇 by (rule assms(2))
  show ?thesis
  proof(intro is_semifunctorI, tactic‹distinct_subgoals_tac›)
    from assms show 
      "smcf_dghm (dghm_const ℭ 𝔇 a f) : smc_dg ℭ ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔇"
      by 
        ( 
          cs_concl cs_shallow 
            cs_simp: slicing_commute[symmetric] 
            cs_intro: dg_cs_intros slicing_intros
        )
    show "vfsequence (smcf_const ℭ 𝔇 a f)" unfolding dghm_const_def by simp
    show "vcard (smcf_const ℭ 𝔇 a f) = 4⇩ℕ"
      unfolding dghm_const_def by (simp add: nat_omega_simps)
    fix g' b c f' a' assume "g' : b ↦⇘ℭ⇙ c" "f' : a' ↦⇘ℭ⇙ b"
    with assms(1-3) show "smcf_const ℭ 𝔇 a f⦇ArrMap⦈⦇g' ∘⇩A⇘ℭ⇙ f'⦈ =
      smcf_const ℭ 𝔇 a f⦇ArrMap⦈⦇g'⦈ ∘⇩A⇘𝔇⇙ smcf_const ℭ 𝔇 a f⦇ArrMap⦈⦇f'⦈"
      by (cs_concl cs_simp: assms(4) smc_cs_simps cs_intro: smc_cs_intros)
  qed (auto simp: assms(1,2) dghm_const_components)
qed 

lemma smcf_const_is_semifunctor'[smc_cs_intros]: 
  assumes "semicategory α ℭ" 
    and "semicategory α 𝔇" 
    and "f : a ↦⇘𝔇⇙ a"
    and "f ∘⇩A⇘𝔇⇙ f = f"
    and "𝔄 = ℭ"
    and "𝔅 = 𝔇"
  shows "smcf_const ℭ 𝔇 a f : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
  using assms(1-4) unfolding assms(5,6) by (rule smcf_const_is_semifunctor)


subsubsection‹Further properties›

lemma (in is_semifunctor) smcf_smcf_comp_smcf_const[smc_cs_simps]:
  assumes "semicategory α ℭ" and "f : a ↦⇘ℭ⇙ a" and "f ∘⇩A⇘ℭ⇙ f = f"
  shows "smcf_const 𝔅 ℭ a f ∘⇩S⇩M⇩C⇩F 𝔉 = smcf_const 𝔄 ℭ a f"
proof(rule smcf_dghm_eqI)
  interpret ℭ: semicategory α ℭ by (rule assms(1))
  from assms(2) show "smcf_const 𝔅 ℭ a f ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps assms(3) cs_intro: smc_cs_intros
      )
  from assms(2) show "smcf_const 𝔄 ℭ a f : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps assms(3) cs_intro: smc_cs_intros
      )
  from is_dghm.dghm_dghm_comp_dghm_const[
    OF smcf_is_dghm ℭ.smc_digraph, unfolded slicing_simps, OF assms(2)
    ]
  show "smcf_dghm (smcf_const 𝔅 ℭ a f ∘⇩S⇩M⇩C⇩F 𝔉) = smcf_dghm (smcf_const 𝔄 ℭ a f)"
    by (cs_prems cs_shallow cs_simp: slicing_simps slicing_commute)
qed simp_all

lemmas [smc_cs_simps] = is_semifunctor.smcf_smcf_comp_smcf_const



subsection‹Faithful semifunctor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›

locale is_ft_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes ft_smcf_is_ft_dghm: 
    "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ smc_dg 𝔅"

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

lemma (in is_ft_semifunctor) ft_smcf_is_ft_dghm'[slicing_intros]:
  assumes "𝔄' = smc_dg 𝔄" and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
  unfolding assms by (rule ft_smcf_is_ft_dghm)

lemmas [slicing_intros] = is_ft_semifunctor.ft_smcf_is_ft_dghm'


text‹Rules.›

lemma (in is_ft_semifunctor) is_ft_semifunctor_axioms'[smcf_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_ft_semifunctor_axioms)

mk_ide rf is_ft_semifunctor_def[unfolded is_ft_semifunctor_axioms_def]
  |intro is_ft_semifunctorI|
  |dest is_ft_semifunctorD[dest]|
  |elim is_ft_semifunctorE[elim]|

lemmas [smcf_cs_intros] = is_ft_semifunctorD(1)

lemma is_ft_semifunctorI':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  using assms
  by (intro is_ft_semifunctorI)
    (
      simp_all add: 
        assms(1) 
        is_ft_dghmI[OF is_semifunctorD(6)[OF assms(1)], unfolded slicing_simps]
    )

lemma is_ft_semifunctorD':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
  by 
    (
      simp_all add: 
        is_ft_semifunctorD[OF assms(1)] 
        is_ft_dghmD(2)[
          OF is_ft_semifunctorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_ft_semifunctorE':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
  using assms by (simp_all add: is_ft_semifunctorD')

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


text‹Elementary properties.›

context is_ft_semifunctor
begin

interpretation dghm: is_ft_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
  by (rule ft_smcf_is_ft_dghm) 

lemmas_with [unfolded slicing_simps]:
  ft_smcf_v11_on_Hom = dghm.ft_dghm_v11_on_Hom
  and ft_smcf_ArrMap_eqD = dghm.ft_dghm_ArrMap_eqD

end


subsubsection‹Opposite faithful semifunctor›

lemma (in is_ft_semifunctor) is_ft_semifunctor_op: 
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_smc 𝔅"   
  by 
    (
      rule is_ft_semifunctorI, 
      unfold smc_op_simps slicing_simps slicing_commute[symmetric]
    )
    (
      simp_all add: 
        is_semifunctor_op is_ft_dghm.ft_dghm_op_dghm_is_ft_dghm 
        ft_smcf_is_ft_dghm
    )

lemma (in is_ft_semifunctor) is_ft_semifunctor_op'[smc_op_intros]: 
  assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅"
  shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
  unfolding assms by (rule is_ft_semifunctor_op)

lemmas is_ft_semifunctor_op[smc_op_intros] = 
  is_ft_semifunctor.is_ft_semifunctor_op'


subsubsection‹
The composition of faithful semifunctors is a faithful semifunctor
›

lemma smcf_comp_is_ft_semifunctor[smcf_cs_intros]:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}.›
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ"
proof(intro is_ft_semifunctorI)
  interpret 𝔊: is_ft_semifunctor α 𝔅 ℭ 𝔊 by (simp add: assms(1))
  interpret 𝔉: is_ft_semifunctor α 𝔄 𝔅 𝔉 by (simp add: assms(2))
  from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms show 𝔊𝔉: 
    "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
    by (auto intro: smc_cs_intros)
  then interpret is_semifunctor α 𝔄 ℭ ‹𝔊 ∘⇩S⇩M⇩C⇩F 𝔉› .
  show "smcf_dghm (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ smc_dg ℭ"
    unfolding slicing_simps slicing_commute[symmetric] 
    by (auto intro: dghm_cs_intros slicing_intros)
qed



subsection‹Full semifunctor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›

locale is_fl_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes fl_smcf_is_fl_dghm:
    "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ smc_dg 𝔅"

syntax "_is_fl_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩lı _)› [51, 51, 51] 51)
syntax_consts "_is_fl_semifunctor" ⇌ is_fl_semifunctor
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" ⇌ "CONST is_fl_semifunctor α 𝔄 𝔅 𝔉"

lemma (in is_fl_semifunctor) fl_smcf_is_fl_dghm'[slicing_intros]:
  assumes "𝔄' = smc_dg 𝔄" and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅'"
  unfolding assms by (rule fl_smcf_is_fl_dghm)

lemmas [slicing_intros] = is_fl_semifunctor.fl_smcf_is_fl_dghm'


text‹Rules.›

mk_ide rf is_fl_semifunctor_def[unfolded is_fl_semifunctor_axioms_def]
  |intro is_fl_semifunctorI|
  |dest is_fl_semifunctorD[dest]|
  |elim is_fl_semifunctorE[elim]|

lemmas [smcf_cs_intros] = is_fl_semifunctorD(1)

lemma is_fl_semifunctorI':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
      𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
  using assms
  by (intro is_fl_semifunctorI)
    (
      simp_all add: 
        assms(1) 
        is_fl_dghmI[OF is_semifunctorD(6)[OF assms(1)], unfolded slicing_simps]
    )

lemma is_fl_semifunctorD':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ 
      𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
  by 
    (
      simp_all add: 
        is_fl_semifunctorD[OF assms(1)] 
        is_fl_dghmD(2)[
          OF is_fl_semifunctorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_fl_semifunctorE':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩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_semifunctorD')


text‹Elementary properties.›

context is_fl_semifunctor
begin

interpretation dghm: is_fl_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
  by (rule fl_smcf_is_fl_dghm) 

lemmas_with [unfolded slicing_simps]:
  fl_smcf_surj_on_Hom = dghm.fl_dghm_surj_on_Hom

end


subsubsection‹Opposite full semifunctor›

lemma (in is_fl_semifunctor) is_fl_semifunctor_op: 
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ op_smc 𝔅"    
  by 
    (
      rule is_fl_semifunctorI, 
      unfold smc_op_simps slicing_simps slicing_commute[symmetric]
    )
    (
      simp_all add: 
        is_semifunctor_op 
        is_fl_dghm.fl_dghm_op_dghm_is_fl_dghm 
        fl_smcf_is_fl_dghm
    )

lemma (in is_fl_semifunctor) is_fl_semifunctor_op'[smc_op_intros]: 
  assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅"
  shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅'"
  unfolding assms by (rule is_fl_semifunctor_op)

lemmas is_fl_semifunctor_op[smc_op_intros] = 
  is_fl_semifunctor.is_fl_semifunctor_op


subsubsection‹The composition of full semifunctors is a full semifunctor›

lemma smcf_comp_is_fl_semifunctor[smcf_cs_intros]:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}.›
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" 
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ"
proof(intro is_fl_semifunctorI)
  interpret 𝔉: is_fl_semifunctor α 𝔄 𝔅 𝔉 using assms(2) by simp
  interpret 𝔊: is_fl_semifunctor α 𝔅 ℭ 𝔊 using assms(1) by simp
  from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms show
    "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    by (auto intro: smc_cs_intros)
  show "smcf_dghm (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ smc_dg ℭ"
    unfolding slicing_commute[symmetric] 
    by (auto intro: dghm_cs_intros slicing_intros)
qed 



subsection‹Fully faithful semifunctor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›

locale is_ff_semifunctor = 
  is_ft_semifunctor α 𝔄 𝔅 𝔉 + is_fl_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉

syntax "_is_ff_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ :/ _ ↦↦⇩S⇩M⇩C⇩.⇩f⇩fı _)› [51, 51, 51] 51)
syntax_consts "_is_ff_semifunctor" ⇌ is_ff_semifunctor
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅" ⇌ "CONST is_ff_semifunctor α 𝔄 𝔅 𝔉"


text‹Rules.›

mk_ide rf is_ff_semifunctor_def
  |intro is_ff_semifunctorI|
  |dest is_ff_semifunctorD[dest]|
  |elim is_ff_semifunctorE[elim]|

lemmas [smcf_cs_intros] = is_ff_semifunctorD


text‹Elementary properties.›

lemma (in is_ff_semifunctor) ff_smcf_is_ff_dghm:
  "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ smc_dg 𝔅"
  by (rule is_ff_dghmI) (auto intro: slicing_intros)

lemma (in is_ff_semifunctor) ff_smcf_is_ff_dghm'[slicing_intros]:
  assumes "𝔄' = smc_dg 𝔄" and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ 𝔅'"
  unfolding assms by (rule ff_smcf_is_ff_dghm)

lemmas [slicing_intros] = is_ff_semifunctor.ff_smcf_is_ff_dghm'


subsubsection‹Opposite fully faithful semifunctor›

lemma (in is_ff_semifunctor) is_ff_semifunctor_op: 
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ op_smc 𝔅"    
  by (rule is_ff_semifunctorI) 
    (auto simp: is_fl_semifunctor_op is_ft_semifunctor_op)

lemma (in is_ff_semifunctor) is_ff_semifunctor_op'[smc_op_intros]: 
  assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅"
  shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅'"
  unfolding assms by (rule is_ff_semifunctor_op)

lemmas is_ff_semifunctor_op[smc_op_intros] = 
  is_ff_semifunctor.is_ff_semifunctor_op'


subsubsection‹
The composition of fully faithful semifunctors is a fully faithful
semifunctor
›

lemma smcf_comp_is_ff_semifunctor[smcf_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ ℭ"
  using assms 
  by (intro is_ff_semifunctorI, elim is_ff_semifunctorE) 
    (auto intro: smcf_cs_intros)



subsection‹Isomorphism of semicategories›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›

locale is_iso_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 + 
  assumes iso_smcf_is_iso_dghm: 
    "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ smc_dg 𝔅"

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

lemma (in is_iso_semifunctor) iso_smcf_is_iso_dghm'[slicing_intros]:
  assumes "𝔄' = smc_dg 𝔄" "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅'"
  unfolding assms by (rule iso_smcf_is_iso_dghm)

lemmas [slicing_intros] = is_iso_semifunctor.iso_smcf_is_iso_dghm'


text‹Rules.›

lemma (in is_iso_semifunctor) is_iso_semifunctor_axioms'[smcf_cs_intros]:
  assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
  shows "𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α'⇙ 𝔅'"
  unfolding assms by (rule is_iso_semifunctor_axioms)

mk_ide rf is_iso_semifunctor_def[unfolded is_iso_semifunctor_axioms_def]
  |intro is_iso_semifunctorI|
  |dest is_iso_semifunctorD[dest]|
  |elim is_iso_semifunctorE[elim]|

lemma is_iso_semifunctorI':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "v11 (𝔉⦇ObjMap⦈)"
    and "v11 (𝔉⦇ArrMap⦈)"
    and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
    and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  using assms
  by (intro is_iso_semifunctorI)
    (
      simp_all add: 
        assms(1) 
        is_iso_dghmI[OF is_semifunctorD(6)[OF assms(1)], unfolded slicing_simps]
    )

lemma is_iso_semifunctorD':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "v11 (𝔉⦇ObjMap⦈)"
    and "v11 (𝔉⦇ArrMap⦈)"
    and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
    and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
  by 
    (
      simp_all add: 
        is_iso_semifunctorD[OF assms(1)] 
        is_iso_dghmD(2-5)[
          OF is_iso_semifunctorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_iso_semifunctorE':
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "v11 (𝔉⦇ObjMap⦈)"
    and "v11 (𝔉⦇ArrMap⦈)"
    and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
    and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
  using assms by (simp_all add: is_iso_semifunctorD')


text‹Elementary properties.›

context is_iso_semifunctor
begin

interpretation dghm: is_iso_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
  by (rule iso_smcf_is_iso_dghm) 

lemmas_with [unfolded slicing_simps]:
  iso_smcf_ObjMap_vrange[smcf_cs_simps] = dghm.iso_dghm_ObjMap_vrange
  and iso_smcf_ArrMap_vrange[smcf_cs_simps] = dghm.iso_dghm_ArrMap_vrange

sublocale ObjMap: v11 ‹𝔉⦇ObjMap⦈›
  rewrites "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈" and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
  by (rule dghm.iso_dghm_ObjMap_v11[unfolded slicing_simps]) 
    (simp_all add: smc_cs_simps smcf_cs_simps)

sublocale ArrMap: v11 ‹𝔉⦇ArrMap⦈›
  rewrites "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈" and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
  by (rule dghm.iso_dghm_ArrMap_v11[unfolded slicing_simps])
    (simp_all add: smc_cs_simps smcf_cs_simps)

lemmas_with [unfolded slicing_simps]:
  iso_smcf_Obj_HomDom_if_Obj_HomCod[elim] = 
    dghm.iso_dghm_Obj_HomDom_if_Obj_HomCod
  and iso_smcf_Arr_HomDom_if_Arr_HomCod[elim] = 
    dghm.iso_dghm_Arr_HomDom_if_Arr_HomCod
  and iso_smcf_ObjMap_eqE[elim] = dghm.iso_dghm_ObjMap_eqE
  and iso_smcf_ArrMap_eqE[elim] = dghm.iso_dghm_ArrMap_eqE

end

sublocale is_iso_semifunctor ⊆ is_ff_semifunctor 
proof-
  interpret dghm: is_iso_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
    by (rule iso_smcf_is_iso_dghm) 
  show "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅" by unfold_locales
qed

lemmas (in is_iso_semifunctor) iso_smcf_is_ff_semifunctor = 
  is_ff_semifunctor_axioms

lemmas [smcf_cs_intros] = is_iso_semifunctor.iso_smcf_is_ff_semifunctor


subsubsection‹Opposite isomorphism of semicategories›

lemma (in is_iso_semifunctor) is_iso_semifunctor_op: 
  "op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ op_smc 𝔅"   
  by 
    (
      rule is_iso_semifunctorI, 
      unfold smc_op_simps slicing_simps slicing_commute[symmetric]
    )
    (
      simp_all add: 
        is_semifunctor_op is_iso_dghm.is_iso_dghm_op iso_smcf_is_iso_dghm
    )

lemmas is_iso_semifunctor_op[smc_op_intros] =
  is_iso_semifunctor.is_iso_semifunctor_op


subsubsection‹
The composition of isomorphisms of semicategories is an isomorphism of 
semicategories
›

lemma smcf_comp_is_iso_semifunctor[smcf_cs_intros]:
  assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
proof(intro is_iso_semifunctorI)
  interpret 𝔉: is_iso_semifunctor α 𝔄 𝔅 𝔉 using assms by auto
  interpret 𝔊: is_iso_semifunctor α 𝔅 ℭ 𝔊 using assms by auto
  from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms show 
    "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" 
    by (auto intro: smcf_cs_intros)
  show "smcf_dghm (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ smc_dg ℭ"
    by 
      (
        auto 
          intro: dghm_cs_intros slicing_intros 
          simp: slicing_commute[symmetric]
      )
qed



subsection‹Inverse semifunctor›

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

lemmas [smc_cs_simps] = inv_dghm_components(3,4)


text‹Slicing.›

lemma dghm_inv_smcf[slicing_commute]: 
  "inv_dghm (smcf_dghm 𝔉) = smcf_dghm (inv_smcf 𝔉)"
  unfolding smcf_dghm_def inv_dghm_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)

context is_iso_semifunctor
begin

interpretation dghm: is_iso_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
  by (rule iso_smcf_is_iso_dghm) 

lemmas_with [unfolded slicing_simps slicing_commute]:
  inv_smcf_ObjMap_v11 = dghm.inv_dghm_ObjMap_v11
  and inv_smcf_ObjMap_vdomain = dghm.inv_dghm_ObjMap_vdomain
  and inv_smcf_ObjMap_app = dghm.inv_dghm_ObjMap_app
  and inv_smcf_ObjMap_vrange = dghm.inv_dghm_ObjMap_vrange
  and inv_smcf_ArrMap_v11 = dghm.inv_dghm_ArrMap_v11
  and inv_smcf_ArrMap_vdomain = dghm.inv_dghm_ArrMap_vdomain
  and inv_smcf_ArrMap_app = dghm.inv_dghm_ArrMap_app
  and inv_smcf_ArrMap_vrange = dghm.inv_dghm_ArrMap_vrange
  and iso_smcf_ObjMap_inv_smcf_ObjMap_app[smcf_cs_simps] =
    dghm.iso_dghm_ObjMap_inv_dghm_ObjMap_app
  and iso_smcf_ArrMap_inv_smcf_ArrMap_app[smcf_cs_simps] = 
    dghm.iso_dghm_ArrMap_inv_dghm_ArrMap_app
  and iso_smcf_HomDom_is_arr_conv = dghm.iso_dghm_HomDom_is_arr_conv
  and iso_smcf_HomCod_is_arr_conv = dghm.iso_dghm_HomCod_is_arr_conv
  and iso_inv_smcf_ObjMap_smcf_ObjMap_app[smcf_cs_simps] = 
    dghm.iso_inv_dghm_ObjMap_dghm_ObjMap_app
  and iso_inv_smcf_ArrMap_smcf_ArrMap_app[smcf_cs_simps] =
    dghm.iso_inv_dghm_ArrMap_dghm_ArrMap_app

end

lemmas [smcf_cs_intros] = 
  is_iso_semifunctor.inv_smcf_ObjMap_v11
  is_iso_semifunctor.inv_smcf_ArrMap_v11

lemmas [smcf_cs_simps] = 
  is_iso_semifunctor.inv_smcf_ObjMap_vdomain
  is_iso_semifunctor.inv_smcf_ObjMap_app
  is_iso_semifunctor.inv_smcf_ObjMap_vrange
  is_iso_semifunctor.inv_smcf_ArrMap_vdomain
  is_iso_semifunctor.inv_smcf_ArrMap_app
  is_iso_semifunctor.inv_smcf_ArrMap_vrange
  is_iso_semifunctor.iso_smcf_ObjMap_inv_smcf_ObjMap_app
  is_iso_semifunctor.iso_smcf_ArrMap_inv_smcf_ArrMap_app
  is_iso_semifunctor.iso_inv_smcf_ObjMap_smcf_ObjMap_app
  is_iso_semifunctor.iso_inv_smcf_ArrMap_smcf_ArrMap_app



subsection‹
An isomorphism of semicategories is an isomorphism in the category ‹SemiCAT›
›

lemma is_iso_arr_is_iso_semifunctor:
  ―‹See Chapter I-3 in \cite{mac_lane_categories_2010}.›
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
    and "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔄"
    and "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 = smcf_id 𝔄"
    and "𝔉 ∘⇩S⇩M⇩C⇩F 𝔊 = smcf_id 𝔅"
  shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
proof-
  interpret 𝔉: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(1))
  interpret 𝔊: is_semifunctor α 𝔅 𝔄 𝔊 by (rule assms(2))
  show ?thesis
  proof(rule is_iso_semifunctorI)
    have dg_𝔊𝔉𝔄: "smcf_dghm 𝔊 ∘⇩D⇩G⇩H⇩M smcf_dghm 𝔉 = dghm_id (smc_dg 𝔄)"
      by (simp add: assms(3) smcf_dghm_smcf_id smcf_dghm_smcf_comp)
    have dg_𝔉𝔊𝔅: "smcf_dghm 𝔉 ∘⇩D⇩G⇩H⇩M smcf_dghm 𝔊 = dghm_id (smc_dg 𝔅)"
      by (simp add: assms(4) smcf_dghm_smcf_id smcf_dghm_smcf_comp)
    from 𝔉.smcf_is_dghm 𝔊.smcf_is_dghm dg_𝔊𝔉𝔄 dg_𝔉𝔊𝔅 show 
      "smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ smc_dg 𝔅"
      by (rule is_iso_arr_is_iso_dghm)
  qed (simp add: 𝔉.is_semifunctor_axioms)
qed

lemma is_iso_semifunctor_is_iso_arr:
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
  shows [smcf_cs_intros]: "inv_smcf 𝔉 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
    and [smcf_cs_simps]: "inv_smcf 𝔉 ∘⇩S⇩M⇩C⇩F 𝔉 = smcf_id 𝔄"
    and [smcf_cs_simps]: "𝔉 ∘⇩S⇩M⇩C⇩F inv_smcf 𝔉 = smcf_id 𝔅"
proof-

  let ?𝔊 = ‹inv_smcf 𝔉›

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

  note is_iso_dghm = is_iso_dghm_is_iso_arr[OF iso_smcf_is_iso_dghm]

  show 𝔊: "?𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"
  proof
    (
      intro is_iso_semifunctorI is_semifunctorI; 
      (unfold slicing_commute[symmetric])?
    )
    show "vfsequence (inv_smcf 𝔉)" unfolding inv_dghm_def by simp
    show "vcard (inv_smcf 𝔉) = 4⇩ℕ"
      unfolding inv_dghm_def by (simp add: nat_omega_simps)
    show inv_iso_dghm_𝔉: 
      "inv_dghm (smcf_dghm 𝔉) : smc_dg 𝔅 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ smc_dg 𝔄"
      by (rule is_iso_dghm(1))
    show inv_dghm_𝔉: "inv_dghm (smcf_dghm 𝔉) : smc_dg 𝔅 ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔄"
      by (rule is_iso_dghmD(1)[OF inv_iso_dghm_𝔉])
    fix b c g a f assume prems: "g : b ↦⇘𝔅⇙ c" "f : a ↦⇘𝔅⇙ b"
    note is_arr_inv = is_dghm.dghm_ArrMap_is_arr[
        OF inv_dghm_𝔉, unfolded slicing_simps slicing_commute
        ]
    from prems is_arr_inv[OF prems(1)] is_arr_inv[OF prems(2)] show 
      "inv_smcf 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘𝔅⇙ f⦈ =
        inv_smcf 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔄⇙ inv_smcf 𝔉⦇ArrMap⦈⦇f⦈"
       unfolding inv_dghm_components
       by (intro v11.v11_vconverse_app)
         (
           cs_concl cs_shallow 
            cs_intro: smc_cs_intros V_cs_intros
            cs_simp: V_cs_simps smc_cs_simps
         )+
  qed (auto simp: smc_cs_simps intro: smc_cs_intros)

  show "?𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 = smcf_id 𝔄"
  proof(rule smcf_eqI, unfold dghm_comp_components inv_dghm_components)
    from 𝔊 is_semifunctor_axioms show "inv_smcf 𝔉 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔄"
      by (blast intro: smc_cs_intros)
  qed
    (
      simp_all add: 
        HomDom.smc_smcf_id_is_semifunctor
        ObjMap.v11_vcomp_vconverse 
        ArrMap.v11_vcomp_vconverse 
        dghm_id_components
    )

  show "𝔉 ∘⇩S⇩M⇩C⇩F inv_smcf 𝔉 = smcf_id 𝔅"
  proof(rule smcf_eqI, unfold dghm_comp_components inv_dghm_components)
    from 𝔊 is_semifunctor_axioms show "𝔉 ∘⇩S⇩M⇩C⇩F inv_smcf 𝔉 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
      by (blast intro: smc_cs_intros)
  qed 
    (
      simp_all add: 
        HomCod.smc_smcf_id_is_semifunctor
        ObjMap.v11_vcomp_vconverse' 
        ArrMap.v11_vcomp_vconverse' 
        dghm_id_components
    )

qed


subsubsection‹An identity semifunctor is an isomorphism of semicategories›

lemma (in semicategory) smc_smcf_id_is_iso_semifunctor: 
  "smcf_id ℭ : ℭ ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
  by (rule is_iso_semifunctorI, unfold slicing_simps slicing_commute[symmetric])
    (
      simp_all add: 
        smc_smcf_id_is_semifunctor digraph.dg_dghm_id_is_iso_dghm smc_digraph
    )

lemma (in semicategory) smc_smcf_id_is_iso_semifunctor'[smcf_cs_intros]: 
  assumes "𝔄' = ℭ" and "𝔅' = ℭ"
  shows "smcf_id ℭ : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅'"
  unfolding assms by (rule smc_smcf_id_is_iso_semifunctor)

lemmas [smcf_cs_intros] = semicategory.smc_smcf_id_is_iso_semifunctor'



subsection‹Isomorphic semicategories›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›

locale iso_semicategory = L: semicategory α 𝔄 + R: semicategory α 𝔅 
  for α 𝔄 𝔅 +
  assumes iso_smc_is_iso_semifunctor: "∃𝔉. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"

notation iso_semicategory (infixl ‹≈⇩S⇩M⇩Cı› 50)


text‹Rules.›

lemma iso_semicategoryI:
  assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" 
  shows "𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔅"
  using assms 
  unfolding iso_semicategory_def iso_semicategory_axioms_def 
  by blast

lemma iso_semicategoryD[dest]:
  assumes "𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔅" 
  shows "∃𝔉. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" 
  using assms 
  unfolding iso_semicategory_def iso_semicategory_axioms_def 
  by simp_all

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


text‹Elementary properties.›

lemma (in iso_semicategory) iso_smc_iso_digraph: "smc_dg 𝔄 ≈⇩D⇩G⇘α⇙ smc_dg 𝔅"
  using iso_smc_is_iso_semifunctor 
  by (auto intro: slicing_intros iso_digraphI)


subsubsection‹A semicategory isomorphism is an equivalence relation›

lemma iso_semicategory_refl: 
  assumes "semicategory α 𝔄" 
  shows "𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔄"
proof(rule iso_semicategoryI[of _  _ _ ‹smcf_id 𝔄›])
  interpret semicategory α 𝔄 by (rule assms)
  show "smcf_id 𝔄 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔄"  
    by (simp add: smc_smcf_id_is_iso_semifunctor)
qed

lemma iso_semicategory_sym[sym]:
  assumes "𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔅" 
  shows "𝔅 ≈⇩S⇩M⇩C⇘α⇙ 𝔄"
proof-
  interpret iso_semicategory α 𝔄 𝔅 by (rule assms)
  from iso_smc_is_iso_semifunctor obtain 𝔉 where "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" 
    by clarsimp
  then have "inv_smcf 𝔉 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔄" 
    by (simp add: is_iso_semifunctor_is_iso_arr(1))
  then show ?thesis by (auto intro: iso_semicategoryI)
qed

lemma iso_semicategory_trans[trans]:
  assumes "𝔄 ≈⇩S⇩M⇩C⇘α⇙ 𝔅" and "𝔅 ≈⇩S⇩M⇩C⇘α⇙ ℭ" 
  shows "𝔄 ≈⇩S⇩M⇩C⇘α⇙ ℭ"
proof-  
  interpret L: iso_semicategory α 𝔄 𝔅 by (rule assms(1))
  interpret R: iso_semicategory α 𝔅 ℭ by (rule assms(2))
  from L.iso_smc_is_iso_semifunctor R.iso_smc_is_iso_semifunctor show ?thesis
    by (auto intro: iso_semicategoryI smcf_cs_intros)
qed

text‹\newpage›

end