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 α) Hom⇩O⇩.⇩C⇘α⇙𝔎⦇HomDom⦈(r,-) 𝔎.
        ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇𝔎⦇HomDom⦈⦇CId⦈⦇r⦈⦈
    )"


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 =
    [
      (λf∈⇩∘Hom (𝔎⦇HomDom⦈) r d. 𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇u⦈),
      Hom (𝔎⦇HomDom⦈) r d,
      𝔎⦇ObjMap⦈⦇d⦈
    ]⇩∘"


text‹Components.›

lemma (in is_functor) Yoneda_component_components: 
  shows "Yoneda_component 𝔉 r u d⦇ArrVal⦈ =
    (λf∈⇩∘Hom 𝔄 r d. 𝔉⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇u⦈)"
    and "Yoneda_component 𝔉 r u d⦇ArrDom⦈ = Hom 𝔄 r d"
    and "Yoneda_component 𝔉 r u d⦇ArrCod⦈ = 𝔉⦇ObjMap⦈⦇d⦈"
  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 ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
    and "d ∈⇩∘ ℭ⦇Obj⦈"
  shows "Yoneda_component 𝔎 r u d : Hom ℭ r d ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇d⦈"   
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 "ℛ⇩∘ (λf∈⇩∘Hom ℭ r d. 𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇u⦈) ⊆⇩∘ 𝔎⦇ObjMap⦈⦇d⦈"
    proof(rule vrange_VLambda_vsubset)
      fix f assume "f ∈⇩∘ Hom ℭ r d"
      then have 𝔎f: "𝔎⦇ArrMap⦈⦇f⦈ : 𝔎⦇ObjMap⦈⦇r⦈ ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇d⦈" 
        by (auto simp: cat_cs_intros)
      note 𝔎f_simps = cat_Set_is_arrD[OF 𝔎f]
      interpret 𝔎f: arr_Set α ‹𝔎⦇ArrMap⦈⦇f⦈› by (rule 𝔎f_simps(1))          
      have "u ∈⇩∘ 𝒟⇩∘ (𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈)" 
        by (simp add: 𝔎f_simps assms cat_Set_cs_simps)
      with 𝔎f.arr_Set_ArrVal_vrange[unfolded 𝔎f_simps] show 
        "𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇u⦈ ∈⇩∘ 𝔎⦇ObjMap⦈⦇d⦈"
        by (blast elim: 𝔎f.ArrVal.vsv_value)
    qed 
    from assms 𝔎.HomCod.cat_Obj_vsubset_Vset show "𝔎⦇ObjMap⦈⦇d⦈ ∈⇩∘ 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 ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
    and "d ∈⇩∘ ℭ⦇Obj⦈"
    and "s = Hom ℭ r d"
    and "t = 𝔎⦇ObjMap⦈⦇d⦈"
    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∈⇩∘𝔎⦇HomDom⦈⦇Obj⦈. Yoneda_component 𝔎 r u d),
      Hom⇩O⇩.⇩C⇘α⇙𝔎⦇HomDom⦈(r,-),
      𝔎,
      𝔎⦇HomDom⦈,
      cat_Set α
    ]⇩∘"


text‹Components.›

