Theory CZH_ECAT_Functor

(* Copyright 2021 (C) Mihails Milehins *)

section‹Functor›
theory CZH_ECAT_Functor
  imports 
    CZH_ECAT_Category
    CZH_Foundations.CZH_SMC_Semifunctor
begin



subsection‹Background›

named_theorems cf_cs_simps
named_theorems cf_cs_intros

named_theorems cat_cn_cs_simps
named_theorems cat_cn_cs_intros

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


subsubsection‹Slicing›

definition cf_smcf :: "V  V"
  where "cf_smcf  = 
    [ObjMap, ArrMap, cat_smc (HomDom), cat_smc (HomCod)]"


text‹Components.›

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



subsection‹Definition and elementary properties›


text‹See Chapter I-3 in cite"mac_lane_categories_2010".›

locale is_functor = 
  𝒵 α + vfsequence 𝔉 + HomDom: category α 𝔄 + HomCod: category α 𝔅 
  for α 𝔄 𝔅 𝔉 +
  assumes cf_length[cat_cs_simps]: "vcard 𝔉 = 4" 
    and cf_is_semifunctor[slicing_intros]: 
      "cf_smcf 𝔉 : cat_smc 𝔄 ↦↦SMCαcat_smc 𝔅" 
    and cf_HomDom[cat_cs_simps]: "𝔉HomDom = 𝔄"
    and cf_HomCod[cat_cs_simps]: "𝔉HomCod = 𝔅"
    and cf_ObjMap_CId[cat_cs_intros]: 
      "c  𝔄Obj  𝔉ArrMap𝔄CIdc = 𝔅CId𝔉ObjMapc"

syntax "_is_functor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦Cı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦Cα𝔅"  "CONST is_functor α 𝔄 𝔅 𝔉"

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

