Theory CZH_ECAT_Yoneda

(* Copyright 2021 (C) Mihails Milehins *)

section‹Yoneda Lemma›
theory CZH_ECAT_Yoneda
  imports 
    CZH_ECAT_FUNCT
    CZH_ECAT_Hom
begin



subsection‹Yoneda map›


text‹
The Yoneda map is the bijection that is used in the statement of the
Yoneda Lemma, as presented, for example, in Chapter III-2 in 
cite"mac_lane_categories_2010" or in subsection 1.15 
in cite"bodo_categories_1970".
›

definition Yoneda_map :: "V  V  V  V"
  where "Yoneda_map α 𝔎 r =
    (
      λψthese_ntcfs α (𝔎HomDom) (cat_Set α) HomO.Cα𝔎HomDom(r,-) 𝔎.
        ψNTMaprArrVal𝔎HomDomCIdr
    )"


text‹Elementary properties.›

mk_VLambda Yoneda_map_def
  |vsv Yoneda_map_vsv[cat_cs_intros]|

mk_VLambda (in is_functor) Yoneda_map_def[where α=α and 𝔎=𝔉, unfolded cf_HomDom]
  |vdomain Yoneda_map_vdomain|
  |app Yoneda_map_app[unfolded these_ntcfs_iff]|

lemmas [cat_cs_simps] = is_functor.Yoneda_map_vdomain

lemmas Yoneda_map_app[cat_cs_simps] = 
  is_functor.Yoneda_map_app[unfolded these_ntcfs_iff]



subsection‹Yoneda component›


subsubsection‹Definition and elementary properties›


text‹
The Yoneda components are the components of the natural transformations
that appear in the statement of the Yoneda Lemma (e.g., see 
Chapter III-2 in cite"mac_lane_categories_2010" or subsection 1.15 
in cite"bodo_categories_1970").
›

definition Yoneda_component :: "V  V  V  V  V"
  where "Yoneda_component 𝔎 r u d =
    [
      (λfHom (𝔎HomDom) r d. 𝔎ArrMapfArrValu),
      Hom (𝔎HomDom) r d,
      𝔎ObjMapd
    ]"


text‹Components.›

lemma (in is_functor) Yoneda_component_components: 
  shows "Yoneda_component 𝔉 r u dArrVal =
    (λfHom 𝔄 r d. 𝔉ArrMapfArrValu)"
    and "Yoneda_component 𝔉 r u dArrDom = Hom 𝔄 r d"
    and "Yoneda_component 𝔉 r u dArrCod = 𝔉ObjMapd"
  unfolding Yoneda_component_def arr_field_simps 
  by (simp_all add: nat_omega_simps cat_cs_simps)


subsubsection‹Arrow value›

mk_VLambda (in is_functor) Yoneda_component_components(1)
  |vsv Yoneda_component_ArrVal_vsv|
  |vdomain Yoneda_component_ArrVal_vdomain|
  |app Yoneda_component_ArrVal_app[unfolded in_Hom_iff]|

lemmas [cat_cs_simps] = is_functor.Yoneda_component_ArrVal_vdomain

lemmas Yoneda_component_ArrVal_app[cat_cs_simps] = 
  is_functor.Yoneda_component_ArrVal_app[unfolded in_Hom_iff]


subsubsection‹Yoneda component is an arrow in the category Set›

lemma (in category) cat_Yoneda_component_is_arr:
  assumes "𝔎 :  ↦↦Cαcat_Set α"
    and "r  Obj"
    and "u  𝔎ObjMapr"
    and "d  Obj"
  shows "Yoneda_component 𝔎 r u d : Hom  r d cat_Set α𝔎ObjMapd"   
proof-
  interpret 𝔎: is_functor α  cat_Set α 𝔎 by (rule assms(1)) 
  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI, unfold 𝔎.Yoneda_component_components)
    show "vfsequence (Yoneda_component 𝔎 r u d)" 
      unfolding Yoneda_component_def by simp
    show "vcard (Yoneda_component 𝔎 r u d) = 3"
      unfolding Yoneda_component_def by (simp add: nat_omega_simps)
    show " (λfHom  r d. 𝔎ArrMapfArrValu)  𝔎ObjMapd"
    proof(rule vrange_VLambda_vsubset)
      fix f assume "f  Hom  r d"
      then have 𝔎f: "𝔎ArrMapf : 𝔎ObjMapr cat_Set α𝔎ObjMapd" 
        by (auto simp: cat_cs_intros)
      note 𝔎f_simps = cat_Set_is_arrD[OF 𝔎f]
      interpret 𝔎f: arr_Set α 𝔎ArrMapf by (rule 𝔎f_simps(1))          
      have "u  𝒟 (𝔎ArrMapfArrVal)" 
        by (simp add: 𝔎f_simps assms cat_Set_cs_simps)
      with 𝔎f.arr_Set_ArrVal_vrange[unfolded 𝔎f_simps] show 
        "𝔎ArrMapfArrValu  𝔎ObjMapd"
        by (blast elim: 𝔎f.ArrVal.vsv_value)
    qed 
    from assms 𝔎.HomCod.cat_Obj_vsubset_Vset show "𝔎ObjMapd  Vset α"
      by (auto dest: 𝔎.cf_ObjMap_app_in_HomCod_Obj)
  qed (auto simp: assms cat_cs_intros)
qed

lemma (in category) cat_Yoneda_component_is_arr':
  assumes "𝔎 :  ↦↦Cαcat_Set α" 
    and "r  Obj"
    and "u  𝔎ObjMapr"
    and "d  Obj"
    and "s = Hom  r d"
    and "t = 𝔎ObjMapd"
    and "𝔇 = cat_Set α"
  shows "Yoneda_component 𝔎 r u d : s 𝔇t"   
  unfolding assms(5-7) using assms(1-4) by (rule cat_Yoneda_component_is_arr)

lemmas [cat_cs_intros] = category.cat_Yoneda_component_is_arr'[rotated 1]



subsection‹Yoneda arrow›


subsubsection‹Definition and elementary properties›


text‹
The Yoneda arrows are the natural transformations that 
appear in the statement of the Yoneda Lemma in Chapter III-2 in 
cite"mac_lane_categories_2010" and subsection 1.15 
in cite"bodo_categories_1970".
›

definition Yoneda_arrow :: "V  V  V  V  V" 
  where "Yoneda_arrow α 𝔎 r u =
    [
      (λd𝔎HomDomObj. Yoneda_component 𝔎 r u d),
      HomO.Cα𝔎HomDom(r,-),
      𝔎,
      𝔎HomDom,
      cat_Set α
    ]"


text‹Components.›

lemma (in is_functor) Yoneda_arrow_components:
  shows "Yoneda_arrow α 𝔉 r uNTMap = 
    (λd𝔄Obj. Yoneda_component 𝔉 r u d)"
    and "Yoneda_arrow α 𝔉 r uNTDom = HomO.Cα𝔄(r,-)"
    and "Yoneda_arrow α 𝔉 r uNTCod = 𝔉"
    and "Yoneda_arrow α 𝔉 r uNTDGDom = 𝔄"
    and "Yoneda_arrow α 𝔉 r uNTDGCod = cat_Set α"
  unfolding Yoneda_arrow_def nt_field_simps 
  by (simp_all add: nat_omega_simps cat_cs_simps)


subsubsection‹Natural transformation map›

mk_VLambda (in is_functor) Yoneda_arrow_components(1)
  |vsv Yoneda_arrow_NTMap_vsv|
  |vdomain Yoneda_arrow_NTMap_vdomain|
  |app Yoneda_arrow_NTMap_app|

lemmas [cat_cs_simps] = is_functor.Yoneda_arrow_NTMap_vdomain

lemmas Yoneda_arrow_NTMap_app[cat_cs_simps] = 
  is_functor.Yoneda_arrow_NTMap_app


subsubsection‹Yoneda arrow is a natural transformation›