lemma (in is_functor) Yoneda_arrow_components:
  shows "Yoneda_arrow α 𝔉 r u⦇NTMap⦈ = 
    (λd∈⇩∘𝔄⦇Obj⦈. Yoneda_component 𝔉 r u d)"
    and "Yoneda_arrow α 𝔉 r u⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)"
    and "Yoneda_arrow α 𝔉 r u⦇NTCod⦈ = 𝔉"
    and "Yoneda_arrow α 𝔉 r u⦇NTDGDom⦈ = 𝔄"
    and "Yoneda_arrow α 𝔉 r u⦇NTDGCod⦈ = 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 ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
  shows "Yoneda_arrow α 𝔎 r u : Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-) ↦⇩C⇩F 𝔎 : ℭ ↦↦⇩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
      "(λd∈⇩∘ℭ⦇Obj⦈. ?𝔎ru d)⦇a⦈ :
        Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇a⦈"
      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 
      "(λd∈⇩∘ℭ⦇Obj⦈. ?𝔎ru d)⦇b⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)⦇ArrMap⦈⦇f⦈ =
        𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ (λd∈⇩∘ℭ⦇Obj⦈. ?𝔎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 ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘ :
          Hom ℭ r a ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇b⦈"
        by
          (
            cs_concl cs_shallow 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
      then have dom_lhs: 
        "𝒟⇩∘ ((?𝔎ru b ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘)⦇ArrVal⦈) =
          Hom ℭ r a"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      from assms that 𝔐a have f_a: 
        "𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?𝔎ru a :
          Hom ℭ r a ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇b⦈"
        by (cs_concl cs_shallow cs_intro: cat_cs_intros)
      then have dom_rhs: 
        "𝒟⇩∘ ((𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?𝔎ru a)⦇ArrVal⦈) = Hom ℭ r a"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)

      have [cat_cs_simps]:
        "?𝔎ru b ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘ =
          𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?𝔎ru a"
      proof(rule arr_Set_eqI[of α])

        from b_f show arr_Set_b_f:
          "arr_Set α (?𝔎ru b ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘)"
          by (auto simp: cat_Set_is_arrD(1))
        interpret b_f: arr_Set α ‹?𝔎ru b ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘›
          by (rule arr_Set_b_f)
        from f_a show arr_Set_f_a:
          "arr_Set α (𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?𝔎ru a)"
          by (auto simp: cat_Set_is_arrD(1))
        interpret f_a: arr_Set α ‹𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?𝔎ru a›
          by (rule arr_Set_f_a)

        show 
          "(?𝔎ru b ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘)⦇ArrVal⦈ =
            (𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_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 ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [ℭ⦇CId⦈⦇r⦈, f]⇩∘)⦇ArrVal⦈⦇q⦈ =
              (𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?𝔎ru a)⦇ArrVal⦈⦇q⦈"
            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) = 𝔎⦇ObjMap⦈⦇r⦈"
    and "(Yoneda_map α 𝔎 r)¯⇩∘ = (λu∈⇩∘𝔎⦇ObjMap⦈⦇r⦈. 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: "𝔎⦇ObjMap⦈⦇r⦈ ∈⇩∘ 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: 
      "𝔐 : Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-) ↦⇩C⇩F 𝔎 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
      "𝔑 : Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-) ↦⇩C⇩F 𝔎 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
      "Yoneda_map α 𝔎 r⦇𝔐⦈ = Yoneda_map α 𝔎 r⦇𝔑⦈"
    from prems(3) have 𝔐r_𝔑r:
      "𝔐⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ = 𝔑⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈"
      unfolding 
        Yoneda_map_app[OF assms(1) prems(1)] 
        Yoneda_map_app[OF assms(1) prems(2)]
      by simp

    interpret 𝔐: is_ntcf α ℭ ‹cat_Set α› ‹Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)› 𝔎 𝔐  
      by (rule prems(1))
    interpret 𝔑: is_ntcf α ℭ ‹cat_Set α› ‹Hom⇩O⇩.⇩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 α ‹𝔐⦇NTMap⦈⦇d⦈› by (rule 𝔐d_simps(1))

      note 𝔑d_simps = cat_Set_is_arrD[OF 𝔑.ntcf_NTMap_is_arr[OF prems']]
      interpret 𝔑d: arr_Set α ‹𝔑⦇NTMap⦈⦇d⦈› by (rule 𝔑d_simps(1))

      show "𝔐⦇NTMap⦈⦇d⦈ = 𝔑⦇NTMap⦈⦇d⦈"
      proof(rule arr_Set_eqI[of α])
        show "𝔐⦇NTMap⦈⦇d⦈⦇ArrVal⦈ = 𝔑⦇NTMap⦈⦇d⦈⦇ArrVal⦈"
        proof
          (
            rule vsv_eqI, 
            unfold 
              𝔑d.arr_Set_ArrVal_vdomain 
              𝔐d.arr_Set_ArrVal_vdomain  
              𝔐d_simps
              𝔑d_simps
          )
          fix f assume prems'': "f ∈⇩∘ Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)⦇ObjMap⦈⦇d⦈"
          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 
            "(
              𝔐⦇NTMap⦈⦇d⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)⦇ArrMap⦈⦇f⦈
            )⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ =
              (𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ 𝔐⦇NTMap⦈⦇r⦈)⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈"
            by simp
          from this category_axioms assms(2) f prems prems' have 𝔐df:
            "𝔐⦇NTMap⦈⦇d⦈⦇ArrVal⦈⦇f⦈ =
              𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇𝔐⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈⦈"
            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
            "(
              𝔑⦇NTMap⦈⦇d⦈ ∘⇩A⇘cat_Set α⇙ 
              Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)⦇ArrMap⦈⦇f⦈
            )⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ = 
              (𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ 𝔑⦇NTMap⦈⦇r⦈)⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈"
            by simp
          from this category_axioms assms(2) f prems prems' have 𝔑df:
            "𝔑⦇NTMap⦈⦇d⦈⦇ArrVal⦈⦇f⦈ =
              𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇𝔑⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈⦈"
            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 "𝔐⦇NTMap⦈⦇d⦈⦇ArrVal⦈⦇f⦈ = 𝔑⦇NTMap⦈⦇d⦈⦇ArrVal⦈⦇f⦈"
            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 α 𝔎 r⦇Yoneda_arrow α 𝔎 r a⦈ = a" 
    if "a ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈" 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 α 𝔎 r⦇Yoneda_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) = 𝔎⦇ObjMap⦈⦇r⦈"
  proof(intro vsubset_antisym)

    show "ℛ⇩∘ (Yoneda_map α 𝔎 r) ⊆⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
      unfolding Yoneda_map_def
    proof(intro vrange_VLambda_vsubset, unfold these_ntcfs_iff 𝔎.cf_HomDom)
      fix 𝔐 assume prems: "𝔐 : Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-) ↦⇩C⇩F 𝔎 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
      then interpret 𝔐: is_ntcf α ℭ ‹cat_Set α› ‹Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)› 𝔎 𝔐 .
      note 𝔐r_simps = cat_Set_is_arrD[OF 𝔐.ntcf_NTMap_is_arr[OF assms(2)]]
      interpret 𝔐r: arr_Set α ‹𝔐⦇NTMap⦈⦇r⦈› by (rule 𝔐r_simps(1))
      from prems category_axioms assms(2) have 
        "ℭ⦇CId⦈⦇r⦈ ∈⇩∘ 𝒟⇩∘ (𝔐⦇NTMap⦈⦇r⦈⦇ArrVal⦈)"
        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 "𝔐⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ ∈⇩∘ ℛ⇩∘ (𝔐⦇NTMap⦈⦇r⦈⦇ArrVal⦈)"
        by (blast elim: 𝔐r.ArrVal.vsv_value)
      then show "𝔐⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
        by (auto simp: 𝔐r_simps dest!: vsubsetD[OF 𝔐r.arr_Set_ArrVal_vrange])
    qed
    
    show "𝔎⦇ObjMap⦈⦇r⦈ ⊆⇩∘ ℛ⇩∘ (Yoneda_map α 𝔎 r)"
    proof(intro vsubsetI)
      fix u assume prems: "u ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
      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∈⇩∘𝔎⦇ObjMap⦈⦇r⦈. 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∈⇩∘𝔎⦇ObjMap⦈⦇r⦈. Yoneda_arrow α 𝔎 r u)⦇a⦈"
      if "a ∈⇩∘ ℛ⇩∘ (Yoneda_map α 𝔎 r)" for a
    proof-
      from that have a: "a ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈" 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)¯⇩∘) = 𝔎⦇ObjMap⦈⦇r⦈"
  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 ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
  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 α) Hom⇩O⇩.⇩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 =
    [
      (
        λf∈⇩∘Hom (φ⦇NTDGCod⦈) (φ⦇NTCod⦈⦇ObjMap⦈⦇a⦈) (ψ⦇NTDom⦈⦇ObjMap⦈⦇b⦈).
          ψ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ψ⦇NTDGCod⦈⇙ f ∘⇩A⇘ψ⦇NTDGCod⦈⇙ φ⦇NTMap⦈⦇a⦈
      ),
      Hom (φ⦇NTDGCod⦈) (φ⦇NTCod⦈⦇ObjMap⦈⦇a⦈) (ψ⦇NTDom⦈⦇ObjMap⦈⦇b⦈),
      Hom (φ⦇NTDGCod⦈) (φ⦇NTDom⦈⦇ObjMap⦈⦇a⦈) (ψ⦇NTCod⦈⦇ObjMap⦈⦇b⦈)
    ]⇩∘"