syntax "_is_cn_cf" :: "V  V  V  V  bool"
  ((_ :/ _ C↦↦ı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 C↦↦α𝔅"  "CONST is_cn_cf α 𝔄 𝔅 𝔉"

abbreviation all_cfs :: "V  V"
  where "all_cfs α  set {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅}"

abbreviation cfs :: "V  V  V  V"
  where "cfs α 𝔄 𝔅  set {𝔉. 𝔉 : 𝔄 ↦↦Cα𝔅}"

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

lemma cn_cf_ObjMap_CId[cat_cn_cs_simps]: 
  assumes "𝔉 : 𝔄 C↦↦α𝔅" and "c  𝔄Obj"
  shows "𝔉ArrMap𝔄CIdc = 𝔅CId𝔉ObjMapc"
proof-
  interpret is_functor α op_cat 𝔄 𝔅 𝔉 by (rule assms(1))
  from assms(2) have c: "c  op_cat 𝔄Obj" unfolding cat_op_simps by simp
  show ?thesis by (rule cf_ObjMap_CId[OF c, unfolded cat_op_simps])
qed

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

lemmas [slicing_intros] = is_functor.cf_is_semifunctor'

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

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


text‹Rules.›

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

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

lemmas [cat_cs_intros] = is_functorD(3,4)

lemma is_functorI':
  assumes "𝒵 α"
    and "vfsequence 𝔉"
    and "category α 𝔄"
    and "category α 𝔅"
    and "vcard 𝔉 = 4"
    and "𝔉HomDom = 𝔄"
    and "𝔉HomCod = 𝔅"
    and "vsv (𝔉ObjMap)"
    and "vsv (𝔉ArrMap)"
    and "𝒟 (𝔉ObjMap) = 𝔄Obj"
    and " (𝔉ObjMap)  𝔅Obj"
    and "𝒟 (𝔉ArrMap) = 𝔄Arr"
    and "a b f. f : a 𝔄b 
      𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"
    and "b c g a f.  g : b 𝔄c; f : a 𝔄b  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"
    and "(c. c  𝔄Obj  𝔉ArrMap𝔄CIdc = 𝔅CId𝔉ObjMapc)"
  shows "𝔉 : 𝔄 ↦↦Cα𝔅"
  by 
    (
      intro is_functorI is_semifunctorI', 
      unfold cf_smcf_components slicing_simps
    )
    (simp_all add: assms cf_smcf_def nat_omega_simps category.cat_semicategory)

lemma is_functorD':
  assumes "𝔉 : 𝔄 ↦↦Cα𝔅"
  shows "𝒵 α"
    and "vfsequence 𝔉"
    and "category α 𝔄"
    and "category α 𝔅"
    and "vcard 𝔉 = 4"
    and "𝔉HomDom = 𝔄"
    and "𝔉HomCod = 𝔅"
    and "vsv (𝔉ObjMap)"
    and "vsv (𝔉ArrMap)"
    and "𝒟 (𝔉ObjMap) = 𝔄Obj"
    and " (𝔉ObjMap)  𝔅Obj"
    and "𝒟 (𝔉ArrMap) = 𝔄Arr"
    and "a b f. f : a 𝔄b 
      𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"
    and "b c g a f.  g : b 𝔄c; f : a 𝔄b  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"
    and "(c. c  𝔄Obj  𝔉ArrMap𝔄CIdc = 𝔅CId𝔉ObjMapc)"
  by 
    (
      simp_all add: 
        is_functorD(2-9)[OF assms] 
        is_semifunctorD'[OF is_functorD(6)[OF assms], unfolded slicing_simps]
    )

lemma is_functorE':
  assumes "𝔉 : 𝔄 ↦↦Cα𝔅"
  obtains "𝒵 α"
    and "vfsequence 𝔉"
    and "category α 𝔄"
    and "category α 𝔅"
    and "vcard 𝔉 = 4"
    and "𝔉HomDom = 𝔄"
    and "𝔉HomCod = 𝔅"
    and "vsv (𝔉ObjMap)"
    and "vsv (𝔉ArrMap)"
    and "𝒟 (𝔉ObjMap) = 𝔄Obj"
    and " (𝔉ObjMap)  𝔅Obj"
    and "𝒟 (𝔉ArrMap) = 𝔄Arr"
    and "a b f. f : a 𝔄b 
      𝔉ArrMapf : 𝔉ObjMapa 𝔅𝔉ObjMapb"
    and "b c g a f.  g : b 𝔄c; f : a 𝔄b  
      𝔉ArrMapg A𝔄f = 𝔉ArrMapg A𝔅𝔉ArrMapf"
    and "(c. c  𝔄Obj  𝔉ArrMap𝔄CIdc = 𝔅CId𝔉ObjMapc)"
  using assms by (simp add: is_functorD')


text‹A functor is a semifunctor.›

context is_functor
begin

interpretation smcf: is_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
  by (rule cf_is_semifunctor)

sublocale ObjMap: vsv 𝔉ObjMap
  by (rule smcf.ObjMap.vsv_axioms[unfolded slicing_simps])
sublocale ArrMap: vsv 𝔉ArrMap
  by (rule smcf.ArrMap.vsv_axioms[unfolded slicing_simps])

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

lemmas_with [unfolded slicing_simps]: 
  cf_ArrMap_Comp = smcf.smcf_ArrMap_Comp

end

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

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


text‹Elementary properties.›

lemma cn_cf_ArrMap_Comp[cat_cn_cs_simps]: 
  assumes "category α 𝔄" 
    and "𝔉 : 𝔄 C↦↦α𝔅"
    and "g : c 𝔄b"
    and "f : b 𝔄a" 
  shows "𝔉ArrMapf A𝔄g = 𝔉ArrMapg A𝔅𝔉ArrMapf"
proof-
  interpret 𝔄: category α 𝔄 by (rule assms(1))
  interpret 𝔉: is_functor α op_cat 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule cn_smcf_ArrMap_Comp
          [
            OF 
              𝔄.cat_semicategory 
              𝔉.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_simps,
            OF assms(3,4)
          ]
      )
qed

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

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

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


text‹Size.›

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

lemma (in is_functor) cf_is_functor_if_ge_Limit:
  assumes "𝒵 β" and "α  β"
  shows "𝔉 : 𝔄 ↦↦Cβ𝔅"
  by (rule is_functorI)
    (
      auto simp:
        cat_cs_simps
        assms 
        vfsequence_axioms
        cf_is_semifunctor_if_ge_Limit
        HomDom.cat_category_if_ge_Limit
        HomCod.cat_category_if_ge_Limit
        intro: cat_cs_intros 
    )

lemma small_all_cfs[simp]: "small {𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅}"
proof(cases 𝒵 α)
  case True
  from is_functor.cf_in_Vset show ?thesis
    by (intro down[of _ Vset (α + ω)])
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{𝔉. 𝔄 𝔅. 𝔉 : 𝔄 ↦↦Cα𝔅} = {}" by auto
  then show ?thesis by simp
qed

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

lemma (in 𝒵) all_cfs_in_Vset: 
  assumes "𝒵 β" and "α  β"
  shows "all_cfs α  Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "all_cfs α  Vset (α + 7)"
  proof(intro vsubsetI)
    fix 𝔉 assume "𝔉  all_cfs α"
    then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦Cα𝔅" by clarsimp
    interpret is_functor α 𝔄 𝔅 𝔉 using 𝔉 by simp
    show "𝔉  Vset (α + 7)" by (rule cf_in_Vset_7)
  qed
  from assms(2) show "Vset (α + 7)  Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

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


subsubsection‹Further properties›

lemma (in is_functor) cf_ArrMap_is_iso_arr:
  assumes "f : a iso𝔄b"
  shows "𝔉ArrMapf : 𝔉ObjMapa iso𝔅𝔉ObjMapb"
proof-

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

  show ?thesis
  proof(intro is_iso_arrI is_inverseI)
    from inv_f(2) show 𝔉_inv_f: 
      "𝔉ArrMapf¯C𝔄 : 𝔉ObjMapb 𝔅𝔉ObjMapa"
      by (cs_concl cs_intro: cat_cs_intros)
    note cf_ArrMap_Comp is_functor.cf_ArrMap_Comp[cat_cs_simps del]
    from assms f(1) inv_f show 
      "𝔉ArrMapf¯C𝔄 A𝔅𝔉ArrMapf = 𝔅CId𝔉ObjMapa"
      "𝔉ArrMapf A𝔅𝔉ArrMapf¯C𝔄 = 𝔅CId𝔉ObjMapb"
      by
        (
          cs_concl
            cs_simp: cat_cs_simps cf_ArrMap_Comp[symmetric] 
            cs_intro: cat_cs_intros
        )+
  qed (intro cf_ArrMap_is_arr[OF f(1)])+

qed

lemma (in is_functor) cf_ArrMap_is_iso_arr'[cat_arrow_cs_intros]:
  assumes "f : a iso𝔄b" and "𝔉a = 𝔉ObjMapa" and "𝔉b = 𝔉ObjMapb"
  shows "𝔉ArrMapf : 𝔉a iso𝔅𝔉b"
  using assms(1) unfolding assms(2,3) by (rule cf_ArrMap_is_iso_arr)

lemmas [cat_arrow_cs_intros] = is_functor.cf_ArrMap_is_iso_arr'



subsection‹Opposite functor›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-2 in cite"mac_lane_categories_2010".›

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


text‹Components.›

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


text‹Slicing.›

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


text‹Elementary properties.›

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


subsubsection‹Further properties›

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

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

lemmas is_functor_op[cat_op_intros] = is_functor.is_functor_op'

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

lemmas cf_op_cf_op_cf[cat_op_simps] = is_functor.cf_op_cf_op_cf

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



subsection‹Composition of covariant functors›


subsubsection‹Definition and elementary properties›

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


text‹Slicing.›

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


subsubsection‹Object map›

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

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

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

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


subsubsection‹Arrow map›

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

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

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

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


subsubsection‹Further properties›

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

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


text‹The opposite of the covariant composition of functors.›

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


text‹Composition helper.›

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



subsection‹Composition of contravariant functors›


subsubsection‹Definition and elementary properties›


text‹See section 1.2 in cite"bodo_categories_1970".›

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


text‹Components.›

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


text‹Slicing.›

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


subsubsection‹Object map: two contravariant functors›

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

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

lemma cf_cn_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 C↦↦α𝔅"
  shows " ((𝔊 CF 𝔉)ObjMap)  Obj"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α op_cat 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ObjMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ObjMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 C↦↦α𝔅" and "a  𝔄Obj"
  shows "(𝔊 CF 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α op_cat 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ObjMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps, 
            OF assms(3)
          ]
      )