lemma (in category) cat_Yoneda_arrow_is_ntcf:
  assumes "𝔎 :  ↦↦Cαcat_Set α" 
    and "r  Obj" 
    and "u  𝔎ObjMapr"
  shows "Yoneda_arrow α 𝔎 r u : HomO.Cα(r,-) CF 𝔎 :  ↦↦Cαcat_Set α"
proof-

  interpret 𝔎: is_functor α  cat_Set α 𝔎 by (rule assms(1)) 
  note 𝔎ru = cat_Yoneda_component_is_arr[OF assms]
  let ?𝔎ru = Yoneda_component 𝔎 r u

  show ?thesis
  proof(intro is_ntcfI', unfold 𝔎.Yoneda_arrow_components)

    show "vfsequence (Yoneda_arrow α 𝔎 r u)"
      unfolding Yoneda_arrow_def by simp
    show "vcard (Yoneda_arrow α 𝔎 r u) = 5" 
      unfolding Yoneda_arrow_def by (simp add: nat_omega_simps)

    show
      "(λdObj. ?𝔎ru d)a :
        HomO.Cα(r,-)ObjMapa cat_Set α𝔎ObjMapa"
      if "a  Obj" for a
      using that assms category_axioms
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_op_simps V_cs_simps 
            cs_intro: cat_cs_intros
        )
    show 
      "(λdObj. ?𝔎ru d)b Acat_Set αHomO.Cα(r,-)ArrMapf =
        𝔎ArrMapf Acat_Set α(λdObj. ?𝔎ru d)a"
      if "f : a b" for a b f
    proof-

      note 𝔐a = 𝔎ru[OF cat_is_arrD(2)[OF that]]
      note 𝔐b = 𝔎ru[OF cat_is_arrD(3)[OF that]]

      from category_axioms assms that 𝔐b have b_f:
        "?𝔎ru b Acat_Set αcf_hom  [CIdr, f] :
          Hom  r a cat_Set α𝔎ObjMapb"
        by
          (
            cs_concl cs_shallow 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
      then have dom_lhs: 
        "𝒟 ((?𝔎ru b Acat_Set αcf_hom  [CIdr, f])ArrVal) =
          Hom  r a"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      from assms that 𝔐a have f_a: 
        "𝔎ArrMapf Acat_Set α?𝔎ru a :
          Hom  r a cat_Set α𝔎ObjMapb"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      then have dom_rhs: 
        "𝒟 ((𝔎ArrMapf Acat_Set α?𝔎ru a)ArrVal) = Hom  r a"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)

      have [cat_cs_simps]:
        "?𝔎ru b Acat_Set αcf_hom  [CIdr, f] =
          𝔎ArrMapf Acat_Set α?𝔎ru a"
      proof(rule arr_Set_eqI[of α])

        from b_f show arr_Set_b_f:
          "arr_Set α (?𝔎ru b Acat_Set αcf_hom  [CIdr, f])"
          by (auto simp: cat_Set_is_arrD(1))
        interpret b_f: arr_Set α ?𝔎ru b Acat_Set αcf_hom  [CIdr, f]
          by (rule arr_Set_b_f)
        from f_a show arr_Set_f_a:
          "arr_Set α (𝔎ArrMapf Acat_Set α?𝔎ru a)"
          by (auto simp: cat_Set_is_arrD(1))
        interpret f_a: arr_Set α 𝔎ArrMapf Acat_Set α?𝔎ru a
          by (rule arr_Set_f_a)

        show 
          "(?𝔎ru b Acat_Set αcf_hom  [CIdr, f])ArrVal =
            (𝔎ArrMapf Acat_Set α?𝔎ru a)ArrVal"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
          fix q assume "q : r a"
          from category_axioms assms that this 𝔐a 𝔐b show 
            "(?𝔎ru b Acat_Set αcf_hom  [CIdr, f])ArrValq =
              (𝔎ArrMapf Acat_Set α?𝔎ru a)ArrValq"
            by
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps cat_op_simps
                  cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
              )
        qed (use arr_Set_b_f arr_Set_f_a in auto)

      qed (use b_f f_a in cs_concl cs_shallow cs_simp: cat_cs_simps)+
  
      from that category_axioms assms 𝔐a 𝔐b show ?thesis
        by
          (
            cs_concl 
              cs_simp: V_cs_simps cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros
          )
    
    qed

  qed (auto simp: assms(2) cat_cs_intros)

qed



subsection‹Yoneda Lemma›

text‹
The following lemma is approximately equivalent to the Yoneda Lemma 
stated in subsection 1.15 in cite"bodo_categories_1970" 
(the first two conclusions correspond to the statement of the 
Yoneda lemma in Chapter III-2 in cite"mac_lane_categories_2010").
›

lemma (in category) cat_Yoneda_Lemma: 
  assumes "𝔎 :  ↦↦Cαcat_Set α" and "r  Obj"
  shows "v11 (Yoneda_map α 𝔎 r)" 
    and " (Yoneda_map α 𝔎 r) = 𝔎ObjMapr"
    and "(Yoneda_map α 𝔎 r)¯ = (λu𝔎ObjMapr. Yoneda_arrow α 𝔎 r u)"
