Theory CZH_ECAT_Hom

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Hom›-functor›
theory CZH_ECAT_Hom
  imports 
    CZH_ECAT_Set
    CZH_ECAT_PCategory
begin



subsection‹‹hom›-function›


text‹
The ‹hom›-function is a part of the definition of the ‹Hom›-functor,
as presented in \<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/hom-functor
}}.
›

definition cf_hom :: "V ⇒ V ⇒ V"
  where "cf_hom ℭ f =
    [
      (
        λq∈⇩∘Hom ℭ (ℭ⦇Cod⦈⦇vpfst f⦈) (ℭ⦇Dom⦈⦇vpsnd f⦈).
          vpsnd f ∘⇩A⇘ℭ⇙ q ∘⇩A⇘ℭ⇙ vpfst f
      ),
      Hom ℭ (ℭ⦇Cod⦈⦇vpfst f⦈) (ℭ⦇Dom⦈⦇vpsnd f⦈),
      Hom ℭ (ℭ⦇Dom⦈⦇vpfst f⦈) (ℭ⦇Cod⦈⦇vpsnd f⦈)
    ]⇩∘"


text‹Components.›

lemma cf_hom_components:
  shows "cf_hom ℭ f⦇ArrVal⦈ = 
      (
        λq∈⇩∘Hom ℭ (ℭ⦇Cod⦈⦇vpfst f⦈) (ℭ⦇Dom⦈⦇vpsnd f⦈). 
          vpsnd f ∘⇩A⇘ℭ⇙ q ∘⇩A⇘ℭ⇙ vpfst f
      )"
    and "cf_hom ℭ f⦇ArrDom⦈ = Hom ℭ (ℭ⦇Cod⦈⦇vpfst f⦈) (ℭ⦇Dom⦈⦇vpsnd f⦈)"
    and "cf_hom ℭ f⦇ArrCod⦈ = Hom ℭ (ℭ⦇Dom⦈⦇vpfst f⦈) (ℭ⦇Cod⦈⦇vpsnd f⦈)"
  unfolding cf_hom_def arr_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda cf_hom_components(1)
  |vsv cf_hom_ArrVal_vsv[cat_cs_intros]|

lemma cf_hom_ArrVal_vdomain[cat_cs_simps]:
  assumes "g : a ↦⇘op_cat ℭ⇙ b" and "f : a' ↦⇘ℭ⇙ b'"
  shows "𝒟⇩∘ (cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈) = Hom ℭ a a'"
  using assms 
  unfolding cf_hom_components
  by (simp_all add: nat_omega_simps cat_op_simps cat_cs_simps)

lemma cf_hom_ArrVal_app[cat_cs_simps]:
  assumes "g : c ↦⇘op_cat ℭ⇙ d" and "q : c ↦⇘ℭ⇙ c'" and "f : c' ↦⇘ℭ⇙ d'"
  shows "cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈⦇q⦈ = f ∘⇩A⇘ℭ⇙ q ∘⇩A⇘ℭ⇙ g"
  using assms 
  unfolding cf_hom_components
  by (simp_all add: nat_omega_simps cat_op_simps cat_cs_simps)

lemma (in category) cf_hom_ArrVal_vrange:
  assumes "g : a ↦⇘op_cat ℭ⇙ b" and "f : a' ↦⇘ℭ⇙ b'"
  shows "ℛ⇩∘ (cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈) ⊆⇩∘ Hom ℭ b b'"
proof(intro vsubsetI)
  interpret gf: vsv ‹cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈› 
    unfolding cf_hom_components by auto
  fix y assume "y ∈⇩∘ ℛ⇩∘ (cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈)"
  then obtain q where y_def: "y = cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈⦇q⦈"
    and "q ∈⇩∘ 𝒟⇩∘ (cf_hom ℭ [g, f]⇩∘⦇ArrVal⦈)"
    by (metis gf.vrange_atD)
  then have q: "q : a ↦⇘ℭ⇙ a'" 
    unfolding cf_hom_ArrVal_vdomain[OF assms] by simp
  from assms q show "y ∈⇩∘ Hom ℭ b b'"
    unfolding y_def cf_hom_ArrVal_app[OF assms(1) q assms(2)] cat_op_simps 
    by (auto intro: cat_cs_intros)
qed


subsubsection‹Arrow domain›

lemma (in category) cf_hom_ArrDom:
  assumes "gf : [c, c']⇩∘ ↦⇘op_cat ℭ ×⇩C ℭ⇙ dd'"
  shows "cf_hom ℭ gf⦇ArrDom⦈ = Hom ℭ c c'"
proof-
  from assms obtain g f d d' 
    where "gf = [g, f]⇩∘" and "g : c ↦⇘op_cat ℭ⇙ d" and "f : c' ↦⇘ℭ⇙ d'"
    unfolding cf_hom_components 
    by (elim cat_prod_2_is_arrE[rotated 2]) (auto intro: cat_cs_intros)
  then show ?thesis
    unfolding cf_hom_components 
    by (simp_all add: nat_omega_simps cat_op_simps cat_cs_simps)
qed

lemmas [cat_cs_simps] = category.cf_hom_ArrDom


subsubsection‹Arrow codomain›

lemma (in category) cf_hom_ArrCod:
  assumes "gf : cc' ↦⇘op_cat ℭ ×⇩C ℭ⇙ [d, d']⇩∘"
  shows "cf_hom ℭ gf⦇ArrCod⦈ = Hom ℭ d d'"
proof-
  from assms obtain g f c c' 
    where "gf = [g, f]⇩∘" and "g : c ↦⇘op_cat ℭ⇙ d" and "f : c' ↦⇘ℭ⇙ d'"
    unfolding cf_hom_components 
    by (elim cat_prod_2_is_arrE[rotated 2]) (auto intro: cat_cs_intros)
  then show ?thesis
    unfolding cf_hom_components 
    by (simp_all add: nat_omega_simps cat_op_simps cat_cs_simps)
qed

lemmas [cat_cs_simps] = category.cf_hom_ArrCod


subsubsection‹‹hom›-function is an arrow in the category ‹Set››

lemma (in category) cat_cf_hom_ArrRel:
  assumes "gf : cc' ↦⇘op_cat ℭ ×⇩C ℭ⇙ dd'"
  shows "arr_Set α (cf_hom ℭ gf)"