qed


subsubsection‹Arrow map: two contravariant functors›

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

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

lemma cf_cn_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 C↦↦α𝔅"
  shows " ((𝔊 CF 𝔉)ArrMap)  Arr"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α op_cat 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ArrMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_comp_ArrMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 C↦↦α𝔅" and "a  𝔄Arr"
  shows "(𝔊 CF 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α op_cat 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_comp_ArrMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsection‹Object map: contravariant and covariant functor›

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

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

lemma cf_cn_cov_comp_ObjMap_vrange:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 ↦↦Cα𝔅"
  shows " ((𝔊 CF 𝔉)ObjMap)  Obj"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ObjMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 ↦↦Cα𝔅" and "a  𝔄Obj"
  shows "(𝔊 CF 𝔉)ObjMapa = 𝔊ObjMap𝔉ObjMapa"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ObjMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsection‹Arrow map: contravariant and covariant functors›

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

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

lemma cf_cn_cov_comp_ArrMap_vrange:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 ↦↦Cα𝔅"
  shows " ((𝔊 CF 𝔉)ArrMap)  Arr"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_vrange
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps
          ]
      )
qed

lemma cf_cn_cov_comp_ArrMap_app[cat_cn_cs_simps]:
  assumes "𝔊 : 𝔅 C↦↦α" and "𝔉 : 𝔄 ↦↦Cα𝔅" and "a  𝔄Arr"
  shows "(𝔊 CF 𝔉)ArrMapa = 𝔊ArrMap𝔉ArrMapa"