proof-

  interpret 𝔎: is_functor α  cat_Set α 𝔎 by (rule assms(1)) 

  from assms(2) 𝔎.HomCod.cat_Obj_vsubset_Vset 𝔎.cf_ObjMap_app_in_HomCod_Obj 
  have 𝔎r_in_Vset: "𝔎ObjMapr  Vset α"
    by auto

  show Ym: "v11 (Yoneda_map α 𝔎 r)"
  proof(intro vsv.vsv_valeq_v11I, unfold 𝔎.Yoneda_map_vdomain these_ntcfs_iff)

    fix 𝔐 𝔑
    assume prems: 
      "𝔐 : HomO.Cα(r,-) CF 𝔎 :  ↦↦Cαcat_Set α"
      "𝔑 : HomO.Cα(r,-) CF 𝔎 :  ↦↦Cαcat_Set α"
      "Yoneda_map α 𝔎 r𝔐 = Yoneda_map α 𝔎 r𝔑"
    from prems(3) have 𝔐r_𝔑r:
      "𝔐NTMaprArrValCIdr = 𝔑NTMaprArrValCIdr"
      unfolding 
        Yoneda_map_app[OF assms(1) prems(1)] 
        Yoneda_map_app[OF assms(1) prems(2)]
      by simp

    interpret 𝔐: is_ntcf α  cat_Set α HomO.Cα(r,-) 𝔎 𝔐  
      by (rule prems(1))
    interpret 𝔑: is_ntcf α  cat_Set α HomO.Cα(r,-) 𝔎 𝔑 
      by (rule prems(2))

    show "𝔐 = 𝔑"
    proof
      (
        rule ntcf_eqI[OF prems(1,2)]; 
        (rule refl)?;
        rule vsv_eqI, 
        unfold 𝔐.ntcf_NTMap_vdomain 𝔑.ntcf_NTMap_vdomain
      )

      fix d assume prems': "d  Obj"

      note 𝔐d_simps = cat_Set_is_arrD[OF 𝔐.ntcf_NTMap_is_arr[OF prems']]
      interpret 𝔐d: arr_Set α 𝔐NTMapd by (rule 𝔐d_simps(1))

      note 𝔑d_simps = cat_Set_is_arrD[OF 𝔑.ntcf_NTMap_is_arr[OF prems']]
      interpret 𝔑d: arr_Set α 𝔑NTMapd by (rule 𝔑d_simps(1))

      show "𝔐NTMapd = 𝔑NTMapd"
      proof(rule arr_Set_eqI[of α])
        show "𝔐NTMapdArrVal = 𝔑NTMapdArrVal"
        proof
          (
            rule vsv_eqI, 
            unfold 
              𝔑d.arr_Set_ArrVal_vdomain 
              𝔐d.arr_Set_ArrVal_vdomain  
              𝔐d_simps
              𝔑d_simps
          )
          fix f assume prems'': "f  HomO.Cα(r,-)ObjMapd"
          from prems'' prems' category_axioms assms(2) have f: "f : r d"
            by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_op_intros)
          from 𝔐.ntcf_Comp_commute[OF f] have 
            "(
              𝔐NTMapd Acat_Set αHomO.Cα(r,-)ArrMapf
            )ArrValCIdr =
              (𝔎ArrMapf Acat_Set α𝔐NTMapr)ArrValCIdr"
            by simp
          from this category_axioms assms(2) f prems prems' have 𝔐df:
            "𝔐NTMapdArrValf =
              𝔎ArrMapfArrVal𝔐NTMaprArrValCIdr"
            by 
              (
                cs_prems cs_shallow
                  cs_simp: cat_cs_simps cat_op_simps 
                  cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
              )
          from 𝔑.ntcf_Comp_commute[OF f] have
            "(
              𝔑NTMapd Acat_Set αHomO.Cα(r,-)ArrMapf
            )ArrValCIdr = 
              (𝔎ArrMapf Acat_Set α𝔑NTMapr)ArrValCIdr"
            by simp
          from this category_axioms assms(2) f prems prems' have 𝔑df:
            "𝔑NTMapdArrValf =
              𝔎ArrMapfArrVal𝔑NTMaprArrValCIdr"
            by
              (
                cs_prems cs_shallow
                  cs_simp: cat_cs_simps cat_op_simps 
                  cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
              )
          show "𝔐NTMapdArrValf = 𝔑NTMapdArrValf"
            unfolding 𝔐df 𝔑df 𝔐r_𝔑r by simp
        qed auto

      qed (simp_all add: 𝔐d_simps 𝔑d_simps)

    qed auto

  qed (auto simp: Yoneda_map_vsv)

  interpret Ym: v11 Yoneda_map α 𝔎 r by (rule Ym)

  have YY: "Yoneda_map α 𝔎 rYoneda_arrow α 𝔎 r a = a" 
    if "a  𝔎ObjMapr" for a
  proof-
    note cat_Yoneda_arrow_is_ntcf[OF assms that]
    moreover with assms have Ya: "Yoneda_arrow α 𝔎 r a  𝒟 (Yoneda_map α 𝔎 r)" 
      by 
        (
          cs_concl cs_shallow 
            cs_simp: these_ntcfs_iff cat_cs_simps cs_intro: cat_cs_intros
        )
    ultimately show "Yoneda_map α 𝔎 rYoneda_arrow α 𝔎 r a = a"
      using assms that 𝔎r_in_Vset
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed        

  show [simp]: " (Yoneda_map α 𝔎 r) = 𝔎ObjMapr"
  proof(intro vsubset_antisym)

    show " (Yoneda_map α 𝔎 r)  𝔎ObjMapr"
      unfolding Yoneda_map_def
    proof(intro vrange_VLambda_vsubset, unfold these_ntcfs_iff 𝔎.cf_HomDom)
      fix 𝔐 assume prems: "𝔐 : HomO.Cα(r,-) CF 𝔎 :  ↦↦Cαcat_Set α"
      then interpret 𝔐: is_ntcf α  cat_Set α HomO.Cα(r,-) 𝔎 𝔐 .
      note 𝔐r_simps = cat_Set_is_arrD[OF 𝔐.ntcf_NTMap_is_arr[OF assms(2)]]
      interpret 𝔐r: arr_Set α 𝔐NTMapr by (rule 𝔐r_simps(1))
      from prems category_axioms assms(2) have 
        "CIdr  𝒟 (𝔐NTMaprArrVal)"
        unfolding 𝔐r.arr_Set_ArrVal_vdomain 𝔐r_simps
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
          )
      then have "𝔐NTMaprArrValCIdr   (𝔐NTMaprArrVal)"
        by (blast elim: 𝔐r.ArrVal.vsv_value)
      then show "𝔐NTMaprArrValCIdr  𝔎ObjMapr"
        by (auto simp: 𝔐r_simps dest!: vsubsetD[OF 𝔐r.arr_Set_ArrVal_vrange])
    qed
    
    show "𝔎ObjMapr   (Yoneda_map α 𝔎 r)"
    proof(intro vsubsetI)
      fix u assume prems: "u  𝔎ObjMapr"
      from cat_Yoneda_arrow_is_ntcf[OF assms prems] have 
        "Yoneda_arrow α 𝔎 r u  𝒟 (Yoneda_map α 𝔎 r)" 
        by 
          (
            cs_concl cs_shallow 
              cs_simp: these_ntcfs_iff cat_cs_simps cs_intro: cat_cs_intros
          )
      with YY[OF prems] show "u   (Yoneda_map α 𝔎 r)" 
        by (force dest!: vdomain_atD)
    qed

  qed

  show "(Yoneda_map α 𝔎 r)¯ = (λu𝔎ObjMapr. Yoneda_arrow α 𝔎 r u)"
  proof(rule vsv_eqI, unfold vdomain_vconverse vdomain_VLambda)
    from Ym show "vsv ((Yoneda_map α 𝔎 r)¯)" by auto
    show "(Yoneda_map α 𝔎 r)¯a = (λu𝔎ObjMapr. Yoneda_arrow α 𝔎 r u)a"
      if "a   (Yoneda_map α 𝔎 r)" for a
    proof-
      from that have a: "a  𝔎ObjMapr" by simp
      note Ya = cat_Yoneda_arrow_is_ntcf[OF assms a]
      then have "Yoneda_arrow α 𝔎 r a  𝒟 (Yoneda_map α 𝔎 r)"
        by 
          (
            cs_concl cs_shallow
              cs_simp: these_ntcfs_iff cat_cs_simps cs_intro: cat_cs_intros
          )
      with Ya YY[OF a] a show ?thesis
        by 
          (
            intro Ym.v11_vconverse_app[
              unfolded 𝔎.Yoneda_map_vdomain these_ntcfs_iff
              ]
          )
          (simp_all add: these_ntcfs_iff cat_cs_simps)
    qed
  qed auto

qed



subsection‹Inverse of the Yoneda map›

lemma (in category) inv_Yoneda_map_v11: 
  assumes "𝔎 :  ↦↦Cαcat_Set α" and "r  Obj"
  shows "v11 ((Yoneda_map α 𝔎 r)¯)"
  using cat_Yoneda_Lemma(1)[OF assms] by (simp add: v11.v11_vconverse)

lemma (in category) inv_Yoneda_map_vdomain: 
  assumes "𝔎 :  ↦↦Cαcat_Set α" and "r  Obj"
  shows "𝒟 ((Yoneda_map α 𝔎 r)¯) = 𝔎ObjMapr"
  unfolding cat_Yoneda_Lemma(3)[OF assms] by simp

lemmas [cat_cs_simps] = category.inv_Yoneda_map_vdomain

lemma (in category) inv_Yoneda_map_app: 
  assumes "𝔎 :  ↦↦Cαcat_Set α" and "r  Obj" and "u  𝔎ObjMapr"
  shows "(Yoneda_map α 𝔎 r)¯u = Yoneda_arrow α 𝔎 r u"
  using assms(3) unfolding cat_Yoneda_Lemma(3)[OF assms(1,2)] by simp

lemmas [cat_cs_simps] = category.inv_Yoneda_map_app

lemma (in category) inv_Yoneda_map_vrange: 
  assumes "𝔎 :  ↦↦Cαcat_Set α"
  shows " ((Yoneda_map α 𝔎 r)¯) =
    these_ntcfs α  (cat_Set α) HomO.Cα(r,-) 𝔎"
proof-
  interpret 𝔎: is_functor α  cat_Set α 𝔎 by (rule assms(1)) 
  show ?thesis unfolding Yoneda_map_def by (simp add: cat_cs_simps)
qed



subsection‹
Component of a composition of a Hom›-natural transformation 
with natural transformations
›


subsubsection‹Definition and elementary properties›


text‹
The following definition is merely a technical generalization
that is used in the context of the description of the 
composition of a Hom›-natural transformation with a natural transformation
later in this section
(also see subsection 1.15 in cite"bodo_categories_1970").
›

