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 𝔄 ↦↦DGα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  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"

syntax "_is_semifunctor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦SMCı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦SMCα𝔅"  "CONST is_semifunctor α 𝔄 𝔅 𝔉"

abbreviation (input) is_cn_semifunctor :: "V  V  V  V  bool"
  where "is_cn_semifunctor α 𝔄 𝔅 𝔉  𝔉 : op_smc 𝔄 ↦↦SMCα𝔅"

syntax "_is_cn_semifunctor" :: "V  V  V  V  bool" 
  ((_ :/ _ SMC↦↦ı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 SMC↦↦α𝔅"  "CONST is_cn_semifunctor α 𝔄 𝔅 𝔉"

abbreviation all_smcfs :: "V  V"
  where "all_smcfs α  set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦SMCα𝔅}"

abbreviation smcfs :: "V  V  V  V"
  where "smcfs α 𝔄 𝔅  set {𝔉. 𝔉 : 𝔄 ↦↦SMCα𝔅}"

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

lemma smcf_is_dghm'[slicing_intros]:
  assumes "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "𝔄' = smc_dg 𝔄"
    and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦DGα𝔅'"
  using assms(1) unfolding assms(2,3) by (rule is_semifunctor.smcf_is_dghm)

lemma cn_dghm_comp_is_dghm: 
  assumes "𝔉 : op_smc 𝔄 ↦↦SMCα𝔅"
  shows "smcf_dghm 𝔉 : op_dg (smc_dg 𝔄) ↦↦DGα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 𝔄 ↦↦SMCα𝔅"
    and "𝔄' = op_dg (smc_dg 𝔄)"
    and "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦DGα𝔅'"
  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 "𝔉 : 𝔄' ↦↦SMCα'𝔅'"
  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 
      𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"
    and "b c g a f.  g : b 𝔄c; f : a 𝔄b  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"
  shows "𝔉 : 𝔄 ↦↦SMCα𝔅"
  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 "𝔉 : 𝔄 ↦↦SMCα𝔅"
  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 
      𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"
    and "b c g a f.  g : b 𝔄c; f : a 𝔄b  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"
  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 "𝔉 : 𝔄 ↦↦SMCα𝔅"
  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 
      𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"
    and "b c g a f.  g : b 𝔄c; f : a 𝔄b  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"
  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 𝔄 ↦↦SMCα𝔅"
    and "g : c 𝔄b"
    and "f : b 𝔄a"
  shows "𝔉ArrMapf A𝔄g = 𝔉ArrMapg A𝔅𝔉ArrMapf"
proof-
  from assms(3,4) have gf:
    "𝔉ArrMapg A𝔅𝔉ArrMapf = 𝔉ArrMapg Aop_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 "𝔊 : 𝔄 ↦↦SMCα𝔅" 
    and "𝔉 :  ↦↦SMCα𝔇"
    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 "𝔊 : 𝔄 ↦↦SMCα𝔅"
    and "𝔉 :  ↦↦SMCα𝔇"
    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 "𝔉 : 𝔄 ↦↦SMCβ𝔅"
  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 {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦SMCα𝔅}"
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 "{𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦SMCα𝔅} = {}" 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 𝔉: "𝔉 : 𝔄 ↦↦SMCα𝔅" 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 {𝔉. 𝔉 : 𝔄 ↦↦SMCα𝔅}"
  by (rule down[of _ set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦SMCα𝔅}]) 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 𝔄 ↦↦SMCα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 𝔉ArrMapg Aop_smc 𝔄f =
      op_smcf 𝔉ArrMapg Aop_smc 𝔅op_smcf 𝔉ArrMapf"
    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 𝔉 : 𝔄' ↦↦SMCα'𝔅'"
  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 𝔉) : 𝔄 ↦↦SMCα𝔅"
    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 "𝔊 : 𝔄 ↦↦SMCα𝔅" and "𝔉 :  ↦↦SMCα𝔇"
  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 "SMCF" 55)
  where "smcf_comp  dghm_comp"


text‹Slicing.›

lemma smcf_dghm_smcf_comp[slicing_commute]: 
  "smcf_dghm 𝔊 DGHM smcf_dghm 𝔉 = smcf_dghm (𝔊 SMCF 𝔉)"
  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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "vsv ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "𝒟 ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows " ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 ↦↦SMCα" 
    and "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and [simp]: "a  𝔄Obj"
  shows "(𝔊 SMCF 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "vsv ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "𝒟 ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows " ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 ↦↦SMCα" 
    and "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and [simp]: "f  𝔄Arr"
  shows "(𝔊 SMCF 𝔉)ArrMapf = 𝔊ArrMap𝔉ArrMapf"
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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMCα"
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 (𝔊 SMCF 𝔉)" by (simp add: dghm_comp_def)
    show "vcard (𝔊 SMCF 𝔉) = 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 "(𝔊 SMCF 𝔉)ArrMapg A𝔄f = 
      (𝔊 SMCF 𝔉)ArrMapg A(𝔊 SMCF 𝔉)ArrMapf"
      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 " :  ↦↦SMCα𝔇" 
    and "𝔊 : 𝔅 ↦↦SMCα" 
    and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "( SMCF 𝔊) SMCF 𝔉 =  SMCF (𝔊 SMCF 𝔉)"
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 " SMCF (𝔊 SMCF 𝔉) : 𝔄 ↦↦SMCα𝔇" 
    and " SMCF 𝔊 SMCF 𝔉 : 𝔄 ↦↦SMCα𝔇"  
    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 (𝔊 SMCF 𝔉) = op_smcf 𝔊 SMCF 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 SMCF 55)
  where "𝔊 SMCF 𝔉 =
    [
      𝔊ObjMap  𝔉ObjMap, 
      𝔊ArrMap  𝔉ArrMap, 
      op_smc (𝔉HomDom), 
      𝔊HomCod
    ]"