proof(intro arr_SetI)
  from assms obtain g f c c' d d'
    where gf_def: "gf = [g, f]⇩∘"
      and cc'_def: "cc' = [c, c']⇩∘"
      and dd'_def: "dd' = [d, d']⇩∘"
      and op_g: "g : c ↦⇘op_cat ℭ⇙ d" 
      and f: "f : c' ↦⇘ℭ⇙ d'"
    unfolding cf_hom_components 
    by (elim cat_prod_2_is_arrE[rotated 2]) (auto intro: cat_cs_intros)
  from op_g have g: "g : d ↦⇘ℭ⇙ c" unfolding cat_op_simps by simp
  then have [simp]: "ℭ⦇Dom⦈⦇g⦈ = d" "ℭ⦇Cod⦈⦇g⦈ = c" 
    and d: "d ∈⇩∘ ℭ⦇Obj⦈" and c: "c ∈⇩∘ ℭ⦇Obj⦈"
    by auto
  from f have [simp]: "ℭ⦇Dom⦈⦇f⦈ = c'" "ℭ⦇Cod⦈⦇f⦈ = d'" 
    and c': "c' ∈⇩∘ ℭ⦇Obj⦈" and d': "d' ∈⇩∘ ℭ⦇Obj⦈"
    by auto
  show "vfsequence (cf_hom ℭ gf)" unfolding cf_hom_def by simp
  show vsv_hom_fg: "vsv (cf_hom ℭ gf⦇ArrVal⦈)"
    unfolding cf_hom_components by auto
  show "vcard (cf_hom ℭ gf) = 3⇩ℕ"
    unfolding cf_hom_def by (simp add: nat_omega_simps)
  show [simp]: "𝒟⇩∘ (cf_hom ℭ gf⦇ArrVal⦈) = cf_hom ℭ gf⦇ArrDom⦈"
    unfolding cf_hom_components by auto
  show "ℛ⇩∘ (cf_hom ℭ gf⦇ArrVal⦈) ⊆⇩∘ cf_hom ℭ gf⦇ArrCod⦈"
  proof(rule vsubsetI)
    interpret hom_fg: vsv ‹cf_hom ℭ gf⦇ArrVal⦈› by (simp add: vsv_hom_fg)
    fix y assume "y ∈⇩∘ ℛ⇩∘ (cf_hom ℭ gf⦇ArrVal⦈)"
    then obtain q where y_def: "y = cf_hom ℭ gf⦇ArrVal⦈⦇q⦈" 
      and q: "q ∈⇩∘ 𝒟⇩∘ (cf_hom ℭ gf⦇ArrVal⦈)"
      by (blast dest: hom_fg.vrange_atD)
    from q have q: "q : c ↦⇘ℭ⇙ c'" 
      by (simp add: cf_hom_ArrDom[OF assms[unfolded cc'_def]])
    with g f have "f ∘⇩A⇘ℭ⇙ q ∘⇩A⇘ℭ⇙ g : d ↦⇘ℭ⇙ d'" 
      by (auto intro: cat_cs_intros)
    then show "y ∈⇩∘ cf_hom ℭ gf⦇ArrCod⦈"  
      unfolding cf_hom_ArrCod[OF assms[unfolded dd'_def]]
      unfolding y_def gf_def cf_hom_ArrVal_app[OF op_g q f] 
      by auto
  qed
  from c c' show "cf_hom ℭ gf⦇ArrDom⦈ ∈⇩∘ Vset α"
    unfolding cf_hom_components gf_def
    by (auto simp: nat_omega_simps intro: cat_cs_intros)
  from d d' show "cf_hom ℭ gf⦇ArrCod⦈ ∈⇩∘ Vset α"
    unfolding cf_hom_components gf_def
    by (auto simp: nat_omega_simps intro: cat_cs_intros)
qed auto

lemmas [cat_cs_intros] = category.cat_cf_hom_ArrRel

lemma (in category) cat_cf_hom_cat_Set_is_arr:
  assumes "gf : [a, b]⇩∘ ↦⇘op_cat ℭ ×⇩C ℭ⇙ [c, d]⇩∘"
  shows "cf_hom ℭ gf : Hom ℭ a b ↦⇘cat_Set α⇙ Hom ℭ c d"
proof(intro is_arrI)
  from assms cat_cf_hom_ArrRel show "cf_hom ℭ gf ∈⇩∘ cat_Set α⦇Arr⦈"
    unfolding cat_Set_components by auto
  with assms show 
    "cat_Set α⦇Dom⦈⦇cf_hom ℭ gf⦈ = Hom ℭ a b"
    "cat_Set α⦇Cod⦈⦇cf_hom ℭ gf⦈ = Hom ℭ c d"
    unfolding cat_Set_components
    by (simp_all add: cf_hom_ArrDom[OF assms] cf_hom_ArrCod[OF assms])
qed

lemma (in category) cat_cf_hom_cat_Set_is_arr':
  assumes "gf : [a, b]⇩∘ ↦⇘op_cat ℭ ×⇩C ℭ⇙ [c, d]⇩∘"
    and "𝔄' = Hom ℭ a b"
    and "𝔅' = Hom ℭ c d"
    and "ℭ' = cat_Set α"
  shows "cf_hom ℭ gf : 𝔄' ↦⇘ℭ'⇙ 𝔅'"
  using assms(1) unfolding assms(2-4) by (rule cat_cf_hom_cat_Set_is_arr)

lemmas [cat_cs_intros] = category.cat_cf_hom_cat_Set_is_arr'


subsubsection‹Composition›

lemma (in category) cat_cf_hom_Comp: 
  assumes "g : b ↦⇘op_cat ℭ⇙ c" 
    and "g' : b' ↦⇘ℭ⇙ c'" 
    and "f : a ↦⇘op_cat ℭ⇙ b"
    and "f' : a' ↦⇘ℭ⇙ b'"
  shows 
    "cf_hom ℭ [g, g']⇩∘ ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [f, f']⇩∘ =
      cf_hom ℭ [g ∘⇩A⇘op_cat ℭ⇙ f, g' ∘⇩A⇘ℭ⇙ f']⇩∘"
proof-

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

  from assms(1,3) have g: "g : c ↦⇘ℭ⇙ b" and f: "f : b ↦⇘ℭ⇙ a"
    unfolding cat_op_simps by simp_all

  from assms(2,4) g f Set.category_axioms category_axioms have gg'_ff': 
    "cf_hom ℭ [g, g']⇩∘ ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [f, f']⇩∘ :
      Hom ℭ a a' ↦⇘cat_Set α⇙ Hom ℭ c c'"
    by 
      (
        cs_concl cs_shallow 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
  then have dom_lhs: 
    "𝒟⇩∘ ((cf_hom ℭ [g, g']⇩∘ ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [f, f']⇩∘)⦇ArrVal⦈) = 
      Hom ℭ a a'"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
  from assms(2,4) g f Set.category_axioms category_axioms have gf_g'f':
    "cf_hom ℭ [g ∘⇩A⇘op_cat ℭ⇙ f, g' ∘⇩A⇘ℭ⇙ f']⇩∘ : 
      Hom ℭ a a' ↦⇘cat_Set α⇙ Hom ℭ c c'"
    by (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros)
  then have dom_rhs: 
    "𝒟⇩∘ (cf_hom ℭ [g ∘⇩A⇘op_cat ℭ⇙ f, g' ∘⇩A⇘ℭ⇙ f']⇩∘⦇ArrVal⦈) = Hom ℭ a a'" 
    by (cs_concl cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    
    from gg'_ff' show arr_Set_gg'_ff':
      "arr_Set α (cf_hom ℭ [g, g']⇩∘ ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [f, f']⇩∘)"
      by (auto dest: cat_Set_is_arrD(1))
    from gf_g'f' show arr_Set_gf_g'f':
      "arr_Set α (cf_hom ℭ [g ∘⇩A⇘op_cat ℭ⇙ f, g' ∘⇩A⇘ℭ⇙ f']⇩∘)"
      by (auto dest: cat_Set_is_arrD(1))
  
    show "(cf_hom ℭ [g, g']⇩∘ ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [f, f']⇩∘)⦇ArrVal⦈ = 
      cf_hom ℭ [g ∘⇩A⇘op_cat ℭ⇙ f, g' ∘⇩A⇘ℭ⇙ f']⇩∘⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix q assume "q ∈⇩∘ Hom ℭ a a'"
      then have q: "q : a ↦⇘ℭ⇙ a'" by auto
      from category_axioms g f assms(2,4) q Set.category_axioms show 
        "(cf_hom ℭ [g, g']⇩∘ ∘⇩A⇘cat_Set α⇙ cf_hom ℭ [f, f']⇩∘)⦇ArrVal⦈⦇q⦈ = 
          cf_hom ℭ [g ∘⇩A⇘op_cat ℭ⇙ f, g' ∘⇩A⇘ℭ⇙ f']⇩∘⦇ArrVal⦈⦇q⦈"
        by 
          (
            cs_concl 
              cs_intro: cat_op_intros cat_cs_intros cat_prod_cs_intros 
              cs_simp: cat_op_simps cat_cs_simps   
         )
    qed (use arr_Set_gg'_ff' arr_Set_gf_g'f' in auto)
  
  qed (use gg'_ff' gf_g'f' in ‹cs_concl cs_simp: cat_cs_simps›)+

qed

lemmas [cat_cs_simps] = category.cat_cf_hom_Comp


subsubsection‹Identity›

lemma (in category) cat_cf_hom_CId:
  assumes "[c, c']⇩∘ ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
  shows "cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, ℭ⦇CId⦈⦇c'⦈]⇩∘ = cat_Set α⦇CId⦈⦇Hom ℭ c c'⦈"
proof-

  interpret Set: category α ‹cat_Set α› by (rule category_cat_Set)
  interpret op_ℭ: category α ‹op_cat ℭ› by (rule category_op)

  from assms have op_c: "c ∈⇩∘ op_cat ℭ⦇Obj⦈" and c': "c' ∈⇩∘ ℭ⦇Obj⦈"
    by (auto elim: cat_prod_2_ObjE[rotated 2] intro: cat_cs_intros)
  then have c: "c ∈⇩∘ ℭ⦇Obj⦈" unfolding cat_op_simps by simp

  from c c' category_axioms Set.category_axioms have cf_hom_cc': 
    "cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, ℭ⦇CId⦈⦇c'⦈]⇩∘ : Hom ℭ c c' ↦⇘cat_Set α⇙ Hom ℭ c c'"
    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: "𝒟⇩∘ (cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, ℭ⦇CId⦈⦇c'⦈]⇩∘⦇ArrVal⦈) = Hom ℭ c c'"
    by (cs_concl cs_simp: cat_cs_simps)
  from c c' category_axioms Set.category_axioms have CId_cc':
    "cat_Set α⦇CId⦈⦇Hom ℭ c c'⦈ : Hom ℭ c c' ↦⇘cat_Set α⇙ Hom ℭ c c'"
    by 
      (
        cs_concl  
          cs_simp: cat_Set_cs_simps cat_Set_components(1) 
          cs_intro: cat_cs_intros cat_prod_cs_intros
      )
  then have dom_rhs: "𝒟⇩∘ (cat_Set α⦇CId⦈⦇Hom ℭ c c'⦈⦇ArrVal⦈) = Hom ℭ c c'"    
    by (cs_concl cs_shallow cs_simp: cat_cs_simps )

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    from cf_hom_cc' show arr_Set_CId_cc': 
      "arr_Set α (cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, ℭ⦇CId⦈⦇c'⦈]⇩∘)"
      by (auto dest: cat_Set_is_arrD(1))  
    from CId_cc' show arr_Set_Hom_cc': 
      "arr_Set α (cat_Set α⦇CId⦈⦇Hom ℭ c c'⦈)"
      by (auto simp: cat_Set_is_arrD(1))
    show "cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, ℭ⦇CId⦈⦇c'⦈]⇩∘⦇ArrVal⦈ =
      cat_Set α⦇CId⦈⦇Hom ℭ c c'⦈⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix q assume "q : c ↦⇘ℭ⇙ c'" 
      with category_axioms show
        "cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, ℭ⦇CId⦈⦇c'⦈]⇩∘⦇ArrVal⦈⦇q⦈ = 
          cat_Set α⦇CId⦈⦇Hom ℭ c c'⦈⦇ArrVal⦈⦇q⦈"
        by (*slow*)
          (
            cs_concl 
              cs_simp: cat_cs_simps cat_op_simps cat_Set_cs_simps
              cs_intro: cat_cs_intros
         )
    qed (use arr_Set_CId_cc' arr_Set_Hom_cc' in auto)
  
  qed (use cf_hom_cc' CId_cc' in ‹cs_concl cs_simp: cat_cs_simps›)+

qed

lemmas [cat_cs_simps] = category.cat_cf_hom_CId


subsubsection‹Opposite ‹hom›-function›

lemma (in category) cat_op_cat_cf_hom:
  assumes "g : a ↦⇘ℭ⇙ b" and "g' : a' ↦⇘op_cat ℭ⇙ b'"
  shows "cf_hom (op_cat ℭ) [g, g']⇩∘ = cf_hom ℭ [g', g]⇩∘"
proof(rule arr_Set_eqI[of α])
  from assms show "arr_Set α (cf_hom (op_cat ℭ) [g, g']⇩∘)"
    by 
      ( 
        cs_concl cs_shallow
          cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_prod_cs_intros
      )
  from assms show "arr_Set α (cf_hom ℭ [g', g]⇩∘)"
    by 
      ( 
        cs_concl cs_shallow 
          cs_simp: cat_op_simps 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
  from assms have dom_lhs:
    "𝒟⇩∘ (cf_hom (op_cat ℭ) [g, g']⇩∘⦇ArrVal⦈) = Hom ℭ a' a"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
      )
  from assms have dom_rhs: "𝒟⇩∘ (cf_hom ℭ [g', g]⇩∘⦇ArrVal⦈) = Hom ℭ a' a"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
      )
  show "cf_hom (op_cat ℭ) [g, g']⇩∘⦇ArrVal⦈ = cf_hom ℭ [g', g]⇩∘⦇ArrVal⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
    fix f assume "f : a' ↦⇘ℭ⇙ a"
    with assms show 
      "cf_hom (op_cat ℭ) [g, g']⇩∘⦇ArrVal⦈⦇f⦈ = cf_hom ℭ [g', g]⇩∘⦇ArrVal⦈⦇f⦈"
      unfolding cat_op_simps
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
        )
  qed (simp_all add: cf_hom_components)
  from category_axioms assms show 
    "cf_hom (op_cat ℭ) [g, g']⇩∘⦇ArrDom⦈ = cf_hom ℭ [g', g]⇩∘⦇ArrDom⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: category.cf_hom_ArrDom cat_op_simps 
          cs_intro: cat_op_intros cat_prod_cs_intros
      )
  from category_axioms assms show 
    "cf_hom (op_cat ℭ) [g, g']⇩∘⦇ArrCod⦈ = cf_hom ℭ [g', g]⇩∘⦇ArrCod⦈"
    by 
      (
        cs_concl cs_shallow
          cs_simp: category.cf_hom_ArrCod cat_op_simps 
          cs_intro: cat_op_intros cat_prod_cs_intros
      )
qed

lemmas [cat_cs_simps] = category.cat_op_cat_cf_hom



subsection‹‹Hom›-functor›


subsubsection‹Definition and elementary properties›


text‹
See \<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/hom-functor
}}.
›

definition cf_Hom :: "V ⇒ V ⇒ V" (‹Hom⇩O⇩.⇩Cı_'(/-,-/')›)
  where "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-) = 
    [
      (λa∈⇩∘(op_cat ℭ ×⇩C ℭ)⦇Obj⦈. Hom ℭ (vpfst a) (vpsnd a)),
      (λf∈⇩∘(op_cat ℭ ×⇩C ℭ)⦇Arr⦈. cf_hom ℭ f),
      op_cat ℭ ×⇩C ℭ,
      cat_Set α
    ]⇩∘"


text‹Components.›

lemma cf_Hom_components:
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈ = 
    (λa∈⇩∘(op_cat ℭ ×⇩C ℭ)⦇Obj⦈. Hom ℭ (vpfst a) (vpsnd a))"
    and "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈ = (λf∈⇩∘(op_cat ℭ ×⇩C ℭ)⦇Arr⦈. cf_hom ℭ f)"
    and "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇HomDom⦈ = op_cat ℭ ×⇩C ℭ"
    and "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇HomCod⦈ = cat_Set α"
  unfolding cf_Hom_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda cf_Hom_components(1)
  |vsv cf_Hom_ObjMap_vsv|

lemma cf_Hom_ObjMap_vdomain[cat_cs_simps]:  
  "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈) = (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
  unfolding cf_Hom_components by simp

lemma cf_Hom_ObjMap_app[cat_cs_simps]: 
  assumes "[a, b]⇩∘ ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇a, b⦈⇩∙ = Hom ℭ a b"
  using assms unfolding cf_Hom_components by (simp add: nat_omega_simps)
                
lemma (in category) cf_Hom_ObjMap_vrange: 
  "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈) ⊆⇩∘ cat_Set α⦇Obj⦈"
proof(intro vsubsetI)
  interpret op_ℭ: category α ‹op_cat ℭ› by (simp add: category_op)
  fix y assume "y ∈⇩∘ ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈)"
  then obtain x where y_def: "y = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇x⦈" 
    and x: "x ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
    unfolding cf_Hom_components by auto
  then obtain a b where x_def: "x = [a, b]⇩∘" 
    and a: "a ∈⇩∘ op_cat ℭ⦇Obj⦈" 
    and b: "b ∈⇩∘ ℭ⦇Obj⦈" 
    by (elim cat_prod_2_ObjE[OF op_ℭ.category_axioms category_axioms x])
  from a have a: "a ∈⇩∘ ℭ⦇Obj⦈" unfolding cat_op_simps by simp
  from a b show "y ∈⇩∘ cat_Set α⦇Obj⦈"
    unfolding 
      y_def x_def cf_Hom_ObjMap_app[OF x[unfolded x_def]] cat_Set_components
    by (auto simp: cat_cs_intros)
qed


subsubsection‹Arrow map›

mk_VLambda cf_Hom_components(2)
  |vsv cf_Hom_ArrMap_vsv|
  |vdomain cf_Hom_ArrMap_vdomain[cat_cs_simps]|
  |app cf_Hom_ArrMap_app[cat_cs_simps]|


subsubsection‹‹Hom›-functor is a functor›

lemma (in category) cat_Hom_is_functor:
  "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-) : op_cat ℭ ×⇩C ℭ ↦↦⇩C⇘α⇙ cat_Set α"
proof-

  interpret Set: category α ‹cat_Set α› by (rule category_cat_Set)
  interpret ℭℭ: category α ‹op_cat ℭ ×⇩C ℭ›
    by (simp add: category_axioms category_cat_prod_2 category_op)
  interpret op_ℭ: category α ‹op_cat ℭ› by (rule category_op)

  show ?thesis
  proof(intro is_functorI')

    show "vfsequence Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)"
      unfolding cf_Hom_def by simp
    show op_ℭ_ℭ: "category α (op_cat ℭ ×⇩C ℭ)" by (auto simp: cat_cs_intros)
    show "vcard Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-) = 4⇩ℕ"
      unfolding cf_Hom_def by (simp add: nat_omega_simps)
  
    show "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈) ⊆⇩∘ cat_Set α⦇Obj⦈"
      by (simp add: cf_Hom_ObjMap_vrange)
    show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇gf⦈ :
      Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇ab⦈ ↦⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇cd⦈"
      if gf: "gf : ab ↦⇘op_cat ℭ ×⇩C ℭ⇙ cd" for gf ab cd
      unfolding slicing_simps cat_smc_cat_Set[symmetric]
    proof-
      obtain g f a b c d where gf_def: "gf = [g, f]⇩∘"
        and ab_def: "ab = [a, b]⇩∘"
        and cd_def: "cd = [c, d]⇩∘"   
        and "g : a ↦⇘op_cat ℭ⇙ c"  
        and f: "f : b ↦⇘ℭ⇙ d"
        by (elim cat_prod_2_is_arrE[OF category_op category_axioms gf])
      then have g: "g : c ↦⇘ℭ⇙ a" unfolding cat_op_simps by simp
      from category_axioms that g f show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇gf⦈ :
        Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇ab⦈ ↦⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇cd⦈"
        unfolding gf_def ab_def cd_def (*slow*)
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros)
    qed

    show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇gg' ∘⇩A⇘op_cat ℭ ×⇩C ℭ⇙ ff'⦈ = 
      Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇gg'⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇ff'⦈"
      if gg': "gg' : bb' ↦⇘op_cat ℭ ×⇩C ℭ⇙ cc'" 
        and ff': "ff' : aa' ↦⇘op_cat ℭ ×⇩C ℭ⇙ bb'" 
      for gg' bb' cc' ff' aa'
    proof-
      obtain g g' b b' c c' 
        where gg'_def: "gg' = [g, g']⇩∘"
          and bb'_def: "bb' = [b, b']⇩∘"
          and cc'_def: "cc' = [c, c']⇩∘"   
          and "g : b ↦⇘op_cat ℭ⇙ c"  
          and g': "g' : b' ↦⇘ℭ⇙ c'"
        by (elim cat_prod_2_is_arrE[OF category_op category_axioms gg'])
      moreover obtain f f' a a' b'' b''' 
        where ff'_def: "ff' = [f, f']⇩∘"
          and aa'_def: "aa' = [a, a']⇩∘"
          and "bb' = [b'', b''']⇩∘"   
          and "f : a ↦⇘op_cat ℭ⇙ b''"  
          and "f' : a' ↦⇘ℭ⇙ b'''"
        by (elim cat_prod_2_is_arrE[OF category_op category_axioms ff'])
      ultimately have f: "f : b ↦⇘ℭ⇙ a" 
        and f': "f' : a' ↦⇘ℭ⇙ b'" 
        and g: "g : c ↦⇘ℭ⇙ b"
        by (auto simp: cat_op_simps)
      from category_axioms that g f  g' f' show ?thesis
        unfolding 
          slicing_simps cat_smc_cat_Set[symmetric] 
          gg'_def bb'_def cc'_def ff'_def aa'_def
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps cat_prod_cs_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed

    show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇(op_cat ℭ ×⇩C ℭ)⦇CId⦈⦇cc'⦈⦈ = 
      cat_Set α⦇CId⦈⦇Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇cc'⦈⦈"
      if "cc' ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈" for cc'
    proof-
      from that obtain c c' 
        where cc'_def: "cc' = [c, c']⇩∘" 
          and c: "c ∈⇩∘ op_cat ℭ⦇Obj⦈"
          and c': "c' ∈⇩∘ ℭ⦇Obj⦈"
        by (elim cat_prod_2_ObjE[rotated 2]) (auto intro: cat_cs_intros)
      then have c: "c ∈⇩∘ ℭ⦇Obj⦈" unfolding cat_op_simps by simp
      with c' category_axioms Set.category_axioms that show ?thesis
        unfolding cc'_def
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps cat_prod_cs_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed

  qed (auto simp: cf_Hom_components cat_cs_intros)

qed

lemma (in category) cat_Hom_is_functor':
  assumes "β = α" and "𝔄' = op_cat ℭ ×⇩C ℭ" and "𝔅' = cat_Set α"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-) : 𝔄' ↦↦⇩C⇘β⇙ 𝔅'"
  unfolding assms by (rule cat_Hom_is_functor)

lemmas [cat_cs_intros] = category.cat_Hom_is_functor'



subsection‹Composition of a ‹Hom›-functor and two functors›


subsubsection‹Definition and elementary properties›

definition cf_bcomp_Hom :: "V ⇒ V ⇒ V ⇒ V ⇒ V" (‹Hom⇩O⇩.⇩Cı_'(/_-,_-/')›)
  ―‹The following definition may seem redundant, but it will help to avoid
  proof duplication later.›
  where "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-) = cf_cn_cov_bcomp (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)) 𝔉 𝔊"


subsubsection‹Object map›

lemma cf_bcomp_Hom_ObjMap_vsv: "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ObjMap⦈)"
  unfolding cf_bcomp_Hom_def by (rule cf_cn_cov_bcomp_ObjMap_vsv)

lemma cf_bcomp_Hom_ObjMap_vdomain[cat_cs_simps]:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ObjMap⦈) = (op_cat 𝔄 ×⇩C 𝔅)⦇Obj⦈"
  using assms unfolding cf_bcomp_Hom_def by (rule cf_cn_cov_bcomp_ObjMap_vdomain)

lemma cf_bcomp_Hom_ObjMap_app[cat_cs_simps]:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "[a, b]⇩∘ ∈⇩∘ (op_cat 𝔄 ×⇩C 𝔅)⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ObjMap⦈⦇a, b⦈⇩∙ = 
    Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈, 𝔊⦇ObjMap⦈⦇b⦈⦈⇩∙"
  using assms unfolding cf_bcomp_Hom_def by (rule cf_cn_cov_bcomp_ObjMap_app)
  
lemma (in category) cf_bcomp_Hom_ObjMap_vrange:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ObjMap⦈) ⊆⇩∘ cat_Set α⦇Obj⦈"
  using category_axioms
  unfolding cf_bcomp_Hom_def
  by (intro cf_cn_cov_bcomp_ObjMap_vrange[OF assms])
    (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)


subsubsection‹Arrow map›

lemma cf_bcomp_Hom_ArrMap_vsv: "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ArrMap⦈)"
  unfolding cf_bcomp_Hom_def by (rule cf_cn_cov_bcomp_ArrMap_vsv)

lemma cf_bcomp_Hom_ArrMap_vdomain[cat_cs_simps]:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ArrMap⦈) = (op_cat 𝔄 ×⇩C 𝔅)⦇Arr⦈"
  using assms 
  unfolding cf_bcomp_Hom_def 
  by (rule cf_cn_cov_bcomp_ArrMap_vdomain)

lemma cf_bcomp_Hom_ArrMap_app[cat_cs_simps]:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "[f, g]⇩∘ ∈⇩∘ (op_cat 𝔄 ×⇩C 𝔅)⦇Arr⦈"
  shows 
    "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ArrMap⦈⦇f, g⦈⇩∙ = 
      Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈, 𝔊⦇ArrMap⦈⦇g⦈⦈⇩∙"
  using assms 
  unfolding cf_bcomp_Hom_def 
  by (rule cf_cn_cov_bcomp_ArrMap_app)

lemma (in category) cf_bcomp_Hom_ArrMap_vrange:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-)⦇ArrMap⦈) ⊆⇩∘ cat_Set α⦇Arr⦈"
  using category_axioms
  unfolding cf_bcomp_Hom_def
  by (intro cf_cn_cov_bcomp_ArrMap_vrange[OF assms])
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )


subsubsection‹Composition of a ‹Hom›-functor and two functors is a functor›

lemma (in category) cat_cf_bcomp_Hom_is_functor:
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-) : op_cat 𝔄 ×⇩C 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
  using assms category_axioms
  unfolding cf_bcomp_Hom_def
  by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

lemma (in category) cat_cf_bcomp_Hom_is_functor':
  assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ" 
    and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "β = α"
    and "𝔄' = op_cat 𝔄 ×⇩C 𝔅"
    and "𝔅' = cat_Set α"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,𝔊-) : 𝔄' ↦↦⇩C⇘β⇙ 𝔅'"
  using assms(1,2) unfolding assms(3-5) by (rule cat_cf_bcomp_Hom_is_functor)