definition ntcf_Hom_component :: "V  V  V  V  V"
  where "ntcf_Hom_component φ ψ a b =
    [
      (
        λfHom (φNTDGCod) (φNTCodObjMapa) (ψNTDomObjMapb).
          ψNTMapb AψNTDGCodf AψNTDGCodφNTMapa
      ),
      Hom (φNTDGCod) (φNTCodObjMapa) (ψNTDomObjMapb),
      Hom (φNTDGCod) (φNTDomObjMapa) (ψNTCodObjMapb)
    ]"


text‹Components.›

lemma ntcf_Hom_component_components: 
  shows "ntcf_Hom_component φ ψ a bArrVal =
    (
      λfHom (φNTDGCod) (φNTCodObjMapa) (ψNTDomObjMapb).
        ψNTMapb AψNTDGCodf AψNTDGCodφNTMapa
    )"
    and "ntcf_Hom_component φ ψ a bArrDom =
      Hom (φNTDGCod) (φNTCodObjMapa) (ψNTDomObjMapb)"
    and "ntcf_Hom_component φ ψ a bArrCod =
      Hom (φNTDGCod) (φNTDomObjMapa) (ψNTCodObjMapb)"
  unfolding ntcf_Hom_component_def arr_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda ntcf_Hom_component_components(1)
  |vsv ntcf_Hom_component_ArrVal_vsv[intro]|

context
  fixes α φ ψ 𝔉 𝔊 𝔉' 𝔊' 𝔄 𝔅 
  assumes φ: "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and ψ: "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
begin

interpretation φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule φ)
interpretation ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule ψ)

mk_VLambda 
  ntcf_Hom_component_components(1)
    [
      of φ ψ, 
      unfolded 
        φ.ntcf_NTDom ψ.ntcf_NTDom 
        φ.ntcf_NTCod ψ.ntcf_NTCod 
        φ.ntcf_NTDGDom ψ.ntcf_NTDGDom
        φ.ntcf_NTDGCod ψ.ntcf_NTDGCod
    ]
  |vdomain ntcf_Hom_component_ArrVal_vdomain|
  |app ntcf_Hom_component_ArrVal_app[unfolded in_Hom_iff]|

lemmas [cat_cs_simps] = 
  ntcf_Hom_component_ArrVal_vdomain
  ntcf_Hom_component_ArrVal_app

lemma ntcf_Hom_component_ArrVal_vrange:
  assumes "a  𝔄Obj" and "b  𝔅Obj"
  shows 
    " (ntcf_Hom_component φ ψ a bArrVal) 
      Hom  (𝔉ObjMapa) (𝔊'ObjMapb)"
proof
  (
    rule vsv.vsv_vrange_vsubset, 
    unfold ntcf_Hom_component_ArrVal_vdomain in_Hom_iff
  )
  fix f assume "f : 𝔊ObjMapa 𝔉'ObjMapb"
  with assms φ ψ show 
    "ntcf_Hom_component φ ψ a bArrValf : 𝔉ObjMapa 𝔊'ObjMapb"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed (rule ntcf_Hom_component_ArrVal_vsv)

end


subsubsection‹Arrow domain and codomain›

context
  fixes α φ ψ 𝔉 𝔊 𝔉' 𝔊' 𝔄 𝔅 
  assumes φ: "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and ψ: "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
begin

interpretation φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule φ)
interpretation ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule ψ)

lemma ntcf_Hom_component_ArrDom[cat_cs_simps]:
  "ntcf_Hom_component φ ψ a bArrDom = Hom  (𝔊ObjMapa) (𝔉'ObjMapb)"
  unfolding ntcf_Hom_component_components by (simp add: cat_cs_simps)

lemma ntcf_Hom_component_ArrCod[cat_cs_simps]:
  "ntcf_Hom_component φ ψ a bArrCod = Hom  (𝔉ObjMapa) (𝔊'ObjMapb)"
  unfolding ntcf_Hom_component_components by (simp add: cat_cs_simps)

end


subsubsection‹
Component of a composition of a Hom›-natural transformation 
with natural transformations is an arrow in the category Set›

lemma (in category) cat_ntcf_Hom_component_is_arr:
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
    and "a  op_cat 𝔄Obj"
    and "b  𝔅Obj"
  shows 
    "ntcf_Hom_component φ ψ a b :
      Hom  (𝔊ObjMapa) (𝔉'ObjMapb) cat_Set αHom  (𝔉ObjMapa) (𝔊'ObjMapb)"
proof-
  
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  interpret ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule assms(2))

  from assms have a: "a  𝔄Obj" unfolding cat_op_simps by simp

  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI)
    show "vfsequence (ntcf_Hom_component φ ψ a b)"
      unfolding ntcf_Hom_component_def by (simp add: nat_omega_simps)
    show "vcard (ntcf_Hom_component φ ψ a b) = 3"
      unfolding ntcf_Hom_component_def by (simp add: nat_omega_simps)
    from assms ntcf_Hom_component_ArrVal_vrange[OF assms(1,2) a assms(4)] show 
      " (ntcf_Hom_component φ ψ a bArrVal)  
        ntcf_Hom_component φ ψ a bArrCod"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    from assms(1,2,4) a show "ntcf_Hom_component φ ψ a bArrDom  Vset α"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(1,2,4) a show "ntcf_Hom_component φ ψ a bArrCod  Vset α"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed (use assms in auto simp: ntcf_Hom_component_components cat_cs_simps)

qed

lemma (in category) cat_ntcf_Hom_component_is_arr':
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
    and "a  op_cat 𝔄Obj"
    and "b  𝔅Obj"
    and "𝔄' = Hom  (𝔊ObjMapa) (𝔉'ObjMapb)"
    and "𝔅' = Hom  (𝔉ObjMapa) (𝔊'ObjMapb)"
    and "ℭ' = cat_Set α"
  shows "ntcf_Hom_component φ ψ a b : 𝔄' ℭ'𝔅'"
  using assms(1-4) unfolding assms(5-7) by (rule cat_ntcf_Hom_component_is_arr)
  
lemmas [cat_cs_intros] = category.cat_ntcf_Hom_component_is_arr'


subsubsection‹
Naturality of the components of a composition of 
a Hom›-natural transformation with natural transformations
›