text‹Components.›

lemma ntcf_Hom_component_components: 
  shows "ntcf_Hom_component φ ψ a b⦇ArrVal⦈ =
    (
      λf∈⇩∘Hom (φ⦇NTDGCod⦈) (φ⦇NTCod⦈⦇ObjMap⦈⦇a⦈) (ψ⦇NTDom⦈⦇ObjMap⦈⦇b⦈).
        ψ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ψ⦇NTDGCod⦈⇙ f ∘⇩A⇘ψ⦇NTDGCod⦈⇙ φ⦇NTMap⦈⦇a⦈
    )"
    and "ntcf_Hom_component φ ψ a b⦇ArrDom⦈ =
      Hom (φ⦇NTDGCod⦈) (φ⦇NTCod⦈⦇ObjMap⦈⦇a⦈) (ψ⦇NTDom⦈⦇ObjMap⦈⦇b⦈)"
    and "ntcf_Hom_component φ ψ a b⦇ArrCod⦈ =
      Hom (φ⦇NTDGCod⦈) (φ⦇NTDom⦈⦇ObjMap⦈⦇a⦈) (ψ⦇NTCod⦈⦇ObjMap⦈⦇b⦈)"
  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 φ: "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and ψ: "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩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 b⦇ArrVal⦈) ⊆⇩∘
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔊'⦇ObjMap⦈⦇b⦈)"
proof
  (
    rule vsv.vsv_vrange_vsubset, 
    unfold ntcf_Hom_component_ArrVal_vdomain in_Hom_iff
  )
  fix f assume "f : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
  with assms φ ψ show 
    "ntcf_Hom_component φ ψ a b⦇ArrVal⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ 𝔊'⦇ObjMap⦈⦇b⦈"
    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 φ: "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and ψ: "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