lemmas [cat_cs_intros] = category.cat_cf_bcomp_Hom_is_functor'



subsection‹Composition of a ‹Hom›-functor and a functor›


subsubsection‹Definition and elementary properties›


text‹See subsection 1.15 in \<^cite>‹"bodo_categories_1970"›.›

definition cf_lcomp_Hom :: "V ⇒ V ⇒ V ⇒ V" (‹Hom⇩O⇩.⇩Cı_'(/_-,-/')›)
  where "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-) = cf_cn_cov_lcomp ℭ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)) 𝔉"

definition cf_rcomp_Hom :: "V ⇒ V ⇒ V ⇒ V" (‹Hom⇩O⇩.⇩Cı_'(/-,_-/')›)
  where "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) = cf_cn_cov_rcomp ℭ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)) 𝔊"


subsubsection‹Object map›

lemma cf_lcomp_Hom_ObjMap_vsv[cat_cs_intros]: "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ObjMap⦈)"
  unfolding cf_lcomp_Hom_def by (rule cf_cn_cov_lcomp_ObjMap_vsv)

lemma cf_rcomp_Hom_ObjMap_vsv[cat_cs_intros]: "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈)"
  unfolding cf_rcomp_Hom_def by (rule cf_cn_cov_rcomp_ObjMap_vsv)