proof-
  interpret L: is_functor α op_cat 𝔅  𝔊 by (rule assms(1)) 
  interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
  show ?thesis
    by 
      (
        rule smcf_cn_cov_comp_ArrMap_app
          [
            OF 
              L.cf_is_semifunctor[unfolded slicing_commute[symmetric]] 
              R.cf_is_semifunctor,
            unfolded slicing_commute slicing_simps,
            OF assms(3)
          ]
      )
qed


subsubsection‹Further properties›

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


text‹See section 1.2 in cite"bodo_categories_1970").›

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


text‹See section 1.2 in cite"bodo_categories_1970".›

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


text‹The opposite of the contravariant composition of functors.›

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



subsection‹Identity functor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in cite"mac_lane_categories_2010".›

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


text‹Slicing.›

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

context category
begin

interpretation smc: semicategory α cat_smc  by (rule cat_semicategory)

lemmas_with [unfolded slicing_simps]:
  cat_smcf_id_is_semifunctor = smc.smc_smcf_id_is_semifunctor

end


subsubsection‹Object map›

lemmas [cat_cs_simps] = dghm_id_ObjMap_app


subsubsection‹Arrow map›

lemmas [cat_cs_simps] = dghm_id_ArrMap_app


subsubsection‹Opposite of an identity functor.›

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


subsubsection‹An identity functor is a functor›

lemma (in category) cat_cf_id_is_functor: "cf_id  :  ↦↦Cα"
proof(rule is_functorI, unfold dghm_id_components)
  from cat_smcf_id_is_semifunctor show 
    "cf_smcf (cf_id ) : cat_smc  ↦↦SMCαcat_smc "
    by (simp add: slicing_commute)
  from cat_CId_is_arr show 
    "c  Obj  vid_on (Arr)CIdc = CIdvid_on (Obj)c"
    for c
    by auto
qed (auto simp: dghm_id_def nat_omega_simps cat_cs_intros)

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

lemmas [cat_cs_intros] = category.cat_cf_id_is_functor'


subsubsection‹Further properties›

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

lemmas [cat_cs_simps] = is_functor.cf_cf_comp_cf_id_left

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