text‹Components.›

lemma smcf_cn_comp_components:
  shows "(𝔊 SMCF 𝔉)ObjMap = 𝔊ObjMap  𝔉ObjMap"
    and "(𝔊 SMCF 𝔉)ArrMap = 𝔊ArrMap  𝔉ArrMap"
    and [smc_cn_cs_simps]: "(𝔊 SMCF 𝔉)HomDom = op_smc (𝔉HomDom)"
    and [smc_cn_cs_simps]: "(𝔊 SMCF 𝔉)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 𝔊 DGHM smcf_dghm 𝔉 = smcf_dghm (𝔊 SMCF 𝔉)"
  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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows "vsv ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows "𝒟 ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows " ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅" and "a  𝔄Obj"
  shows "(𝔊 SMCF 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows "vsv ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows "𝒟 ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows " ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅" and "a  𝔄Arr"
  shows "(𝔊 SMCF 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa"
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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "vsv ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "𝒟 ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows " ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅" and "a  𝔄Obj"
  shows "(𝔊 SMCF 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "vsv ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "𝒟 ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows " ((𝔊 SMCF 𝔉)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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅" and "f  𝔄Arr"
  shows "(𝔊 SMCF 𝔉)ArrMapf = 𝔊ArrMap𝔉ArrMapf"
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 (𝔊 SMCF 𝔉) = op_smcf 𝔊 SMCF 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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMCα"
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 (𝔊 SMCF 𝔉) : smc_dg 𝔄 ↦↦DGα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 "(𝔊 SMCF 𝔉)ArrMapg A𝔄f = 
      (𝔊 SMCF 𝔉)ArrMapg A(𝔊 SMCF 𝔉)ArrMapf"
      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 "𝔊 : 𝔅 SMC↦↦α" and "𝔉 : 𝔄 ↦↦SMCα𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 SMC↦↦α"
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 (𝔊 SMCF 𝔉) : smc_dg (op_smc 𝔄) ↦↦DGαsmc_dg "
      by 
        (
          cs_concl cs_shallow 
            cs_simp: slicing_commute[symmetric]
            cs_intro: dg_cn_cs_intros slicing_intros
        )
    show "vfsequence (𝔊 SMCF 𝔉)" unfolding smcf_cn_comp_def by simp
    show "vcard (𝔊 SMCF 𝔉) = 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 
      "(𝔊 SMCF 𝔉)ArrMapf A𝔄g = 
        (𝔊 SMCF 𝔉)ArrMapg A(𝔊 SMCF 𝔉)ArrMapf"
      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 "𝔊 : 𝔅 ↦↦SMCα" and "𝔉 : 𝔄 SMC↦↦α𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 SMC↦↦α"
  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  :  ↦↦SMCα"
proof(rule is_semifunctorI, unfold dghm_id_components)
  from smc_dghm_id_is_dghm show 
    "smcf_dghm (smcf_id ) : smc_dg  ↦↦DGα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 Af = 
    vid_on (Arr)g Avid_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  : 𝔄 ↦↦SMCα𝔅"
  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 𝔅 SMCF 𝔉 = 𝔉"
  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}).›
  "𝔉 SMCF 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 :  ↦↦SMCα𝔇"
proof-
  interpret: semicategory α  by (rule assms(1))
  interpret 𝔇: semicategory α 𝔇 by (rule assms(2))
  show ?thesis
  proof(intro is_semifunctorI, tacticdistinct_subgoals_tac)
    from assms show 
      "smcf_dghm (dghm_const  𝔇 a f) : smc_dg  ↦↦DGα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 fArrMapg' Af' =
      smcf_const  𝔇 a fArrMapg' A𝔇smcf_const  𝔇 a fArrMapf'"
      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 : 𝔄 ↦↦SMCα𝔅"
  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 Af = f"
  shows "smcf_const 𝔅  a f SMCF 𝔉 = smcf_const 𝔄  a f"
proof(rule smcf_dghm_eqI)
  interpret: semicategory α  by (rule assms(1))
  from assms(2) show "smcf_const 𝔅  a f SMCF 𝔉 : 𝔄 ↦↦SMCα"
    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 : 𝔄 ↦↦SMCα"
    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 SMCF 𝔉) = 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 𝔄 ↦↦DG.faithfulαsmc_dg 𝔅"