lemma cf_lcomp_Hom_ObjMap_vdomain[cat_cs_simps]:
  assumes "category α ℭ" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ObjMap⦈) = (op_cat 𝔅 ×⇩C ℭ)⦇Obj⦈"
  using assms
  by 
    ( 
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cf_lcomp_Hom_def cs_intro: cat_cs_intros
    )

lemma cf_rcomp_Hom_ObjMap_vdomain[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈) = (op_cat ℭ ×⇩C 𝔅)⦇Obj⦈"
  using assms
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cf_rcomp_Hom_def cs_intro: cat_cs_intros
    )

lemma cf_lcomp_Hom_ObjMap_app[cat_cs_simps]:
  assumes "category α ℭ"
    and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "b ∈⇩∘ op_cat 𝔅⦇Obj⦈"
    and "c ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ObjMap⦈⦇b, c⦈⇩∙ = 
    Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇b⦈, c⦈⇩∙"
  using assms
  unfolding cf_lcomp_Hom_def
  by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_prod_cs_intros)

lemma cf_rcomp_Hom_ObjMap_app[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "c ∈⇩∘ op_cat ℭ⦇Obj⦈"
    and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈⦇c, b⦈⇩∙ =
    Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇c, 𝔊⦇ObjMap⦈⦇b⦈⦈⇩∙"
  using assms
  by 
    (
      cs_concl cs_shallow
        cs_simp: cat_cs_simps cf_rcomp_Hom_def
        cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
    )

lemma (in category) cat_cf_lcomp_Hom_ObjMap_vrange: 
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ObjMap⦈) ⊆⇩∘ cat_Set α⦇Obj⦈"
  using category_axioms assms
  unfolding cf_lcomp_Hom_def
  by (intro cf_cn_cov_lcomp_ObjMap_vrange) 
    (cs_concl cs_shallow cs_intro: cat_cs_intros)