lemmas [cat_cs_simps] = is_functor.cf_cf_comp_cf_id_right



subsection‹Constant functor›


subsubsection‹Definition and elementary properties›


text‹See Chapter III-3 in cite"mac_lane_categories_2010".›

abbreviation cf_const :: "V  V  V  V"
  where "cf_const  𝔇 a  smcf_const  𝔇 a (𝔇CIda)"


text‹Slicing.›

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


subsubsection‹Object map and arrow map›

context
  fixes 𝔇 a :: V
begin

lemmas_with [where 𝔇=𝔇 and a=a and f=𝔇CIda, cat_cs_simps]: 
  dghm_const_ObjMap_app
  dghm_const_ArrMap_app

end


subsubsection‹Opposite constant functor›

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


subsubsection‹A constant functor is a functor›

lemma cf_const_is_functor: 
  assumes "category α " and "category α 𝔇" and "a  𝔇Obj" 
  shows "cf_const  𝔇 a :  ↦↦Cα𝔇"
proof-
  interpret: category α  by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  show ?thesis
  proof(intro is_functorI, tacticdistinct_subgoals_tac)
    show "vfsequence (dghm_const  𝔇 a (𝔇CIda))"
      unfolding dghm_const_def by simp
    show "vcard (cf_const  𝔇 a) = 4"
      unfolding dghm_const_def by (simp add: nat_omega_simps)
    from assms show "cf_smcf (cf_const  𝔇 a) : cat_smc  ↦↦SMCαcat_smc 𝔇"
      by 
        ( 
          cs_concl cs_shallow
            cs_simp: cat_cs_simps slicing_simps slicing_commute[symmetric] 
            cs_intro: smc_cs_intros cat_cs_intros slicing_intros
        )
    fix c assume "c  Obj"
    with assms show 
      "cf_const  𝔇 aArrMapCIdc = 𝔇CIdcf_const  𝔇 aObjMapc"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto simp: dghm_const_components assms)
qed 

lemma cf_const_is_functor'[cat_cs_intros]: 
  assumes "category α " 
    and "category α 𝔇" 
    and "a  𝔇Obj" 
    and "𝔄 = "
    and "𝔅 = 𝔇"
    and "f = (𝔇CIda)"
  shows "dghm_const  𝔇 a f : 𝔄 ↦↦Cα𝔅"
  using assms(1-3) unfolding assms(4-6) by (rule cf_const_is_functor)


subsubsection‹Further properties›

lemma cf_comp_cf_const_right[cat_cs_simps]:
  assumes "category α 𝔄"
    and "𝔊 : 𝔅 ↦↦Cα"
    and "b  𝔅Obj"
  shows "𝔊 CF cf_const 𝔄 𝔅 b = cf_const 𝔄  (𝔊ObjMapb)"
proof(rule cf_eqI)

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

  from assms(3) show "𝔊 CF cf_const 𝔄 𝔅 b : 𝔄 ↦↦Cα"
    by (cs_concl cs_intro: cat_cs_intros)
  from assms(3) show "cf_const 𝔄  (𝔊ObjMapb) : 𝔄 ↦↦Cα"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(3) have ObjMap_dom_lhs: 
    "𝒟 ((𝔊 CF cf_const 𝔄 𝔅 b)ObjMap) = 𝔄Obj"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(3) have ObjMap_dom_rhs: 
    "𝒟 (cf_const 𝔄  (𝔊ObjMapb)ObjMap) = 𝔄Obj"
    by (cs_concl cs_simp: cat_cs_simps)
  show "(𝔊 CF cf_const 𝔄 𝔅 b)ObjMap = cf_const 𝔄  (𝔊ObjMapb)ObjMap"
  proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
    fix a assume "a  𝔄Obj"
    with assms(3) show "(𝔊 CF cf_const 𝔄 𝔅 b)ObjMapa =
      cf_const 𝔄  (𝔊ObjMapb)ObjMapa"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto intro: assms(3) cat_cs_intros)
  from assms(3) have ArrMap_dom_lhs: 
    "𝒟 ((𝔊 CF cf_const 𝔄 𝔅 b)ArrMap) = 𝔄Arr"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(3) have ArrMap_dom_rhs: 
    "𝒟 (cf_const 𝔄  (𝔊ObjMapb)ArrMap) = 𝔄Arr"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "(𝔊 CF cf_const 𝔄 𝔅 b)ArrMap = cf_const 𝔄  (𝔊ObjMapb)ArrMap"
  proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
    fix a assume "a  𝔄Arr"
    with assms(3) show "(𝔊 CF cf_const 𝔄 𝔅 b)ArrMapa =
      cf_const 𝔄  (𝔊ObjMapb)ArrMapa"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (auto intro: assms(3) cat_cs_intros)