syntax "_is_ft_semifunctor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦SMC.faithfulı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦SMC.faithfulα𝔅"  "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 𝔉 : 𝔄' ↦↦DG.faithfulα𝔅'"
  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 "𝔉 : 𝔄' ↦↦SMC.faithfulα'𝔅'"
  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 "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   v11 (𝔉ArrMap l Hom 𝔄 a b)"
  shows "𝔉 : 𝔄 ↦↦SMC.faithfulα𝔅"
  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 "𝔉 : 𝔄 ↦↦SMC.faithfulα𝔅"
  shows "𝔉 : 𝔄 ↦↦SMCα𝔅"
    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 "𝔉 : 𝔄 ↦↦SMC.faithfulα𝔅"
  obtains "𝔉 : 𝔄 ↦↦SMCα𝔅"
    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 "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "a b g f.
       g : a 𝔄b; f : a 𝔄b; 𝔉ArrMapg = 𝔉ArrMapf   g = f"
  shows "𝔉 : 𝔄 ↦↦SMC.faithfulα𝔅"
  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 𝔄 ↦↦SMC.faithfulα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 𝔉 : 𝔄' ↦↦SMC.faithfulα𝔅'"
  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 "𝔊 : 𝔅 ↦↦SMC.faithfulα" and "𝔉 : 𝔄 ↦↦SMC.faithfulα𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMC.faithfulα"
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 𝔊𝔉: 
    "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMCα"
    by (auto intro: smc_cs_intros)
  then interpret is_semifunctor α 𝔄  𝔊 SMCF 𝔉 .
  show "smcf_dghm (𝔊 SMCF 𝔉) : smc_dg 𝔄 ↦↦DG.faithfulα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 𝔄 ↦↦DG.fullαsmc_dg 𝔅"

syntax "_is_fl_semifunctor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦SMC.fullı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦SMC.fullα𝔅"  "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 𝔉 : 𝔄' ↦↦DG.fullα𝔅'"
  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 "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj  
      𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  shows "𝔉 : 𝔄 ↦↦SMC.fullα𝔅"
  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 "𝔉 : 𝔄 ↦↦SMC.fullα𝔅"
  shows "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   
      𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  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 "𝔉 : 𝔄 ↦↦SMC.fullα𝔅"
  obtains "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   
      𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  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 𝔄 ↦↦SMC.fullα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 𝔉 : 𝔄' ↦↦SMC.fullα𝔅'"
  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 "𝔊 : 𝔅 ↦↦SMC.fullα" and "𝔉 : 𝔄 ↦↦SMC.fullα𝔅" 
  shows "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMC.fullα"
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
    "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMCα" 
    by (auto intro: smc_cs_intros)
  show "smcf_dghm (𝔊 DGHM 𝔉) : smc_dg 𝔄 ↦↦DG.fullα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"
  ((_ :/ _ ↦↦SMC.ffı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦SMC.ffα𝔅"  "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 𝔄 ↦↦DG.ffα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 𝔉 : 𝔄' ↦↦DG.ffα𝔅'"
  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 𝔄 ↦↦SMC.ffα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 𝔉 : 𝔄' ↦↦SMC.ffα𝔅'"
  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 "𝔊 : 𝔅 ↦↦SMC.ffα" and "𝔉 : 𝔄 ↦↦SMC.ffα𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMC.ffα"
  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 𝔄 ↦↦DG.isoαsmc_dg 𝔅"

syntax "_is_iso_semifunctor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦SMC.isoı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"  "CONST is_iso_semifunctor α 𝔄 𝔅 𝔉"

lemma (in is_iso_semifunctor) iso_smcf_is_iso_dghm'[slicing_intros]:
  assumes "𝔄' = smc_dg 𝔄" "𝔅' = smc_dg 𝔅"
  shows "smcf_dghm 𝔉 : 𝔄' ↦↦DG.isoα𝔅'"
  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 "𝔉 : 𝔄' ↦↦SMC.isoα'𝔅'"
  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 "𝔉 : 𝔄 ↦↦SMCα𝔅"
    and "v11 (𝔉ObjMap)"
    and "v11 (𝔉ArrMap)"
    and " (𝔉ObjMap) = 𝔅Obj"
    and " (𝔉ArrMap) = 𝔅Arr"
  shows "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  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 "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  shows "𝔉 : 𝔄 ↦↦SMCα𝔅"
    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 "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  obtains "𝔉 : 𝔄 ↦↦SMCα𝔅"
    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 "𝔉 : 𝔄 ↦↦SMC.ffα𝔅" 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 𝔄 ↦↦SMC.isoα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 "𝔊 : 𝔅 ↦↦SMC.isoα" and "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  shows "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMC.isoα"
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 
    "𝔊 SMCF 𝔉 : 𝔄 ↦↦SMCα" 
    by (auto intro: smcf_cs_intros)
  show "smcf_dghm (𝔊 DGHM 𝔉) : smc_dg 𝔄 ↦↦DG.isoα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