lemma (in category) cat_cf_rcomp_Hom_ObjMap_vrange: 
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈) ⊆⇩∘ cat_Set α⦇Obj⦈"
  using category_axioms assms
  unfolding cf_rcomp_Hom_def  
  by (intro cf_cn_cov_rcomp_ObjMap_vrange) 
    (cs_concl cs_shallow cs_intro: cat_cs_intros)


subsubsection‹Arrow map›

lemma cf_lcomp_Hom_ArrMap_vsv[cat_cs_intros]: "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ArrMap⦈)"
  unfolding cf_lcomp_Hom_def by (rule cf_cn_cov_lcomp_ArrMap_vsv)

lemma cf_rcomp_Hom_ArrMap_vsv[cat_cs_intros]: "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈)"
  unfolding cf_rcomp_Hom_def by (rule cf_cn_cov_rcomp_ArrMap_vsv)

lemma cf_lcomp_Hom_ArrMap_vdomain[cat_cs_simps]:  
  assumes "category α ℭ" and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ArrMap⦈) = (op_cat 𝔅 ×⇩C ℭ)⦇Arr⦈"
  using assms
  unfolding cf_lcomp_Hom_def
  by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

lemma cf_rcomp_Hom_ArrMap_vdomain[cat_cs_simps]:  
  assumes "category α ℭ" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈) = (op_cat ℭ ×⇩C 𝔅)⦇Arr⦈"
  using assms
  unfolding cf_rcomp_Hom_def 
  by (cs_concl cs_shallow cs_simp: cat_cs_simps)

lemma cf_lcomp_Hom_ArrMap_app[cat_cs_simps]:
  assumes "category α ℭ" 
    and "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "g : a ↦⇘op_cat 𝔅⇙ b"
    and "f : a' ↦⇘ℭ⇙ b'"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ArrMap⦈⦇g, f⦈⇩∙ =
    Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇g⦈, f⦈⇩∙"
  using assms
  unfolding cf_lcomp_Hom_def cat_op_simps 
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cat_op_simps 
        cs_intro: cat_cs_intros cat_prod_cs_intros
    )

lemma cf_rcomp_Hom_ArrMap_app[cat_cs_simps]:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
    and "g : a ↦⇘op_cat ℭ⇙ b"
    and "f : a' ↦⇘𝔅⇙ b'"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈⦇g, f⦈⇩∙ =
    Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈⦇g, 𝔊⦇ArrMap⦈⦇f⦈⦈⇩∙"
  using assms 
  by
    (
      cs_concl 
        cs_simp: cat_cs_simps cf_rcomp_Hom_def
        cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
    )

lemma (in category) cf_lcomp_Hom_ArrMap_vrange: 
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⦇ArrMap⦈) ⊆⇩∘ cat_Set α⦇Arr⦈"
  using category_axioms assms
  unfolding cf_lcomp_Hom_def
  by (intro cf_cn_cov_lcomp_ArrMap_vrange)
    (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

lemma (in category) cf_rcomp_Hom_ArrMap_vrange: 
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "ℛ⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈) ⊆⇩∘ cat_Set α⦇Arr⦈"
  using category_axioms assms
  unfolding cf_rcomp_Hom_def
  by (intro cf_cn_cov_rcomp_ArrMap_vrange)
    (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)


subsubsection‹Further properties›

lemma cf_bcomp_Hom_cf_lcomp_Hom[cat_cs_simps]:
  "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,cf_id ℭ-) = Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)"
  unfolding cf_lcomp_Hom_def cf_cn_cov_lcomp_def cf_bcomp_Hom_def ..

lemma cf_bcomp_Hom_cf_rcomp_Hom[cat_cs_simps]:
  "Hom⇩O⇩.⇩C⇘α⇙ℭ(cf_id ℭ-,𝔊-) = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)"
  unfolding cf_rcomp_Hom_def cf_cn_cov_rcomp_def cf_bcomp_Hom_def ..


subsubsection‹Composition of a ‹Hom›-functor and a functor is a functor›

lemma (in category) cat_cf_lcomp_Hom_is_functor:
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-) : op_cat 𝔅 ×⇩C ℭ ↦↦⇩C⇘α⇙ cat_Set α"
  using category_axioms assms
  unfolding cf_lcomp_Hom_def
  by (intro cf_cn_cov_lcomp_is_functor) 
    (cs_concl cs_shallow cs_intro: cat_cs_intros)

lemma (in category) cat_cf_lcomp_Hom_is_functor':
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" 
    and "β = α" 
    and "𝔄' = op_cat 𝔅 ×⇩C ℭ" 
    and "𝔅' = cat_Set α"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-) : 𝔄' ↦↦⇩C⇘β⇙ 𝔅'"
  using assms(1) 
  unfolding assms(2-4) 
  by (rule cat_cf_lcomp_Hom_is_functor) 

lemmas [cat_cs_intros] = category.cat_cf_lcomp_Hom_is_functor'

lemma (in category) cat_cf_rcomp_Hom_is_functor:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) : op_cat ℭ ×⇩C 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
  using category_axioms assms
  unfolding cf_rcomp_Hom_def
  by (intro cf_cn_cov_rcomp_is_functor) 
    (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)

lemma (in category) cat_cf_rcomp_Hom_is_functor':
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "β = α" 
    and "𝔄' = op_cat ℭ ×⇩C 𝔅" 
    and "𝔅' = cat_Set α"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) : 𝔄' ↦↦⇩C⇘β⇙ 𝔅'"
  using assms(1) 
  unfolding assms(2-4) 
  by (rule cat_cf_rcomp_Hom_is_functor) 

lemmas [cat_cs_intros] = category.cat_cf_rcomp_Hom_is_functor'


subsubsection‹Flip of a projections of a ‹Hom›-functor›

lemma (in category) cat_bifunctor_flip_cf_rcomp_Hom:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows 
    "bifunctor_flip (op_cat ℭ) 𝔅 (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)) =
      Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)"