lemma (in category) cat_ntcf_Hom_component_nat:
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
    and "g : a op_cat 𝔄a'"
    and "f : b 𝔅b'" 
  shows
    "ntcf_Hom_component φ ψ a' b' Acat_Set αcf_hom  [𝔊ArrMapg, 𝔉'ArrMapf] =
      cf_hom  [𝔉ArrMapg, 𝔊'ArrMapf] Acat_Set αntcf_Hom_component φ ψ a b"
proof-

  let ?Y_ab = ntcf_Hom_component φ ψ a b
    and ?Y_a'b' = ntcf_Hom_component φ ψ a' b'
    and ?𝔊g = 𝔊ArrMapg
    and ?𝔉'f = 𝔉'ArrMapf
    and ?𝔉g = 𝔉ArrMapg
    and ?𝔊'f = 𝔊'ArrMapf
    and ?𝔊a = 𝔊ObjMapa
    and ?𝔉'b = 𝔉'ObjMapb
    and ?𝔉a' = 𝔉ObjMapa'
    and ?𝔊'b' = 𝔊'ObjMapb'

  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  interpret ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule assms(2))
  interpret Set: category α cat_Set α by (rule category_cat_Set)

  from assms(3) have g: "g : a' 𝔄a" unfolding cat_op_simps by simp

  from Set.category_axioms category_axioms assms g have a'b_Gg𝔉'f:
    "?Y_a'b' Acat_Set αcf_hom  [?𝔊g, ?𝔉'f] :
      Hom  ?𝔊a ?𝔉'b cat_Set αHom  ?𝔉a' ?𝔊'b'"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
  then have dom_lhs: 
    "𝒟 ((?Y_a'b' Acat_Set αcf_hom  [?𝔊g, ?𝔉'f])ArrVal) = 
      Hom  ?𝔊a ?𝔉'b"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from Set.category_axioms category_axioms assms g have 𝔉g𝔊'f_ab: 
    "cf_hom  [?𝔉g, ?𝔊'f] Acat_Set α?Y_ab : 
      Hom  ?𝔊a ?𝔉'b cat_Set αHom  ?𝔉a' ?𝔊'b'"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
  then have dom_rhs: 
    "𝒟 ((cf_hom  [?𝔉g, ?𝔊'f] Acat_Set α?Y_ab)ArrVal) =
      Hom  ?𝔊a ?𝔉'b"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    from a'b_Gg𝔉'f show arr_Set_a'b_Gg𝔉'f:
      "arr_Set α (?Y_a'b' Acat_Set αcf_hom  [?𝔊g, ?𝔉'f])"
      by (auto dest: cat_Set_is_arrD(1))
    from 𝔉g𝔊'f_ab show arr_Set_𝔉g𝔊'f_ab: 
      "arr_Set α (cf_hom  [?𝔉g, ?𝔊'f] Acat_Set α?Y_ab)"
      by (auto dest: cat_Set_is_arrD(1))
    show 
      "(?Y_a'b' Acat_Set αcf_hom  [?𝔊g, ?𝔉'f])ArrVal =
        (cf_hom  [?𝔉g, ?𝔊'f] Acat_Set α?Y_ab)ArrVal"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix h assume prems: "h : 𝔊ObjMapa 𝔉'ObjMapb"
      from assms(1,2) g have [cat_cs_simps]:
        "ψNTMapb' A(?𝔉'f A(h A(?𝔊g AφNTMapa'))) =
          ψNTMapb' A(?𝔉'f A(h A(φNTMapa A?𝔉g)))"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: is_ntcf.ntcf_Comp_commute cs_intro: cat_cs_intros
          )
      also from assms(1,2,4) prems g have " =
        (((ψNTMapb' A?𝔉'f) Ah) AφNTMapa) A?𝔉g"
        by (cs_concl cs_shallow cs_simp: cat_Comp_assoc cs_intro: cat_cs_intros) 
      also from assms(1,2,4) have " =
        (((?𝔊'f AψNTMapb) Ah) AφNTMapa) A?𝔉g"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: is_ntcf.ntcf_Comp_commute cs_intro: cat_cs_intros
          )
      also from assms(1,2,4) prems g have " =
        ?𝔊'f A(ψNTMapb A(h A(φNTMapa A?𝔉g)))"
        by (cs_concl cs_simp: cat_Comp_assoc cs_intro: cat_cs_intros) (*slow*)
      finally have nat:
        "ψNTMapb' A(?𝔉'f A(h A(?𝔊g AφNTMapa'))) =
          ?𝔊'f A(ψNTMapb A(h A(φNTMapa A?𝔉g)))".
      from prems Set.category_axioms category_axioms assms(1,2,4) g show 
        "(?Y_a'b' Acat_Set αcf_hom  [?𝔊g, ?𝔉'f])ArrValh =
          (cf_hom  [?𝔉g, ?𝔊'f] Acat_Set α?Y_ab)ArrValh"
        by (*slow*)
          (
            cs_concl 
              cs_simp: nat cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed (use arr_Set_a'b_Gg𝔉'f arr_Set_𝔉g𝔊'f_ab in auto)

  qed (use a'b_Gg𝔉'f 𝔉g𝔊'f_ab in cs_concl cs_shallow cs_simp: cat_cs_simps)+

qed


subsubsection‹
Composition of the components of a composition of a Hom›-natural 
transformation with natural transformations
›

lemma (in category) cat_ntcf_Hom_component_Comp:
  assumes "φ' : 𝔊 CF  : 𝔄 ↦↦Cα" 
    and "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "ψ' : 𝔊' CF ℌ' : 𝔅 ↦↦Cα" 
    and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
    and "a  𝔄Obj"
    and "b  𝔅Obj"
  shows 
    "ntcf_Hom_component φ ψ' a b Acat_Set αntcf_Hom_component φ' ψ a b =
      ntcf_Hom_component (φ' NTCF φ) (ψ' NTCF ψ) a b"
    (is ?φψ' Acat_Set α?φ'ψ = ?φ'φψ'ψ)
proof-

  interpret Set: category α cat_Set α by (rule category_cat_Set)

  from assms Set.category_axioms category_axioms have φψ'_φ'ψ: 
    "?φψ' Acat_Set α?φ'ψ :
      Hom  (ObjMapa) (𝔉'ObjMapb) cat_Set αHom  (𝔉ObjMapa) (ℌ'ObjMapb)"    
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  then have dom_lhs: 
    "𝒟 ((?φψ' Acat_Set α?φ'ψ)ArrVal) = 
      Hom  (ObjMapa) (𝔉'ObjMapb)"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from assms Set.category_axioms category_axioms have φ'φψ'ψ: 
    "?φ'φψ'ψ :
      Hom  (ObjMapa) (𝔉'ObjMapb) cat_Set αHom  (𝔉ObjMapa) (ℌ'ObjMapb)"    
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  then have dom_rhs: 
    "𝒟 (?φ'φψ'ψArrVal) = Hom  (ObjMapa) (𝔉'ObjMapb)" 
    by (cs_concl cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    from φψ'_φ'ψ show arr_Set_φψ'_φ'ψ: "arr_Set α (?φψ' Acat_Set α?φ'ψ)"
      by (auto dest: cat_Set_is_arrD(1))
    from φ'φψ'ψ show arr_Set_φ'φψ'ψ: "arr_Set α ?φ'φψ'ψ"
      by (auto dest: cat_Set_is_arrD(1))
    show "(?φψ' Acat_Set α?φ'ψ)ArrVal = ?φ'φψ'ψArrVal"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix f assume "f : ObjMapa 𝔉'ObjMapb"
      with category_axioms assms Set.category_axioms show 
        "(?φψ' Acat_Set α?φ'ψ)ArrValf = ?φ'φψ'ψArrValf"
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed (use arr_Set_φ'φψ'ψ arr_Set_φψ'_φ'ψ in auto)
    
  qed (use φψ'_φ'ψ φ'φψ'ψ in cs_concl cs_simp: cat_cs_simps)+

qed

lemmas [cat_cs_simps] = category.cat_ntcf_Hom_component_Comp


subsubsection‹
Component of a composition of Hom›-natural 
transformation with the identity natural transformations
›

lemma (in category) cat_ntcf_Hom_component_ntcf_id:
  assumes "𝔉 : 𝔄 ↦↦Cα" 
    and "𝔉': 𝔅 ↦↦Cα"
    and "a  𝔄Obj"
    and "b  𝔅Obj"
  shows 
    "ntcf_Hom_component (ntcf_id 𝔉) (ntcf_id 𝔉') a b =
      cat_Set αCIdHom  (𝔉ObjMapa) (𝔉'ObjMapb)"
    (is ?𝔉𝔉' = cat_Set αCId?𝔉a𝔉'b)
proof-

  interpret 𝔉: is_functor α 𝔄  𝔉 by (rule assms(1))
  interpret 𝔉': is_functor α 𝔅  𝔉' by (rule assms(2))
  interpret Set: category α cat_Set α by (rule category_cat_Set)

  from assms Set.category_axioms category_axioms have 𝔉𝔉': 
    "?𝔉𝔉' :
      Hom  (𝔉ObjMapa) (𝔉'ObjMapb) cat_Set αHom  (𝔉ObjMapa) (𝔉'ObjMapb)"    
    by (cs_concl cs_intro: cat_cs_intros cat_op_intros)
  then have dom_lhs: "𝒟 (?𝔉𝔉'ArrVal) = Hom  (𝔉ObjMapa) (𝔉'ObjMapb)"
    by (cs_concl cs_simp: cat_cs_simps)

  from category_axioms assms Set.category_axioms have 𝔉a𝔉'b: 
    "cat_Set αCId?𝔉a𝔉'b :
      Hom  (𝔉ObjMapa) (𝔉'ObjMapb) cat_Set αHom  (𝔉ObjMapa) (𝔉'ObjMapb)"
    by 
      (
        cs_concl 
          cs_simp: cat_Set_cs_simps cat_Set_components(1) 
          cs_intro: cat_cs_intros
      )
  then have dom_rhs: 
    "𝒟 (cat_Set αCId?𝔉a𝔉'bArrVal) = Hom  (𝔉ObjMapa) (𝔉'ObjMapb)"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    from 𝔉𝔉' show arr_Set_𝔉ψ: "arr_Set α ?𝔉𝔉'" 
      by (auto dest: cat_Set_is_arrD(1))
    from 𝔉a𝔉'b show arr_Set_𝔉a𝔉'b: "arr_Set α (cat_Set αCId?𝔉a𝔉'b)" 
      by (auto dest: cat_Set_is_arrD(1))
    show "?𝔉𝔉'ArrVal = cat_Set αCId?𝔉a𝔉'bArrVal"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)  
      fix f assume "f : 𝔉ObjMapa 𝔉'ObjMapb"
      with category_axioms Set.category_axioms assms show 
        "?𝔉𝔉'ArrValf = cat_Set αCId?𝔉a𝔉'bArrValf"
        by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_Set_components(1)
              cs_intro: cat_cs_intros
          )
    qed (use arr_Set_𝔉a𝔉'b in auto)
      
  qed (use 𝔉𝔉' 𝔉a𝔉'b in cs_concl cs_simp: cat_cs_simps)+

qed

lemmas [cat_cs_simps] = category.cat_ntcf_Hom_component_ntcf_id



subsection‹
Component of a composition of a Hom›-natural transformation 
with a natural transformation
›


subsubsection‹Definition and elementary properties›

definition ntcf_lcomp_Hom_component :: "V  V  V  V"
  where "ntcf_lcomp_Hom_component φ a b =
    ntcf_Hom_component φ (ntcf_id (cf_id (φNTDGCod))) a b"

definition ntcf_rcomp_Hom_component :: "V  V  V  V"
  where "ntcf_rcomp_Hom_component ψ a b =
    ntcf_Hom_component (ntcf_id (cf_id (ψNTDGCod))) ψ a b"


subsubsection‹Arrow value›

lemma ntcf_lcomp_Hom_component_ArrVal_vsv: 
  "vsv (ntcf_lcomp_Hom_component φ a bArrVal)"
  unfolding ntcf_lcomp_Hom_component_def by (rule ntcf_Hom_component_ArrVal_vsv)

lemma ntcf_rcomp_Hom_component_ArrVal_vsv: 
  "vsv (ntcf_rcomp_Hom_component ψ a bArrVal)"
  unfolding ntcf_rcomp_Hom_component_def by (rule ntcf_Hom_component_ArrVal_vsv)

lemma ntcf_lcomp_Hom_component_ArrVal_vdomain[cat_cs_simps]: 
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα" and "b  Obj"
  shows "𝒟 (ntcf_lcomp_Hom_component φ a bArrVal) = Hom  (𝔊ObjMapa) b"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  show ?thesis
    using assms
    unfolding ntcf_lcomp_Hom_component_def φ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_rcomp_Hom_component_ArrVal_vdomain[cat_cs_simps]: 
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα" and "a  op_cat Obj"
  shows "𝒟 (ntcf_rcomp_Hom_component ψ a bArrVal) = Hom  a (𝔉ObjMapb)"
proof-
  interpret ψ: is_ntcf α 𝔅  𝔉 𝔊 ψ by (rule assms(1))
  show ?thesis
    using assms
    unfolding cat_op_simps ntcf_rcomp_Hom_component_def ψ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_lcomp_Hom_component_ArrVal_app[cat_cs_simps]: 
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "a  op_cat 𝔄Obj"
    and "b  Obj"
    and "h : 𝔊ObjMapa b"
  shows "ntcf_lcomp_Hom_component φ a bArrValh = h AφNTMapa"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  show ?thesis
    using assms
    unfolding cat_op_simps ntcf_lcomp_Hom_component_def φ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_rcomp_Hom_component_ArrVal_app[cat_cs_simps]: 
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα"
    and "a  op_cat Obj"
    and "b  𝔅Obj"
    and "h : a 𝔉ObjMapb"
  shows "ntcf_rcomp_Hom_component ψ a bArrValh = ψNTMapb Ah"
proof-
  interpret ψ: is_ntcf α 𝔅  𝔉 𝔊 ψ by (rule assms(1))
  show ?thesis
    using assms
    unfolding cat_op_simps ntcf_rcomp_Hom_component_def ψ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_lcomp_Hom_component_ArrVal_vrange: 
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "a  op_cat 𝔄Obj" 
    and "b  Obj"
  shows " (ntcf_lcomp_Hom_component φ a bArrVal)  Hom  (𝔉ObjMapa) b"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  from assms(2) have a: "a  𝔄Obj" unfolding cat_op_simps by simp
  from assms(1,3) a have 
    " (ntcf_lcomp_Hom_component φ a bArrVal) 
      Hom  (𝔉ObjMapa) (cf_id ObjMapb)"
    by 
      (
        unfold cat_op_simps ntcf_lcomp_Hom_component_def φ.ntcf_NTDGCod, 
        intro ntcf_Hom_component_ArrVal_vrange
      ) 
      (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
  from this assms(3) show ?thesis by (cs_prems cs_shallow cs_simp: cat_cs_simps)
qed

lemma ntcf_rcomp_Hom_component_ArrVal_vrange: 
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα"
    and "a  op_cat Obj"
    and "b  𝔅Obj"
  shows " (ntcf_rcomp_Hom_component ψ a bArrVal)  Hom  a (𝔊ObjMapb)"
proof-
  interpret ψ: is_ntcf α 𝔅  𝔉 𝔊 ψ by (rule assms(1))
  from assms(2) have a: "a  Obj" unfolding cat_op_simps by simp
  from assms(1,3) a have 
    " (ntcf_rcomp_Hom_component ψ a bArrVal) 
      Hom  (cf_id ObjMapa) (𝔊ObjMapb)"
    by 
      (
        unfold ntcf_rcomp_Hom_component_def ψ.ntcf_NTDGCod, 
        intro ntcf_Hom_component_ArrVal_vrange
      ) 
      (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from this a show ?thesis by (cs_prems cs_shallow cs_simp: cat_cs_simps)
qed


subsubsection‹Arrow domain and codomain›

lemma ntcf_lcomp_Hom_component_ArrDom[cat_cs_simps]:
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα" and "b  Obj"
  shows "ntcf_lcomp_Hom_component φ a bArrDom = Hom  (𝔊ObjMapa) b"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  from assms show ?thesis
    unfolding ntcf_lcomp_Hom_component_def φ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_rcomp_Hom_component_ArrDom[cat_cs_simps]:
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα" and "a  op_cat Obj"
  shows "ntcf_rcomp_Hom_component ψ a bArrDom = Hom  a (𝔉ObjMapb)"
proof-
  interpret ψ: is_ntcf α 𝔅  𝔉 𝔊 ψ by (rule assms(1))
  from assms show ?thesis
    unfolding cat_op_simps ntcf_rcomp_Hom_component_def ψ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_lcomp_Hom_component_ArrCod[cat_cs_simps]:
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα" and "b  Obj"
  shows "ntcf_lcomp_Hom_component φ a bArrCod = Hom  (𝔉ObjMapa) b"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  from assms show ?thesis
    unfolding ntcf_lcomp_Hom_component_def φ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma ntcf_rcomp_Hom_component_ArrCod[cat_cs_simps]:
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα" and "a  op_cat Obj"
  shows "ntcf_rcomp_Hom_component ψ a bArrCod = Hom  a (𝔊ObjMapb)" 
proof-
  interpret ψ: is_ntcf α 𝔅  𝔉 𝔊 ψ by (rule assms(1))
  from assms show ?thesis
    unfolding cat_op_simps ntcf_rcomp_Hom_component_def ψ.ntcf_NTDGCod
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed


subsubsection‹
Component of a composition of a Hom›-natural transformation 
with a natural transformation is an arrow in the category Set›

lemma (in category) cat_ntcf_lcomp_Hom_component_is_arr:
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "a  op_cat 𝔄Obj" 
    and "b  Obj"
  shows "ntcf_lcomp_Hom_component φ a b :
    Hom  (𝔊ObjMapa) b cat_Set αHom  (𝔉ObjMapa) b"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  from assms have a: "a  𝔄Obj" unfolding cat_op_simps by simp
  from assms(1,3) a have 
    "ntcf_lcomp_Hom_component φ a b :
      Hom  (𝔊ObjMapa) (cf_id ObjMapb) cat_Set αHom  (𝔉ObjMapa) (cf_id ObjMapb)"
    unfolding ntcf_lcomp_Hom_component_def φ.ntcf_NTDGCod
    by (intro cat_ntcf_Hom_component_is_arr)
      (cs_concl cs_intro: cat_cs_intros cat_op_intros)+
  from this assms(1,3) a show ?thesis 
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)
qed

lemma (in category) cat_ntcf_lcomp_Hom_component_is_arr':
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "a  op_cat 𝔄Obj" 
    and "b  Obj"
    and "𝔄' = Hom  (𝔊ObjMapa) b"
    and "𝔅' = Hom  (𝔉ObjMapa) b"
    and "ℭ' = cat_Set α"
  shows "ntcf_lcomp_Hom_component φ a b : 𝔄' ℭ'𝔅'"
  using assms(1-3) 
  unfolding assms(4-6) 
  by (rule cat_ntcf_lcomp_Hom_component_is_arr)

lemmas [cat_cs_intros] = category.cat_ntcf_lcomp_Hom_component_is_arr'

lemma (in category) cat_ntcf_rcomp_Hom_component_is_arr:
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα"
    and "a  op_cat Obj" 
    and "b  𝔅Obj"
  shows "ntcf_rcomp_Hom_component ψ a b :
    Hom  a (𝔉ObjMapb) cat_Set αHom  a (𝔊ObjMapb)"
proof-
  interpret ψ: is_ntcf α 𝔅  𝔉 𝔊 ψ by (rule assms(1))
  from assms have a: "a  Obj" unfolding cat_op_simps by simp
  from assms(1,3) a have 
    "ntcf_rcomp_Hom_component ψ a b :
      Hom  (cf_id ObjMapa) (𝔉ObjMapb) cat_Set αHom  (cf_id ObjMapa) (𝔊ObjMapb)"
    unfolding ntcf_rcomp_Hom_component_def ψ.ntcf_NTDGCod
    by (intro cat_ntcf_Hom_component_is_arr)
      (cs_concl cs_intro: cat_cs_intros cat_op_intros)
  from this assms(1,3) a show ?thesis 
    by (cs_prems cs_shallow cs_simp: cat_cs_simps)
qed

lemma (in category) cat_ntcf_rcomp_Hom_component_is_arr':
  assumes "ψ : 𝔉 CF 𝔊 : 𝔅 ↦↦Cα"
    and "a  op_cat Obj" 
    and "b  𝔅Obj"
    and "𝔄' = Hom  a (𝔉ObjMapb)"
    and "𝔅' = Hom  a (𝔊ObjMapb)"
    and "ℭ' = cat_Set α"
  shows "ntcf_rcomp_Hom_component ψ a b : 𝔄' ℭ'𝔅'"
  using assms(1-3) 
  unfolding assms(4-6)
  by (rule cat_ntcf_rcomp_Hom_component_is_arr)

lemmas [cat_cs_intros] = category.cat_ntcf_rcomp_Hom_component_is_arr'



subsection‹
Composition of a Hom›-natural transformation with two natural transformations
›


subsubsection‹Definition and elementary properties›


text‹See subsection 1.15 in cite"bodo_categories_1970".›

definition ntcf_Hom :: "V  V  V  V" (HomA.Cı'(/_-,_-/'))
  where "HomA.Cα(φ-,ψ-) =
    [
      (
        λab(op_cat (φNTDGDom) ×C ψNTDGDom)Obj.
          ntcf_Hom_component φ ψ (vpfst ab) (vpsnd ab)
      ),
      HomO.CαψNTDGCod(φNTCod-,ψNTDom-),
      HomO.CαψNTDGCod(φNTDom-,ψNTCod-),
      op_cat (φNTDGDom) ×C ψNTDGDom,
      cat_Set α
    ]"


text‹Components.›

lemma ntcf_Hom_components:
  shows "HomA.Cα(φ-,ψ-)NTMap =
    (
      λab(op_cat (φNTDGDom) ×C ψNTDGDom)Obj.
        ntcf_Hom_component φ ψ (vpfst ab) (vpsnd ab)
    )"
    and "HomA.Cα(φ-,ψ-)NTDom =
      HomO.CαψNTDGCod(φNTCod-,ψNTDom-)"
    and "HomA.Cα(φ-,ψ-)NTCod =
      HomO.CαψNTDGCod(φNTDom-,ψNTCod-)"
    and "HomA.Cα(φ-,ψ-)NTDGDom = op_cat (φNTDGDom) ×C ψNTDGDom"
    and "HomA.Cα(φ-,ψ-)NTDGCod = cat_Set α"
  unfolding ntcf_Hom_def nt_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

mk_VLambda ntcf_Hom_components(1)
  |vsv ntcf_Hom_NTMap_vsv|

context
  fixes α φ ψ 𝔉 𝔊 𝔉' 𝔊' 𝔄 𝔅 
  assumes φ: "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and ψ: "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
begin

interpretation φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule φ)
interpretation ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule ψ)

mk_VLambda ntcf_Hom_components(1)[of _ φ ψ, simplified]
  |vdomain ntcf_Hom_NTMap_vdomain[unfolded in_Hom_iff]|

lemmas [cat_cs_simps] = ntcf_Hom_NTMap_vdomain

lemma ntcf_Hom_NTMap_app[cat_cs_simps]:
  assumes "[a, b]  (op_cat 𝔄 ×C 𝔅)Obj"
  shows "HomA.Cα(φ-,ψ-)NTMapa, b = ntcf_Hom_component φ ψ a b"
  using assms
  unfolding ntcf_Hom_components
  by (simp add: nat_omega_simps cat_cs_simps)

end

lemma (in category) ntcf_Hom_NTMap_vrange: 
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα" and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
  shows " (HomA.Cα(φ-,ψ-)NTMap)  cat_Set αArr"
proof-
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  interpret ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule assms(2))
  show ?thesis
  proof
    (
      rule vsv.vsv_vrange_vsubset, 
      unfold ntcf_Hom_NTMap_vdomain[OF assms] cat_cs_simps
    )
    fix ab assume "ab  (op_cat 𝔄 ×C 𝔅)Obj"
    then obtain a b
      where ab_def: "ab = [a, b]" 
        and a: "a  op_cat 𝔄Obj" 
        and b: "b  𝔅Obj"
      by 
        (
          rule cat_prod_2_ObjE[
            OF φ.NTDom.HomDom.category_op ψ.NTDom.HomDom.category_axioms
            ]
        )
    from assms a b category_cat_Set category_axioms show 
      "HomA.Cα(φ-,ψ-)NTMapab  cat_Set αArr"
      unfolding ab_def cat_op_simps
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
        )
  qed (simp add: ntcf_Hom_NTMap_vsv)
qed


subsubsection‹
Composition of a Hom›-natural transformation with 
two natural transformations is a natural transformation
›

lemma (in category) cat_ntcf_Hom_is_ntcf: 
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα" and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
  shows "HomA.Cα(φ-,ψ-) :
    HomO.Cα(𝔊-,𝔉'-) CF HomO.Cα(𝔉-,𝔊'-) :
    op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
proof-

  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(1))
  interpret ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule assms(2))

  show ?thesis
  proof(intro is_ntcfI')
    show "vfsequence (HomA.Cα(φ-,ψ-))" unfolding ntcf_Hom_def by simp
    show "vcard (HomA.Cα(φ-,ψ-)) = 5"
      unfolding ntcf_Hom_def by (simp add: nat_omega_simps)
    from assms category_axioms show 
      "HomO.Cα(𝔊-,𝔉'-) : op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms category_axioms show 
      "HomO.Cα(𝔉-,𝔊'-) : op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms show "𝒟 (HomA.Cα(φ-,ψ-)NTMap) = (op_cat 𝔄 ×C 𝔅)Obj"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "HomA.Cα(φ-,ψ-)NTMapab :
      HomO.Cα(𝔊-,𝔉'-)ObjMapab cat_Set αHomO.Cα(𝔉-,𝔊'-)ObjMapab"
      if "ab  (op_cat 𝔄 ×C 𝔅)Obj" for ab 
    proof-
      from that obtain a b
        where ab_def: "ab = [a, b]" 
          and a: "a  op_cat 𝔄Obj" 
          and b: "b  𝔅Obj"
        by 
          (
            rule cat_prod_2_ObjE[
              OF φ.NTDom.HomDom.category_op ψ.NTDom.HomDom.category_axioms
              ]
          )
      from category_axioms assms a b show 
        "HomA.Cα(φ-,ψ-)NTMapab :
          HomO.Cα(𝔊-,𝔉'-)ObjMapab cat_Set αHomO.Cα(𝔉-,𝔊'-)ObjMapab"
        unfolding ab_def cat_op_simps
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed
    show 
      "HomA.Cα(φ-,ψ-)NTMapa'b' Acat_Set αHomO.Cα(𝔊-,𝔉'-)ArrMapgf =
        HomO.Cα(𝔉-,𝔊'-)ArrMapgf Acat_Set αHomA.Cα(φ-,ψ-)NTMapab"
      if "gf : ab op_cat 𝔄 ×C 𝔅a'b'" for ab a'b' gf
    proof-
      from that obtain g f a b a' b'
        where gf_def: "gf = [g, f]" 
          and ab_def: "ab = [a, b]" 
          and a'b'_def: "a'b' = [a', b']"
          and g: "g : a op_cat 𝔄a'"
          and f: "f : b 𝔅b'" 
        by 
          (
            elim 
              cat_prod_2_is_arrE[
                OF φ.NTDom.HomDom.category_op ψ.NTDom.HomDom.category_axioms
                ]
          )
      from assms category_axioms that g f show ?thesis
        unfolding gf_def ab_def a'b'_def cat_op_simps
        by (*slow*)
          (
            cs_concl 
              cs_simp: cat_ntcf_Hom_component_nat cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed
  qed (auto simp: ntcf_Hom_components cat_cs_simps)

qed

lemma (in category) cat_ntcf_Hom_is_ntcf': 
  assumes "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα" 
    and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
    and "β = α"
    and "𝔄' = HomO.Cα(𝔊-,𝔉'-)"
    and "𝔅' = HomO.Cα(𝔉-,𝔊'-)"
    and "ℭ' = op_cat 𝔄 ×C 𝔅"
    and "𝔇' = cat_Set α"
  shows "HomA.Cα(φ-,ψ-) : 𝔄' CF 𝔅' : ℭ' ↦↦Cβ𝔇'"
  using assms(1-2) unfolding assms(3-7) by (rule cat_ntcf_Hom_is_ntcf)

lemmas [cat_cs_intros] = category.cat_ntcf_Hom_is_ntcf'


subsubsection‹
Composition of a Hom›-natural transformation with 
two vertical compositions of natural transformations
›

lemma (in category) cat_ntcf_Hom_vcomp:
  assumes "φ' : 𝔊 CF  : 𝔄 ↦↦Cα" 
    and "φ : 𝔉 CF 𝔊 : 𝔄 ↦↦Cα"
    and "ψ' : 𝔊' CF ℌ' : 𝔅 ↦↦Cα" 
    and "ψ : 𝔉' CF 𝔊' : 𝔅 ↦↦Cα"
  shows 
    "HomA.Cα(φ' NTCF φ-,ψ' NTCF ψ-) =
      HomA.Cα(φ-,ψ'-) NTCF HomA.Cα(φ'-,ψ-)"
proof(rule ntcf_eqI[of α])

  interpret φ': is_ntcf α 𝔄  𝔊  φ' by (rule assms(1))
  interpret φ: is_ntcf α 𝔄  𝔉 𝔊 φ by (rule assms(2))
  interpret ψ': is_ntcf α 𝔅  𝔊' ℌ' ψ' by (rule assms(3))
  interpret ψ: is_ntcf α 𝔅  𝔉' 𝔊' ψ by (rule assms(4))

  from category_axioms assms show H_vcomp:
    "HomA.Cα(φ' NTCF φ-,ψ' NTCF ψ-) :
      HomO.Cα(-,𝔉'-) CF HomO.Cα(𝔉-,ℌ'-) :
      op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from category_axioms assms show vcomp_H:
    "HomA.Cα(φ-,ψ'-) NTCF HomA.Cα(φ'-,ψ-) :
      HomO.Cα(-,𝔉'-) CF HomO.Cα(𝔉-,ℌ'-) :
      op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from category_axioms assms H_vcomp have dom_H_vcomp:
    "𝒟 (HomA.Cα(φ' NTCF φ-,ψ' NTCF ψ-)NTMap) = (op_cat 𝔄 ×C 𝔅)Obj"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from category_axioms assms H_vcomp have dom_vcomp_H:
    "𝒟 ((HomA.Cα(φ-,ψ'-) NTCF HomA.Cα(φ'-,ψ-))NTMap) =
      (op_cat 𝔄 ×C 𝔅)Obj"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

  show "HomA.Cα(φ' NTCF φ-,ψ' NTCF ψ-)NTMap =
    (HomA.Cα(φ-,ψ'-) NTCF HomA.Cα(φ'-,ψ-))NTMap"
  proof(rule vsv_eqI, unfold dom_H_vcomp dom_vcomp_H)
    fix ab assume prems: "ab  (op_cat 𝔄 ×C 𝔅)Obj"
    then obtain a b
      where ab_def: "ab = [a, b]" 
        and a: "a  𝔄Obj" 
        and b: "b  𝔅Obj"
      by 
        ( 
          auto 
            elim: 
              cat_prod_2_ObjE[
                OF φ'.NTDom.HomDom.category_op ψ'.NTDom.HomDom.category_axioms
                ]
            simp: cat_op_simps
        )
    from 
      assms a b
      category_axioms 
      φ'.NTDom.HomDom.category_axioms
      ψ'.NTDom.HomDom.category_axioms 
    show
      "HomA.Cα(φ' NTCF φ-,ψ' NTCF ψ-)NTMapab =
        (HomA.Cα(φ-,ψ'-) NTCF HomA.Cα(φ'-,ψ-))NTMapab"
      by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps ab_def
            cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
        )
  qed (auto simp: ntcf_Hom_NTMap_vsv cat_cs_intros)

qed simp_all

lemmas [cat_cs_simps] = category.cat_ntcf_Hom_vcomp

lemma (in category) cat_ntcf_Hom_ntcf_id:
  assumes "𝔉 : 𝔄 ↦↦Cα" and "𝔉': 𝔅 ↦↦Cα"
  shows "HomA.Cα(ntcf_id 𝔉-,ntcf_id 𝔉'-) = ntcf_id HomO.Cα(𝔉-,𝔉'-)"
proof(rule ntcf_eqI[of α])

  interpret 𝔉: is_functor α 𝔄  𝔉 by (rule assms(1))
  interpret 𝔉': is_functor α 𝔅  𝔉' by (rule assms(2))

  from category_axioms assms show H_id:
    "HomA.Cα(ntcf_id 𝔉-,ntcf_id 𝔉'-) :
      HomO.Cα(𝔉-,𝔉'-) CF HomO.Cα(𝔉-,𝔉'-) :
      op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from category_axioms assms show id_H:
    "ntcf_id HomO.Cα(𝔉-,𝔉'-) :
      HomO.Cα(𝔉-,𝔉'-) CF HomO.Cα(𝔉-,𝔉'-) :
      op_cat 𝔄 ×C 𝔅 ↦↦Cαcat_Set α"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

  from category_axioms assms H_id have dom_H_id:
    "𝒟 (HomA.Cα(