qed simp_all

lemma cf_comp_cf_const_right'[cat_cs_simps]:
  assumes "category α 𝔄"
    and "𝔊 : 𝔅 ↦↦Cα"
    and "b  𝔅Obj"
    and "f = 𝔅CIdb"
  shows "𝔊 CF dghm_const 𝔄 𝔅 b f = cf_const 𝔄  (𝔊ObjMapb)"
  using assms(1-3) unfolding assms(4) by (rule cf_comp_cf_const_right)

lemma (in is_functor) cf_comp_cf_const_left[cat_cs_simps]:
  assumes "category α " and "a  Obj"
  shows "cf_const 𝔅  a CF 𝔉 = cf_const 𝔄  a"
proof(rule cf_smcf_eqI)
  interpret: category α  by (rule assms(1))
  from assms(2) show "cf_const 𝔅  a CF 𝔉 : 𝔄 ↦↦Cα"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms(2) show "cf_const 𝔄  a : 𝔄 ↦↦Cα"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms(2) have CId_a: "CIda : a a"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from assms(2) have CId_CId_a: "CIda ACIda = CIda"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from 
    is_semifunctor.smcf_smcf_comp_smcf_const
      [
        OF cf_is_semifunctor ℭ.cat_semicategory, 
        unfolded slicing_simps, 
        OF CId_a CId_CId_a
      ]
  show "cf_smcf (cf_const 𝔅  a DGHM 𝔉) = cf_smcf (cf_const 𝔄  a)"
    by (cs_prems cs_shallow cs_simp: slicing_simps slicing_commute)
qed simp_all

lemma (in is_functor) cf_comp_cf_const_left'[cat_cs_simps]:
  assumes "category α " 
    and "a  Obj"
    and "f = CIda"
  shows "dghm_const 𝔅  a f CF 𝔉 = cf_const 𝔄  a"
  using assms(1,2) unfolding assms(3) by (rule cf_comp_cf_const_left)

lemmas [cat_cs_simps] = is_functor.cf_comp_cf_const_left'



subsection‹Faithful functor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in cite"mac_lane_categories_2010").›

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

syntax "_is_ft_functor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦C.faithfulı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦C.faithfulα𝔅"  "CONST is_ft_functor α 𝔄 𝔅 𝔉"

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

lemmas [slicing_intros] = is_ft_functor.ft_cf_is_ft_functor'


text‹Rules.›

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

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

lemmas [cf_cs_intros] = is_ft_functorD(1)