proof(rule cf_eqI)

  interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms)

  from category_axioms assms show bf_Hom:
    "bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) :
      𝔅 ×⇩C op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from category_axioms assms show op_Hom:
    "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-) : 𝔅 ×⇩C op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_op_intros
      )
  from bf_Hom have ObjMap_dom_lhs:
    "𝒟⇩∘ (bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈) = 
      (𝔅 ×⇩C op_cat ℭ)⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  from op_Hom have ObjMap_dom_rhs:
    "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ObjMap⦈) = (𝔅 ×⇩C op_cat ℭ)⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  from bf_Hom have ArrMap_dom_lhs:
    "𝒟⇩∘ (bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈) = 
      (𝔅 ×⇩C op_cat ℭ)⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  from op_Hom have ArrMap_dom_rhs:
    "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ArrMap⦈) = (𝔅 ×⇩C op_cat ℭ)⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps)

  show 
    "bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈ =
      Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ObjMap⦈"
  proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
    fix bc assume "bc ∈⇩∘ (𝔅 ×⇩C op_cat ℭ)⦇Obj⦈"
    then obtain b c 
      where bc_def: "bc = [b, c]⇩∘" and b: "b ∈⇩∘ 𝔅⦇Obj⦈" and c: "c ∈⇩∘ ℭ⦇Obj⦈"
      by 
        (
          auto 
            elim: cat_prod_2_ObjE[OF 𝔊.HomDom.category_axioms category_op] 
            simp: cat_op_simps
        )
    from category_axioms assms b c show 
      "bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈⦇bc⦈ =
        Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ObjMap⦈⦇bc⦈"
      unfolding bc_def
      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 (auto intro: cat_cs_intros)

  show 
    "bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈ =
      Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
    fix gf assume "gf ∈⇩∘ (𝔅 ×⇩C op_cat ℭ)⦇Arr⦈"
    then obtain g f 
      where gf_def: "gf = [g, f]⇩∘" and "g ∈⇩∘ 𝔅⦇Arr⦈" and "f ∈⇩∘ ℭ⦇Arr⦈"
      by 
        (
          auto 
            elim: cat_prod_2_ArrE[OF 𝔊.HomDom.category_axioms category_op] 
            simp: cat_op_simps
        )
    then obtain a b c d where g: "g : a ↦⇘𝔅⇙ b" and f: "f : c ↦⇘ℭ⇙ d"
      by (auto intro!: is_arrI)
    from category_axioms assms g f show 
      "bifunctor_flip (op_cat ℭ) 𝔅 Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈⦇gf⦈ =
        Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ArrMap⦈⦇gf⦈"
      unfolding gf_def
      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 (auto intro: cat_cs_intros)

qed (auto intro: cat_cs_intros simp: cat_op_simps)

lemmas [cat_cs_simps] = category.cat_bifunctor_flip_cf_rcomp_Hom 

lemma (in category) cat_bifunctor_flip_cf_lcomp_Hom:
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
  shows 
    "bifunctor_flip (op_cat 𝔅) ℭ (Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)) =
      Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(-,op_cf 𝔉-)"
proof-
  interpret 𝔉: is_functor α 𝔅 ℭ 𝔉 by (rule assms(1))
  note Hom_𝔉 = 
    category.cat_bifunctor_flip_cf_rcomp_Hom
      [
        OF category_op is_functor_op[OF assms], 
        unfolded cat_op_simps, 
        symmetric
      ]
  from category_axioms assms show ?thesis
    by (subst Hom_𝔉)
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_op_intros
      )+
qed

lemmas [cat_cs_simps] = category.cat_bifunctor_flip_cf_lcomp_Hom



subsection‹Projections of the ‹Hom›-functor›


text‹
The projections of the ‹Hom›-functor coincide with the definitions
of the ‹Hom›-functor given in Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.
They are also exposed in the aforementioned article in 
nLab \<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/hom-functor
}}.
›


subsubsection‹Definitions and elementary properties›

definition cf_Hom_snd :: "V ⇒ V ⇒ V ⇒ V" (‹Hom⇩O⇩.⇩Cı_'(/_,-/')›)
  where "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⇘op_cat ℭ,ℭ⇙(a,-)⇩C⇩F"
definition cf_Hom_fst :: "V ⇒ V ⇒ V ⇒ V" (‹Hom⇩O⇩.⇩Cı_'(/-,_/')›)
  where "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b) = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⇘op_cat ℭ,ℭ⇙(-,b)⇩C⇩F"


subsubsection‹Projections of the ‹Hom›-functor are functors›

lemma (in category) cat_cf_Hom_snd_is_functor:
  assumes "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
proof-  
  from assms have a: "a ∈⇩∘ op_cat ℭ⦇Obj⦈" unfolding cat_op_simps by simp
  have op_ℭ: "category α (op_cat ℭ)" by (auto intro: cat_cs_intros)
  from op_ℭ category_axioms cat_Hom_is_functor a show ?thesis
    unfolding cf_Hom_snd_def by (rule bifunctor_proj_snd_is_functor)
qed

lemma (in category) cat_cf_Hom_snd_is_functor':
  assumes "a ∈⇩∘ ℭ⦇Obj⦈" and "β = α" and "ℭ' = ℭ" and "𝔇' = cat_Set α"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) : ℭ' ↦↦⇩C⇘β⇙ 𝔇'"
  using assms(1) unfolding assms(2-4) by (rule cat_cf_Hom_snd_is_functor)

lemmas [cat_cs_intros] = category.cat_cf_Hom_snd_is_functor'

lemma (in category) cat_cf_Hom_fst_is_functor:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b) : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
proof-  
  have op_ℭ: "category α (op_cat ℭ)" by (auto intro: cat_cs_intros)
  from op_ℭ category_axioms cat_Hom_is_functor assms show ?thesis
    unfolding cf_Hom_fst_def by (rule bifunctor_proj_fst_is_functor)
qed

lemma (in category) cat_cf_Hom_fst_is_functor':
  assumes "b ∈⇩∘ ℭ⦇Obj⦈" and "β = α" and "ℭ' = op_cat ℭ" and "𝔇' = cat_Set α"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b) : ℭ' ↦↦⇩C⇘β⇙ 𝔇'"
  using assms(1) unfolding assms(2-4) by (rule cat_cf_Hom_fst_is_functor)

lemmas [cat_cs_intros] = category.cat_cf_Hom_fst_is_functor'


subsubsection‹Object maps›

lemma (in category) cat_cf_Hom_snd_ObjMap_vsv[cat_cs_intros]:
  assumes "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ObjMap⦈)"
  unfolding cf_Hom_snd_def
  using category_axioms assms
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_intros] = category.cat_cf_Hom_snd_ObjMap_vsv

lemma (in category) cat_cf_Hom_fst_ObjMap_vsv[cat_cs_intros]:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ObjMap⦈)"
  unfolding cf_Hom_fst_def
  using category_axioms assms
  by
    (
      cs_concl cs_shallow
        cs_simp: cat_prod_cs_simps cat_cs_simps
        cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
    )

lemmas [cat_cs_intros] = category.cat_cf_Hom_fst_ObjMap_vsv

lemma (in category) cat_cf_Hom_snd_ObjMap_vdomain[cat_cs_simps]:
  assumes "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ObjMap⦈) = ℭ⦇Obj⦈"
  using category_axioms assms
  unfolding cf_Hom_snd_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_simps] = category.cat_cf_Hom_snd_ObjMap_vdomain

lemma (in category) cat_cf_Hom_fst_ObjMap_vdomain[cat_cs_simps]:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ObjMap⦈) = op_cat ℭ⦇Obj⦈"
  using category_axioms assms
  unfolding cf_Hom_fst_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_simps] = category.cat_cf_Hom_fst_ObjMap_vdomain

lemma (in category) cat_cf_Hom_snd_ObjMap_app[cat_cs_simps]:
  assumes "a ∈⇩∘ op_cat ℭ⦇Obj⦈" and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ObjMap⦈⦇b⦈ = Hom ℭ a b"
proof-
  from assms have ab: "[a, b]⇩∘ ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
    by (intro cat_prod_2_ObjI) (auto intro: cat_cs_intros)
  show ?thesis
    unfolding 
      cf_Hom_snd_def
      bifunctor_proj_snd_ObjMap_app[OF category_op category_axioms ab]
      cf_Hom_ObjMap_app[OF ab]
      ..
qed

lemmas [cat_cs_simps] = category.cat_cf_Hom_snd_ObjMap_app

lemma (in category) cat_cf_Hom_fst_ObjMap_app[cat_cs_simps]:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈" and "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ObjMap⦈⦇a⦈ = Hom ℭ a b"
proof-
  from assms have ab: "[a, b]⇩∘ ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
    by (intro cat_prod_2_ObjI) (auto intro: cat_cs_intros)
  show ?thesis
    unfolding 
      cf_Hom_fst_def
      bifunctor_proj_fst_ObjMap_app[OF category_op category_axioms ab]
      cf_Hom_ObjMap_app[OF ab]
      ..