begin

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

lemma ntcf_Hom_component_ArrDom[cat_cs_simps]:
  "ntcf_Hom_component φ ψ a b⦇ArrDom⦈ = Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"
  unfolding ntcf_Hom_component_components by (simp add: cat_cs_simps)

lemma ntcf_Hom_component_ArrCod[cat_cs_simps]:
  "ntcf_Hom_component φ ψ a b⦇ArrCod⦈ = Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔊'⦇ObjMap⦈⦇b⦈)"
  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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat 𝔄⦇Obj⦈"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows 
    "ntcf_Hom_component φ ψ a b :
      Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔊'⦇ObjMap⦈⦇b⦈)"
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 b⦇ArrVal⦈) ⊆⇩∘ 
        ntcf_Hom_component φ ψ a b⦇ArrCod⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    from assms(1,2,4) a show "ntcf_Hom_component φ ψ a b⦇ArrDom⦈ ∈⇩∘ 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 b⦇ArrCod⦈ ∈⇩∘ 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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat 𝔄⦇Obj⦈"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
    and "𝔄' = Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"
    and "𝔅' = Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔊'⦇ObjMap⦈⦇b⦈)"
    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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "g : a ↦⇘op_cat 𝔄⇙ a'"
    and "f : b ↦⇘𝔅⇙ b'" 
  shows
    "ntcf_Hom_component φ ψ a' b' ∘⇩A⇘cat_Set α⇙
     cf_hom ℭ [𝔊⦇ArrMap⦈⦇g⦈, 𝔉'⦇ArrMap⦈⦇f⦈]⇩∘ =
      cf_hom ℭ [𝔉⦇ArrMap⦈⦇g⦈, 𝔊'⦇ArrMap⦈⦇f⦈]⇩∘ ∘⇩A⇘cat_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 = ‹𝔊⦇ArrMap⦈⦇g⦈›
    and ?𝔉'f = ‹𝔉'⦇ArrMap⦈⦇f⦈›
    and ?𝔉g = ‹𝔉⦇ArrMap⦈⦇g⦈›
    and ?𝔊'f = ‹𝔊'⦇ArrMap⦈⦇f⦈›
    and ?𝔊a = ‹𝔊⦇ObjMap⦈⦇a⦈›
    and ?𝔉'b = ‹𝔉'⦇ObjMap⦈⦇b⦈›
    and ?𝔉a' = ‹𝔉⦇ObjMap⦈⦇a'⦈›
    and ?𝔊'b' = ‹𝔊'⦇ObjMap⦈⦇b'⦈›

  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' ∘⇩A⇘cat_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' ∘⇩A⇘cat_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]⇩∘ ∘⇩A⇘cat_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]⇩∘ ∘⇩A⇘cat_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' ∘⇩A⇘cat_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]⇩∘ ∘⇩A⇘cat_Set α⇙ ?Y_ab)"
      by (auto dest: cat_Set_is_arrD(1))
    show 
      "(?Y_a'b' ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [?𝔊g, ?𝔉'f]⇩∘)⦇ArrVal⦈ =
        (cf_hom ℭ [?𝔉g, ?𝔊'f]⇩∘ ∘⇩A⇘cat_Set α⇙ ?Y_ab)⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix h assume prems: "h : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
      from assms(1,2) g have [cat_cs_simps]:
        "ψ⦇NTMap⦈⦇b'⦈ ∘⇩A⇘ℭ⇙ (?𝔉'f ∘⇩A⇘ℭ⇙ (h ∘⇩A⇘ℭ⇙ (?𝔊g ∘⇩A⇘ℭ⇙ φ⦇NTMap⦈⦇a'⦈))) =
          ψ⦇NTMap⦈⦇b'⦈ ∘⇩A⇘ℭ⇙ (?𝔉'f ∘⇩A⇘ℭ⇙ (h ∘⇩A⇘ℭ⇙ (φ⦇NTMap⦈⦇a⦈ ∘⇩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 "… =
        (((ψ⦇NTMap⦈⦇b'⦈ ∘⇩A⇘ℭ⇙ ?𝔉'f) ∘⇩A⇘ℭ⇙ h) ∘⇩A⇘ℭ⇙ φ⦇NTMap⦈⦇a⦈) ∘⇩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⇘ℭ⇙ ψ⦇NTMap⦈⦇b⦈) ∘⇩A⇘ℭ⇙ h) ∘⇩A⇘ℭ⇙ φ⦇NTMap⦈⦇a⦈) ∘⇩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⇘ℭ⇙ (ψ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (h ∘⇩A⇘ℭ⇙ (φ⦇NTMap⦈⦇a⦈ ∘⇩A⇘ℭ⇙ ?𝔉g)))"
        by (cs_concl cs_simp: cat_Comp_assoc cs_intro: cat_cs_intros) (*slow*)
      finally have nat:
        "ψ⦇NTMap⦈⦇b'⦈ ∘⇩A⇘ℭ⇙ (?𝔉'f ∘⇩A⇘ℭ⇙ (h ∘⇩A⇘ℭ⇙ (?𝔊g ∘⇩A⇘ℭ⇙ φ⦇NTMap⦈⦇a'⦈))) =
          ?𝔊'f ∘⇩A⇘ℭ⇙ (ψ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ (h ∘⇩A⇘ℭ⇙ (φ⦇NTMap⦈⦇a⦈ ∘⇩A⇘ℭ⇙ ?𝔉g)))".
      from prems Set.category_axioms category_axioms assms(1,2,4) g show 
        "(?Y_a'b' ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [?𝔊g, ?𝔉'f]⇩∘)⦇ArrVal⦈⦇h⦈ =
          (cf_hom ℭ [?𝔉g, ?𝔊'f]⇩∘ ∘⇩A⇘cat_Set α⇙ ?Y_ab)⦇ArrVal⦈⦇h⦈"
        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 "φ' : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
    and "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "ψ' : 𝔊' ↦⇩C⇩F ℌ' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ 𝔄⦇Obj⦈"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows 
    "ntcf_Hom_component φ ψ' a b ∘⇩A⇘cat_Set α⇙ ntcf_Hom_component φ' ψ a b =
      ntcf_Hom_component (φ' ∙⇩N⇩T⇩C⇩F φ) (ψ' ∙⇩N⇩T⇩C⇩F ψ) a b"
    (is ‹?φψ' ∘⇩A⇘cat_Set α⇙ ?φ'ψ = ?φ'φψ'ψ›)
proof-

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

  from assms Set.category_axioms category_axioms have φψ'_φ'ψ: 
    "?φψ' ∘⇩A⇘cat_Set α⇙ ?φ'ψ :
      Hom ℭ (ℌ⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (ℌ'⦇ObjMap⦈⦇b⦈)"    
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  then have dom_lhs: 
    "𝒟⇩∘ ((?φψ' ∘⇩A⇘cat_Set α⇙ ?φ'ψ)⦇ArrVal⦈) = 
      Hom ℭ (ℌ⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from assms Set.category_axioms category_axioms have φ'φψ'ψ: 
    "?φ'φψ'ψ :
      Hom ℭ (ℌ⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (ℌ'⦇ObjMap⦈⦇b⦈)"    
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  then have dom_rhs: 
    "𝒟⇩∘ (?φ'φψ'ψ⦇ArrVal⦈) = Hom ℭ (ℌ⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)" 
    by (cs_concl cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    from φψ'_φ'ψ show arr_Set_φψ'_φ'ψ: "arr_Set α (?φψ' ∘⇩A⇘cat_Set α⇙ ?φ'ψ)"
      by (auto dest: cat_Set_is_arrD(1))
    from φ'φψ'ψ show arr_Set_φ'φψ'ψ: "arr_Set α ?φ'φψ'ψ"
      by (auto dest: cat_Set_is_arrD(1))
    show "(?φψ' ∘⇩A⇘cat_Set α⇙ ?φ'ψ)⦇ArrVal⦈ = ?φ'φψ'ψ⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix f assume "f : ℌ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
      with category_axioms assms Set.category_axioms show 
        "(?φψ' ∘⇩A⇘cat_Set α⇙ ?φ'ψ)⦇ArrVal⦈⦇f⦈ = ?φ'φψ'ψ⦇ArrVal⦈⦇f⦈"
        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 α⦇CId⦈⦇Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)⦈"
    (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 ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"    
    by (cs_concl cs_intro: cat_cs_intros cat_op_intros)
  then have dom_lhs: "𝒟⇩∘ (?𝔉𝔉'⦇ArrVal⦈) = Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"
    by (cs_concl cs_simp: cat_cs_simps)

  from category_axioms assms Set.category_axioms have 𝔉a𝔉'b: 
    "cat_Set α⦇CId⦈⦇?𝔉a𝔉'b⦈ :
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"
    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𝔉'b⦈⦇ArrVal⦈) = Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)"
    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𝔉'b⦈⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)  
      fix f assume "f : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
      with category_axioms Set.category_axioms assms show 
        "?𝔉𝔉'⦇ArrVal⦈⦇f⦈ = cat_Set α⦇CId⦈⦇?𝔉a𝔉'b⦈⦇ArrVal⦈⦇f⦈"
        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 b⦇ArrVal⦈)"
  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 b⦇ArrVal⦈)"
  unfolding ntcf_rcomp_Hom_component_def by (rule ntcf_Hom_component_ArrVal_vsv)

lemma ntcf_lcomp_Hom_component_ArrVal_vdomain[cat_cs_simps]: 
  assumes "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "𝒟⇩∘ (ntcf_lcomp_Hom_component φ a b⦇ArrVal⦈) = Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) 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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
  shows "𝒟⇩∘ (ntcf_rcomp_Hom_component ψ a b⦇ArrVal⦈) = Hom ℭ a (𝔉⦇ObjMap⦈⦇b⦈)"
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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat 𝔄⦇Obj⦈"
    and "b ∈⇩∘ ℭ⦇Obj⦈"
    and "h : 𝔊⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ b"
  shows "ntcf_lcomp_Hom_component φ a b⦇ArrVal⦈⦇h⦈ = h ∘⇩A⇘ℭ⇙ φ⦇NTMap⦈⦇a⦈"
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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
    and "h : a ↦⇘ℭ⇙ 𝔉⦇ObjMap⦈⦇b⦈"
  shows "ntcf_rcomp_Hom_component ψ a b⦇ArrVal⦈⦇h⦈ = ψ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ h"
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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" 
    and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "ℛ⇩∘ (ntcf_lcomp_Hom_component φ a b⦇ArrVal⦈) ⊆⇩∘ Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) 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 b⦇ArrVal⦈) ⊆⇩∘
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (cf_id ℭ⦇ObjMap⦈⦇b⦈)"
    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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "ℛ⇩∘ (ntcf_rcomp_Hom_component ψ a b⦇ArrVal⦈) ⊆⇩∘ Hom ℭ a (𝔊⦇ObjMap⦈⦇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_rcomp_Hom_component ψ a b⦇ArrVal⦈) ⊆⇩∘
      Hom ℭ (cf_id ℭ⦇ObjMap⦈⦇a⦈) (𝔊⦇ObjMap⦈⦇b⦈)"
    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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "ntcf_lcomp_Hom_component φ a b⦇ArrDom⦈ = Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) 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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
  shows "ntcf_rcomp_Hom_component ψ a b⦇ArrDom⦈ = Hom ℭ a (𝔉⦇ObjMap⦈⦇b⦈)"
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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "ntcf_lcomp_Hom_component φ a b⦇ArrCod⦈ = Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) 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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
  shows "ntcf_rcomp_Hom_component ψ a b⦇ArrCod⦈ = Hom ℭ a (𝔊⦇ObjMap⦈⦇b⦈)" 
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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" 
    and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "ntcf_lcomp_Hom_component φ a b :
    Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) b ↦⇘cat_Set α⇙ Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) 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 ℭ (𝔊⦇ObjMap⦈⦇a⦈) (cf_id ℭ⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙ 
      Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) (cf_id ℭ⦇ObjMap⦈⦇b⦈)"
    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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" 
    and "b ∈⇩∘ ℭ⦇Obj⦈"
    and "𝔄' = Hom ℭ (𝔊⦇ObjMap⦈⦇a⦈) b"
    and "𝔅' = Hom ℭ (𝔉⦇ObjMap⦈⦇a⦈) 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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat ℭ⦇Obj⦈" 
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "ntcf_rcomp_Hom_component ψ a b :
    Hom ℭ a (𝔉⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙ Hom ℭ a (𝔊⦇ObjMap⦈⦇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_rcomp_Hom_component ψ a b :
      Hom ℭ (cf_id ℭ⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙
      Hom ℭ (cf_id ℭ⦇ObjMap⦈⦇a⦈) (𝔊⦇ObjMap⦈⦇b⦈)"
    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 "ψ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "a ∈⇩∘ op_cat ℭ⦇Obj⦈" 
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
    and "𝔄' = Hom ℭ a (𝔉⦇ObjMap⦈⦇b⦈)"
    and "𝔅' = Hom ℭ a (𝔊⦇ObjMap⦈⦇b⦈)"
    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" (‹Hom⇩A⇩.⇩Cı'(/_-,_-/')›)
  where "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-) =
    [
      (
        λab∈⇩∘(op_cat (φ⦇NTDGDom⦈) ×⇩C ψ⦇NTDGDom⦈)⦇Obj⦈.
          ntcf_Hom_component φ ψ (vpfst ab) (vpsnd ab)
      ),
      Hom⇩O⇩.⇩C⇘α⇙ψ⦇NTDGCod⦈(φ⦇NTCod⦈-,ψ⦇NTDom⦈-),
      Hom⇩O⇩.⇩C⇘α⇙ψ⦇NTDGCod⦈(φ⦇NTDom⦈-,ψ⦇NTCod⦈-),
      op_cat (φ⦇NTDGDom⦈) ×⇩C ψ⦇NTDGDom⦈,
      cat_Set α
    ]⇩∘"


text‹Components.›

lemma ntcf_Hom_components:
  shows "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈ =
    (
      λab∈⇩∘(op_cat (φ⦇NTDGDom⦈) ×⇩C ψ⦇NTDGDom⦈)⦇Obj⦈.
        ntcf_Hom_component φ ψ (vpfst ab) (vpsnd ab)
    )"
    and "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTDom⦈ =
      Hom⇩O⇩.⇩C⇘α⇙ψ⦇NTDGCod⦈(φ⦇NTCod⦈-,ψ⦇NTDom⦈-)"
    and "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTCod⦈ =
      Hom⇩O⇩.⇩C⇘α⇙ψ⦇NTDGCod⦈(φ⦇NTDom⦈-,ψ⦇NTCod⦈-)"
    and "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTDGDom⦈ = op_cat (φ⦇NTDGDom⦈) ×⇩C ψ⦇NTDGDom⦈"
    and "Hom⇩A⇩.⇩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 φ: "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and ψ: "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩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 "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈⦇a, 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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩A⇩.⇩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 
      "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈⦇ab⦈ ∈⇩∘ 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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-) :
    Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔊-,𝔉'-) ↦⇩C⇩F Hom⇩O⇩.⇩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 (Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-))" unfolding ntcf_Hom_def by simp
    show "vcard (Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)) = 5⇩ℕ"
      unfolding ntcf_Hom_def by (simp add: nat_omega_simps)
    from assms category_axioms show 
      "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔊-,𝔉'-) : op_cat 𝔄 ×⇩C 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms category_axioms show 
      "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊'-) : op_cat 𝔄 ×⇩C 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms show "𝒟⇩∘ (Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈) = (op_cat 𝔄 ×⇩C 𝔅)⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈⦇ab⦈ :
      Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔊-,𝔉'-)⦇ObjMap⦈⦇ab⦈ ↦⇘cat_Set α⇙
      Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊'-)⦇ObjMap⦈⦇ab⦈"
      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 
        "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈⦇ab⦈ :
          Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔊-,𝔉'-)⦇ObjMap⦈⦇ab⦈ ↦⇘cat_Set α⇙
          Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊'-)⦇ObjMap⦈⦇ab⦈"
        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 
      "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈⦇a'b'⦈ ∘⇩A⇘cat_Set α⇙
       Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔊-,𝔉'-)⦇ArrMap⦈⦇gf⦈ =
        Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊'-)⦇ArrMap⦈⦇gf⦈ ∘⇩A⇘cat_Set α⇙
        Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-)⦇NTMap⦈⦇ab⦈"
      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 "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
    and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "β = α"
    and "𝔄' = Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔊-,𝔉'-)"
    and "𝔅' = Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊'-)"
    and "ℭ' = op_cat 𝔄 ×⇩C 𝔅"
    and "𝔇' = cat_Set α"
  shows "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ-) : 𝔄' ↦⇩C⇩F 𝔅' : ℭ' ↦↦⇩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 "φ' : 𝔊 ↦⇩C⇩F ℌ : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
    and "φ : 𝔉 ↦⇩C⇩F 𝔊 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "ψ' : 𝔊' ↦⇩C⇩F ℌ' : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "ψ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows 
    "Hom⇩A⇩.⇩C⇘α⇙(φ' ∙⇩N⇩T⇩C⇩F φ-,ψ' ∙⇩N⇩T⇩C⇩F ψ-) =
      Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ'-) ∙⇩N⇩T⇩C⇩F Hom⇩A⇩.⇩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:
    "Hom⇩A⇩.⇩C⇘α⇙(φ' ∙⇩N⇩T⇩C⇩F φ-,ψ' ∙⇩N⇩T⇩C⇩F ψ-) :
      Hom⇩O⇩.⇩C⇘α⇙ℭ(ℌ-,𝔉'-) ↦⇩C⇩F Hom⇩O⇩.⇩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:
    "Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ'-) ∙⇩N⇩T⇩C⇩F Hom⇩A⇩.⇩C⇘α⇙(φ'-,ψ-) :
      Hom⇩O⇩.⇩C⇘α⇙ℭ(ℌ-,𝔉'-) ↦⇩C⇩F Hom⇩O⇩.⇩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:
    "𝒟⇩∘ (Hom⇩A⇩.⇩C⇘α⇙(φ' ∙⇩N⇩T⇩C⇩F φ-,ψ' ∙⇩N⇩T⇩C⇩F ψ-)⦇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:
    "𝒟⇩∘ ((Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ'-) ∙⇩N⇩T⇩C⇩F Hom⇩A⇩.⇩C⇘α⇙(φ'-,ψ-))⦇NTMap⦈) =
      (op_cat 𝔄 ×⇩C 𝔅)⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

  show "Hom⇩A⇩.⇩C⇘α⇙(φ' ∙⇩N⇩T⇩C⇩F φ-,ψ' ∙⇩N⇩T⇩C⇩F ψ-)⦇NTMap⦈ =
    (Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ'-) ∙⇩N⇩T⇩C⇩F Hom⇩A⇩.⇩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
      "Hom⇩A⇩.⇩C⇘α⇙(φ' ∙⇩N⇩T⇩C⇩F φ-,ψ' ∙⇩N⇩T⇩C⇩F ψ-)⦇NTMap⦈⦇ab⦈ =
        (Hom⇩A⇩.⇩C⇘α⇙(φ-,ψ'-) ∙⇩N⇩T⇩C⇩F Hom⇩A⇩.⇩C⇘α⇙(φ'-,ψ-))⦇NTMap⦈⦇ab⦈"
      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 "Hom⇩A⇩.⇩C⇘α⇙(ntcf_id 𝔉-,ntcf_id 𝔉'-) = ntcf_id Hom⇩O⇩.⇩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:
    "Hom⇩A⇩.⇩C⇘α⇙(ntcf_id 𝔉-,ntcf_id 𝔉'-) :
      Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔉'-) ↦⇩C⇩F Hom⇩O⇩.⇩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 Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔉'-) :
      Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔉'-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔉'-) :
      op_cat 𝔄 ×⇩C 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
    by (cs_concl cs_shallow cs_simp