lemma is_ft_functorI':
  assumes "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   v11 (𝔉ArrMap l Hom 𝔄 a b)"
  shows "𝔉 : 𝔄 ↦↦C.faithfulα𝔅"
  using assms
  by (intro is_ft_functorI)
    (
      simp_all add: 
        assms(1) 
        is_ft_semifunctorI'[OF is_functorD(6)[
          OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_ft_functorD':
  assumes "𝔉 : 𝔄 ↦↦C.faithfulα𝔅"
  shows "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   v11 (𝔉ArrMap l Hom 𝔄 a b)"
  by 
    (
      simp_all add: 
        is_ft_functorD[OF assms(1)] 
        is_ft_semifunctorD'(2)[
          OF is_ft_functorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_ft_functorE':
  assumes "𝔉 : 𝔄 ↦↦C.faithfulα𝔅"
  obtains "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   v11 (𝔉ArrMap l Hom 𝔄 a b)"
  using assms by (simp_all add: is_ft_functorD')

lemma is_ft_functorI'':
  assumes "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b g f.
       g : a 𝔄b; f : a 𝔄b; 𝔉ArrMapg = 𝔉ArrMapf   g = f"
  shows "𝔉 : 𝔄 ↦↦C.faithfulα𝔅"
  by 
    (
      intro is_ft_functorI assms,
      rule is_ft_semifunctorI'', 
      unfold slicing_simps, 
      rule is_functor.cf_is_semifunctor[OF assms(1)], 
      rule assms(2)
    )


text‹Elementary properties.›

context is_ft_functor
begin

interpretation smcf: is_ft_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
  by (rule ft_cf_is_ft_semifunctor) 

lemmas_with [unfolded slicing_simps]:
  ft_cf_v11_on_Hom = smcf.ft_smcf_v11_on_Hom
  and ft_cf_ArrMap_eqD = smcf.ft_smcf_ArrMap_eqD

end


subsubsection‹Opposite faithful functor.›

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

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

lemmas is_ft_functor_op[cat_op_intros] = is_ft_functor.is_ft_functor_op'


subsubsection‹The composition of faithful functors is a faithful functor›

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



subsection‹Full functor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in cite"mac_lane_categories_2010").›

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

syntax "_is_fl_functor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦C.fullı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦C.fullα𝔅"  "CONST is_fl_functor α 𝔄 𝔅 𝔉"

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

lemmas [slicing_intros] = is_fl_functor.fl_cf_is_fl_semifunctor


text‹Rules.›

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

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

lemmas [cf_cs_intros] = is_fl_functorD(1)

lemma is_fl_functorI':
  assumes "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj  
    𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  shows "𝔉 : 𝔄 ↦↦C.fullα𝔅"
  using assms
  by (intro is_fl_functorI)
    (
      simp_all add: 
        assms(1) 
        is_fl_semifunctorI'[
          OF is_functorD(6)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_fl_functorD':
  assumes "𝔉 : 𝔄 ↦↦C.fullα𝔅"
  shows "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj  
    𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  by 
    (
      simp_all add: 
        is_fl_functorD[OF assms(1)] 
        is_fl_semifunctorD'(2)[
          OF is_fl_functorD(2)[OF assms(1)], unfolded slicing_simps
          ]
    )

lemma is_fl_functorE':
  assumes "𝔉 : 𝔄 ↦↦C.fullα𝔅"
  obtains "𝔉 : 𝔄 ↦↦Cα𝔅"
    and "a b.  a  𝔄Obj; b  𝔄Obj   
    𝔉ArrMap ` (Hom 𝔄 a b) = Hom 𝔅 (𝔉ObjMapa) (𝔉ObjMapb)"
  using assms by (simp_all add: is_fl_functorD')


text‹Elementary properties.›

context is_fl_functor
begin

interpretation smcf: is_fl_semifunctor α cat_smc 𝔄 cat_smc 𝔅 cf_smcf 𝔉
  by (rule fl_cf_is_fl_semifunctor) 

lemmas_with [unfolded slicing_simps]:
  fl_cf_surj_on_Hom = smcf.fl_smcf_surj_on_Hom

end


subsubsection‹Opposite full functor›

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

lemmas is_fl_functor_op[cat_op_intros] = is_fl_functor.is_fl_functor_op


subsubsection‹The composition of full functor is a full functor›

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



subsection‹Fully faithful functor›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-3 in cite"mac_lane_categories_2010").›

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

syntax "_is_ff_functor" :: "V  V  V  V  bool"
  ((_ :/ _ ↦↦C.ffı _) [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦C.ffα𝔅"  "CONST is_ff_functor α 𝔄 𝔅 𝔉"


text‹Rules.›

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

lemmas [cf_cs_intros] = is_ff_functorD


text‹Elementary properties.›

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

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

lemmas [slicing_intros] = is_ff_functor.ff_cf_is_ff_semifunctor'


subsubsection‹Opposite fully faithful functor›

lemma (in