qed

lemmas [cat_cs_simps] = category.cat_cf_Hom_fst_ObjMap_app


subsubsection‹Arrow maps›

lemma (in category) cat_cf_Hom_snd_ArrMap_vsv[cat_cs_intros]:
  assumes "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
  shows "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ArrMap⦈)"
  unfolding cf_Hom_snd_def
  using category_axioms assms
  by
    (
      cs_concl cs_shallow
        cs_simp: cat_cs_simps 
        cs_intro: bifunctor_proj_snd_ArrMap_vsv cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_intros] = category.cat_cf_Hom_snd_ArrMap_vsv

lemma (in category) cat_cf_Hom_fst_ArrMap_vsv[cat_cs_intros]:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ArrMap⦈)"
  unfolding cf_Hom_fst_def
  using category_axioms assms
  by
    (
      cs_concl cs_shallow
        cs_simp: cat_cs_simps
        cs_intro: bifunctor_proj_fst_ArrMap_vsv cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_intros] = category.cat_cf_Hom_fst_ArrMap_vsv

lemma (in category) cat_cf_Hom_snd_ArrMap_vdomain[cat_cs_simps]:
  assumes "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ArrMap⦈) = ℭ⦇Arr⦈"
  using category_axioms assms
  unfolding cf_Hom_snd_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_simps] = category.cat_cf_Hom_snd_ArrMap_vdomain

lemma (in category) cat_cf_Hom_fst_ArrMap_vdomain[cat_cs_simps]:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ArrMap⦈) = op_cat ℭ⦇Arr⦈"
  using category_axioms assms
  unfolding cf_Hom_fst_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_simps] = category.cat_cf_Hom_fst_ArrMap_vdomain

lemma (in category) cat_cf_Hom_snd_ArrMap_app[cat_cs_simps]:
  assumes "a ∈⇩∘ op_cat ℭ⦇Obj⦈" and "f : b ↦⇘ℭ⇙ b'"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ArrMap⦈⦇f⦈ = cf_hom ℭ [op_cat ℭ⦇CId⦈⦇a⦈, f]⇩∘"
proof-
  from assms(2) have f: "f ∈⇩∘ ℭ⦇Arr⦈" by (simp add: cat_cs_intros)
  from category_axioms assms show ?thesis
    unfolding 
      cf_Hom_snd_def
      bifunctor_proj_snd_ArrMap_app[OF category_op category_axioms assms(1) f]
      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

lemmas [cat_cs_simps] = category.cat_cf_Hom_snd_ArrMap_app

lemma (in category) cat_cf_Hom_fst_ArrMap_app[cat_cs_simps]:
  assumes "b ∈⇩∘ ℭ⦇Obj⦈" and "f : a ↦⇘op_cat ℭ⇙ a'"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ArrMap⦈⦇f⦈ = cf_hom ℭ [f, ℭ⦇CId⦈⦇b⦈]⇩∘"
proof-
  from assms(2) have f: "f ∈⇩∘ op_cat ℭ⦇Arr⦈" by (simp add: cat_cs_intros)
  with category_axioms assms show ?thesis
    unfolding 
      cf_Hom_fst_def
      bifunctor_proj_fst_ArrMap_app[OF category_op category_axioms assms(1) f]
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
qed

lemmas [cat_cs_simps] = category.cat_cf_Hom_fst_ArrMap_app


subsubsection‹Opposite ‹Hom›-functor projections›

lemma (in category) cat_op_cat_cf_Hom_snd:
  assumes "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-) = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)"
proof(rule cf_eqI[of α])

  from assms category_axioms show 
    "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-) : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"  
    by
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps cat_op_simps   
          cs_intro: cat_cs_intros cat_op_intros
      )
  from assms category_axioms show 
    "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a) : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cat_op_simps   
          cs_intro: cat_cs_intros cat_op_intros
      )

  show "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ObjMap⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ObjMap⦈"
  proof(rule vsv_eqI)
    from assms category_axioms show "vsv (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ObjMap⦈)"
      by (intro is_functor.cf_ObjMap_vsv)
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
    from assms category_axioms show "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ObjMap⦈)"
      by (intro is_functor.cf_ObjMap_vsv)
        (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms category_axioms show 
      "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ObjMap⦈) = 𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ObjMap⦈)"
      by
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps   
            cs_intro: cat_cs_intros cat_op_intros
        )
    show "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ObjMap⦈⦇b⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ObjMap⦈⦇b⦈"
      if "b ∈⇩∘ 𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ObjMap⦈)" for b
    proof-
      from that have "b ∈⇩∘ ℭ⦇Obj⦈"
        by 
          (
            simp add: 
              category.cat_cf_Hom_snd_ObjMap_vdomain[
                OF category_op, unfolded cat_op_simps, OF assms
                ]
          )
      from category_axioms assms this show ?thesis
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_op_intros
          )
    qed
  qed
  
  show "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ArrMap⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ArrMap⦈"
  proof(rule vsv_eqI)
    from assms category_axioms show "vsv (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ArrMap⦈)"
      by (intro is_functor.cf_ArrMap_vsv)
        (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
    from assms category_axioms show "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ArrMap⦈)"
      by (intro is_functor.cf_ArrMap_vsv)
        (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms category_axioms show 
      "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ArrMap⦈) = 𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ArrMap⦈)"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_op_intros
        )
    show "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ArrMap⦈⦇f⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ArrMap⦈⦇f⦈"
      if "f ∈⇩∘ 𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(a,-)⦇ArrMap⦈)" for f
    proof-
      from that have "f ∈⇩∘ ℭ⦇Arr⦈"
        by 
          (
            simp add: 
              category.cat_cf_Hom_snd_ArrMap_vdomain[
                OF category_op, unfolded cat_op_simps, OF assms
                ]
          )
      then obtain a b where "f : a ↦⇘ℭ⇙ b" by auto
      from category_axioms assms this show ?thesis
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros cat_op_intros
          )
    qed
  qed

qed simp_all

lemmas [cat_op_simps] = category.cat_op_cat_cf_Hom_snd

lemma (in category) cat_op_cat_cf_Hom_fst:
  assumes "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(-,a) = Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)"
proof-
  from assms have a: "a ∈⇩∘ op_cat ℭ⦇Obj⦈" unfolding cat_op_simps .
  have "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) = Hom⇩O⇩.⇩C⇘α⇙op_cat (op_cat ℭ)(a,-)" 
    unfolding cat_op_simps ..
  also have "… = Hom⇩O⇩.⇩C⇘α⇙(op_cat ℭ)(-,a)"
    unfolding category.cat_op_cat_cf_Hom_snd[OF category_op a] by simp
  finally show "Hom⇩O⇩.⇩C⇘α⇙(op_cat ℭ)(-,a) = Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)" by simp
qed

lemmas [cat_op_simps] = category.cat_op_cat_cf_Hom_fst


subsubsection‹‹Hom›-functors are injections on objects›

lemma (in category) cat_cf_Hom_snd_inj:
  assumes "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) = Hom⇩O⇩.⇩C⇘α⇙ℭ(b,-)" 
    and "a ∈⇩∘ ℭ⦇Obj⦈"
    and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "a = b"
proof(rule ccontr)
  assume prems: "a ≠ b"
  from assms(1) have "Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-)⦇ObjMap⦈⦇b⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(b,-)⦇ObjMap⦈⦇b⦈" 
    by simp
  then have "Hom ℭ a b = Hom ℭ b b"
    unfolding 
      cat_cf_Hom_snd_ObjMap_app[unfolded cat_op_simps, OF assms(2,3)]
      cat_cf_Hom_snd_ObjMap_app[unfolded cat_op_simps, OF assms(3,3)]
    by simp
  with assms prems show False by (force intro: cat_cs_intros)
qed

lemma (in category) cat_cf_Hom_fst_inj:
  assumes "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a) = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)" and "a ∈⇩∘ ℭ⦇Obj⦈" and "b ∈⇩∘ ℭ⦇Obj⦈"
  shows "a = b"
proof(rule ccontr)
  assume prems: "a ≠ b"
  from assms(1) have "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,a)⦇ObjMap⦈⦇b⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,b)⦇ObjMap⦈⦇b⦈" 
    by simp
  then have "Hom ℭ b a = Hom ℭ b b"
    unfolding 
      cat_cf_Hom_fst_ObjMap_app[unfolded cat_op_simps, OF assms(2,3)]
      cat_cf_Hom_fst_ObjMap_app[unfolded cat_op_simps, OF assms(3,3)]
    by simp
  with assms prems show False by (force intro: cat_cs_intros)
qed


subsubsection‹‹Hom›-functor is an array bifunctor›

lemma (in category) cat_cf_Hom_is_cf_array:
  ―‹See Chapter II-3 in \cite{mac_lane_categories_2010}.›
  "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-) =
    cf_array (op_cat ℭ) ℭ (cat_Set α) (cf_Hom_fst α ℭ) (cf_Hom_snd α ℭ)"
proof(rule cf_eqI[of α])

  show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-) : op_cat ℭ ×⇩C ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by (rule cat_Hom_is_functor)

  have c1: "category α (op_cat ℭ)" by (auto intro: cat_cs_intros)
  have c2: "category α ℭ" by (auto intro: cat_cs_intros)
  have c3: "category α (cat_Set α)" by (simp add: category_cat_Set)
  have c4: "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c) : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    if "c ∈⇩∘ ℭ⦇Obj⦈" for c
    using that by (rule cat_cf_Hom_fst_is_functor)
  have c5: "Hom⇩O⇩.⇩C⇘α⇙ℭ(b,-) : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    if "b ∈⇩∘ op_cat ℭ⦇Obj⦈" for b
    using that unfolding cat_op_simps by (rule cat_cf_Hom_snd_is_functor)
  have c6: "Hom⇩O⇩.⇩C⇘α⇙ℭ(b,-)⦇ObjMap⦈⦇c⦈ = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c)⦇ObjMap⦈⦇b⦈"
    if "b ∈⇩∘ op_cat ℭ⦇Obj⦈" and "c ∈⇩∘ ℭ⦇Obj⦈" for b c
    using that category_axioms
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  have c7: 
    "Hom⇩O⇩.⇩C⇘α⇙ℭ(b',-)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c)⦇ArrMap⦈⦇f⦈ =
      Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c' )⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙ℭ(b,- )⦇ArrMap⦈⦇g⦈"
    if "f : b ↦⇘op_cat ℭ⇙ b'" and "g : c ↦⇘ℭ⇙ c'" for b c  b'  c' f g 
    using that category_axioms 
    unfolding cat_op_simps
    by 
      (
        cs_concl  
          cs_simp: cat_cs_simps cat_op_simps 
          cs_intro: cat_cs_intros cat_op_intros
      )
  
  let ?cfa =
    ‹cf_array (op_cat ℭ) ℭ (cat_Set α) (cf_Hom_fst α ℭ) (cf_Hom_snd α ℭ)›

  note cf_array_specification = 
    cf_array_specification[OF c1 c2 c3 c4 c5 c6 c7, simplified]

  from c1 c2 c3 c4 c5 c6 c7 show "?cfa : op_cat ℭ ×⇩C ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by (rule cf_array_is_functor)

  show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈ = ?cfa⦇ObjMap⦈"
  proof(rule vsv_eqI, unfold cat_cs_simps)
    fix aa' assume "aa' ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Obj⦈"
    then obtain a a' 
      where aa'_def: "aa' = [a, a']⇩∘" 
        and a: "a ∈⇩∘ op_cat ℭ⦇Obj⦈" 
        and a': "a' ∈⇩∘ ℭ⦇Obj⦈"
      by (elim cat_prod_2_ObjE[OF c1 c2])
    from category_axioms a a' show 
      "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ObjMap⦈⦇aa'⦈ = ?cfa⦇ObjMap⦈⦇aa'⦈"
      unfolding aa'_def cf_array_specification(2)[OF a a'] cat_op_simps
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cs_intro: cat_op_intros cat_prod_cs_intros
        )
  qed (auto simp: cf_array_ObjMap_vsv cf_Hom_ObjMap_vsv cat_cs_simps)

  show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,-)⦇ArrMap⦈ = ?cfa⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold cat_cs_simps)
    fix ff' assume "ff' ∈⇩∘ (op_cat ℭ ×⇩C ℭ)⦇Arr⦈"
    then obtain f f' 
      where ff'_def: "ff' = [f, f']⇩∘" 
        and f: "f ∈⇩∘ op_cat ℭ⦇Arr⦈" 
        and f': "f' ∈⇩∘ ℭ⦇Arr⦈"
      by (elim cat_prod_2_ArrE[OF c1 c2])
    then obtain a b a' b' 
      where f: "f : a ↦⇘op_cat ℭ⇙ b" and f': "f' : a' ↦⇘ℭ⇙ b'"
      by (blast intro: is_arrI)
    from category_axioms f f' show "cf_hom ℭ ff' = ?cfa⦇ArrMap⦈⦇ff'⦈"
      unfolding ff'_def cat_op_simps
      by 
        (
          cs_concl  
            cs_simp: cat_cs_simps cat_op_simps 
            cs_intro: cat_cs_intros cat_op_intros
        )
  qed (auto simp: cf_array_ArrMap_vsv cf_Hom_ArrMap_vsv cat_cs_simps)

qed simp_all


subsubsection‹
Projections of the compositions of a ‹Hom›-functor and a functor are
projections of the ‹Hom›-functor
›

lemma (in category) cat_cf_rcomp_Hom_cf_Hom_snd:
  assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "a ∈⇩∘ ℭ⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⇘op_cat ℭ,𝔅⇙(a,-)⇩C⇩F = Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) ∘⇩C⇩F 𝔊"
  using category_axioms assms 
  unfolding cf_rcomp_Hom_def cf_Hom_snd_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )
  
lemmas [cat_cs_simps] = category.cat_cf_rcomp_Hom_cf_Hom_snd

lemma (in category) cat_cf_lcomp_Hom_cf_Hom_snd:
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉-,-)⇘op_cat 𝔅,ℭ⇙(b,-)⇩C⇩F = Hom⇩O⇩.⇩C⇘α⇙ℭ(𝔉⦇ObjMap⦈⦇b⦈,-)"
  using category_axioms assms 
  unfolding cf_lcomp_Hom_def cf_Hom_snd_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
    )

lemmas [cat_cs_simps] = category.cat_cf_lcomp_Hom_cf_Hom_snd

lemma (in category) cat_cf_rcomp_Hom_cf_Hom_fst:
  assumes "𝔉 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "b ∈⇩∘ 𝔅⦇Obj⦈"
  shows "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)"
proof-

  from category_axioms assms have H𝔉b:
    "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by (cs_concl cs_intro: cat_cs_intros)
  from category_axioms assms have H𝔉b':
    "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈) : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
    by (cs_concl cs_intro: cat_cs_intros)

  from category_axioms assms have [cat_cs_simps]:
    "𝒟⇩∘ ((Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ObjMap⦈) = op_cat ℭ⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros)+
  from category_axioms assms have [cat_cs_simps]:
    "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈) = op_cat ℭ⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

  from category_axioms assms have [cat_cs_simps]:
    "𝒟⇩∘ ((Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ArrMap⦈) = op_cat ℭ⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros)+
  from category_axioms assms have [cat_cs_simps]:
    "𝒟⇩∘ (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈) = op_cat ℭ⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

  show ?thesis
  proof(rule cf_eqI[OF H𝔉b H𝔉b'])

    show 
      "(Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ObjMap⦈ = 
        Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold cat_cs_simps)
      from category_axioms assms show 
        "vsv ((Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ObjMap⦈)"
        by (intro bifunctor_proj_fst_ObjMap_vsv[of α]) 
          (cs_concl cs_intro: cat_cs_intros)+
      from assms show "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈)"
        by (intro cat_cf_Hom_fst_ObjMap_vsv)
          (cs_concl cs_intro: cat_cs_intros)+
      fix a assume prems: "a ∈⇩∘ op_cat ℭ⦇Obj⦈"
      with category_axioms assms show 
        "(Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ObjMap⦈⦇a⦈ = 
          Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈⦇a⦈"
        by 
          (
            cs_concl  
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed simp

    show 
      "(Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ArrMap⦈ = 
        Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold cat_cs_simps cat_op_simps)
      from category_axioms assms show 
        "vsv ((Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ArrMap⦈)"
        by (intro bifunctor_proj_fst_ArrMap_vsv[of α]) 
          (cs_concl cs_intro: cat_cs_intros)+
      from assms show "vsv (Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈)"
        by (intro cat_cf_Hom_fst_ArrMap_vsv)
          (cs_concl cs_intro: cat_cs_intros)+
      fix f assume "f ∈⇩∘ ℭ⦇Arr⦈"
      then obtain a' b' where "f : a' ↦⇘ℭ⇙ b'" by (auto simp: cat_op_simps)
      from category_axioms assms this show 
        "(Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉-)⇘op_cat ℭ,𝔅⇙(-,b)⇩C⇩F)⦇ArrMap⦈⦇f⦈ = 
          Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔉⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈⦇f⦈"
        by 
          (
            cs_concl  
              cs_simp: cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed simp

  qed simp_all

qed

lemmas [cat_cs_simps] = category.cat_cf_rcomp_Hom_cf_Hom_fst

text‹\newpage›

end