Theory CZH_ECAT_Hom

(* Copyright 2021 (C) Mihails Milehins *)

sectionHom›-functor›
theory CZH_ECAT_Hom
  imports 
    CZH_ECAT_Set
    CZH_ECAT_PCategory
begin



subsectionhom›-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 =
    [
      (
        λqHom  (Codvpfst f) (Domvpsnd f).
          vpsnd f Aq Avpfst f
      ),
      Hom  (Codvpfst f) (Domvpsnd f),
      Hom  (Domvpfst f) (Codvpsnd f)
    ]"


text‹Components.›

lemma cf_hom_components:
  shows "cf_hom  fArrVal = 
      (
        λqHom  (Codvpfst f) (Domvpsnd f). 
          vpsnd f Aq Avpfst f
      )"
    and "cf_hom  fArrDom = Hom  (Codvpfst f) (Domvpsnd f)"
    and "cf_hom  fArrCod = Hom  (Domvpfst f) (Codvpsnd 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]ArrValq = f Aq Ag"
  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]ArrValq"
    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  gfArrDom = 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  gfArrCod = 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


subsubsectionhom›-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]: "Domg = d" "Codg = c" 
    and d: "d  Obj" and c: "c  Obj"
    by auto
  from f have [simp]: "Domf = c'" "Codf = 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  gfArrVal)"
    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  gfArrVal) = cf_hom  gfArrDom"
    unfolding cf_hom_components by auto
  show " (cf_hom  gfArrVal)  cf_hom  gfArrCod"
  proof(rule vsubsetI)
    interpret hom_fg: vsv cf_hom  gfArrVal by (simp add: vsv_hom_fg)
    fix y assume "y   (cf_hom  gfArrVal)"
    then obtain q where y_def: "y = cf_hom  gfArrValq" 
      and q: "q  𝒟 (cf_hom  gfArrVal)"
      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 Aq Ag : d d'" 
      by (auto intro: cat_cs_intros)
    then show "y  cf_hom  gfArrCod"  
      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  gfArrDom  Vset α"
    unfolding cf_hom_components gf_def
    by (auto simp: nat_omega_simps intro: cat_cs_intros)
  from d d' show "cf_hom  gfArrCod  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 αDomcf_hom  gf = Hom  a b"
    "cat_Set αCodcf_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'] Acat_Set αcf_hom  [f, f'] =
      cf_hom  [g Aop_cat f, g' Af']"
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'] Acat_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'] Acat_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 Aop_cat f, g' Af'] : 
      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 Aop_cat f, g' Af']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'] Acat_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 Aop_cat f, g' Af'])"
      by (auto dest: cat_Set_is_arrD(1))
  
    show "(cf_hom  [g, g'] Acat_Set αcf_hom  [f, f'])ArrVal = 
      cf_hom  [g Aop_cat f, g' Af']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'] Acat_Set αcf_hom  [f, f'])ArrValq = 
          cf_hom  [g Aop_cat f, g' Af']ArrValq"
        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  [CIdc, CIdc'] = cat_Set αCIdHom  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  [CIdc, CIdc'] : 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  [CIdc, CIdc']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 αCIdHom  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 αCIdHom  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  [CIdc, CIdc'])"
      by (auto dest: cat_Set_is_arrD(1))  
    from CId_cc' show arr_Set_Hom_cc': 
      "arr_Set α (cat_Set αCIdHom  c c')"
      by (auto simp: cat_Set_is_arrD(1))
    show "cf_hom  [CIdc, CIdc']ArrVal =
      cat_Set αCIdHom  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  [CIdc, CIdc']ArrValq = 
          cat_Set αCIdHom  c c'ArrValq"
        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']ArrValf = cf_hom  [g', g]ArrValf"
      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



subsectionHom›-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" (HomO.Cı_'(/-,-/'))
  where "HomO.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 "HomO.Cα(-,-)ObjMap = 
    (λa(op_cat  ×C )Obj. Hom  (vpfst a) (vpsnd a))"
    and "HomO.Cα(-,-)ArrMap = (λf(op_cat  ×C )Arr. cf_hom  f)"
    and "HomO.Cα(-,-)HomDom = op_cat  ×C "
    and "HomO.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]:  
  "𝒟 (HomO.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 "HomO.Cα(-,-)ObjMapa, b = Hom  a b"
  using assms unfolding cf_Hom_components by (simp add: nat_omega_simps)
                
lemma (in category) cf_Hom_ObjMap_vrange: 
  " (HomO.Cα(-,-)ObjMap)  cat_Set αObj"
proof(intro vsubsetI)
  interpret op_ℭ: category α op_cat  by (simp add: category_op)
  fix y assume "y   (HomO.Cα(-,-)ObjMap)"
  then obtain x where y_def: "y = HomO.Cα(-,-)ObjMapx" 
    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]|


subsubsectionHom›-functor is a functor›

lemma (in category) cat_Hom_is_functor:
  "HomO.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 HomO.Cα(-,-)"
      unfolding cf_Hom_def by simp
    show op_ℭ_ℭ: "category α (op_cat  ×C )" by (auto simp: cat_cs_intros)
    show "vcard HomO.Cα(-,-) = 4"
      unfolding cf_Hom_def by (simp add: nat_omega_simps)
  
    show " (HomO.Cα(-,-)ObjMap)  cat_Set αObj"
      by (simp add: cf_Hom_ObjMap_vrange)
    show "HomO.Cα(-,-)ArrMapgf :
      HomO.Cα(-,-)ObjMapab cat_Set αHomO.Cα(-,-)ObjMapcd"
      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 "HomO.Cα(-,-)ArrMapgf :
        HomO.Cα(-,-)ObjMapab cat_Set αHomO.Cα(-,-)ObjMapcd"
        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 "HomO.Cα(-,-)ArrMapgg' Aop_cat  ×C ff' = 
      HomO.Cα(-,-)ArrMapgg' Acat_Set αHomO.Cα(-,-)ArrMapff'"
      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 "HomO.Cα(-,-)ArrMap(op_cat  ×C )CIdcc' = 
      cat_Set αCIdHomO.Cα(-,-)ObjMapcc'"
      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 "HomO.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" (HomO.Cı_'(/_-,_-/'))
  ―‹The following definition may seem redundant, but it will help to avoid
  proof duplication later.›
  where "HomO.Cα(𝔉-,𝔊-) = cf_cn_cov_bcomp (HomO.Cα(-,-)) 𝔉 𝔊"


subsubsection‹Object map›

lemma cf_bcomp_Hom_ObjMap_vsv: "vsv (HomO.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 "𝒟 (HomO.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 "HomO.Cα(𝔉-,𝔊-)ObjMapa, b = 
    HomO.Cα(-,-)ObjMap𝔉ObjMapa, 𝔊ObjMapb"
  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 " (HomO.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 (HomO.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 "𝒟 (HomO.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 
    "HomO.Cα(𝔉-,𝔊-)ArrMapf, g = 
      HomO.Cα(-,-)ArrMap𝔉ArrMapf, 𝔊ArrMapg"
  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 " (HomO.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 "HomO.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 "HomO.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" (HomO.Cı_'(/_-,-/'))
  where "HomO.Cα(𝔉-,-) = cf_cn_cov_lcomp  (HomO.Cα(-,-)) 𝔉"

definition cf_rcomp_Hom :: "V  V  V  V" (HomO.Cı_'(/-,_-/'))
  where "HomO.Cα(-,𝔊-) = cf_cn_cov_rcomp  (HomO.Cα(-,-)) 𝔊"


subsubsection‹Object map›

lemma cf_lcomp_Hom_ObjMap_vsv[cat_cs_intros]: "vsv (HomO.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 (HomO.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 "𝒟 (HomO.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 "𝒟 (HomO.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 "HomO.Cα(𝔉-,-)ObjMapb, c = 
    HomO.Cα(-,-)ObjMap𝔉ObjMapb, 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 "HomO.Cα(-,𝔊-)ObjMapc, b =
    HomO.Cα(-,-)ObjMapc, 𝔊ObjMapb"
  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 " (HomO.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 " (HomO.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 (HomO.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 (HomO.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 "𝒟 (HomO.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 "𝒟 (HomO.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 "HomO.Cα(𝔉-,-)ArrMapg, f =
    HomO.Cα(-,-)ArrMap𝔉ArrMapg, 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 "HomO.Cα(-,𝔊-)ArrMapg, f =
    HomO.Cα(-,-)ArrMapg, 𝔊ArrMapf"
  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 " (HomO.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 " (HomO.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]:
  "HomO.Cα(𝔉-,cf_id -) = HomO.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]:
  "HomO.Cα(cf_id -,𝔊-) = HomO.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 "HomO.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 "HomO.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 "HomO.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 "HomO.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 ) 𝔅 (HomO.Cα(-,𝔊-)) =
      HomO.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 ) 𝔅 HomO.Cα(-,𝔊-) :
      𝔅 ×C op_cat  ↦↦Cαcat_Set α"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from category_axioms assms show op_Hom:
    "HomO.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 ) 𝔅 HomO.Cα(-,𝔊-)ObjMap) = 
      (𝔅 ×C op_cat )Obj"
    by (cs_concl cs_simp: cat_cs_simps)
  from op_Hom have ObjMap_dom_rhs:
    "𝒟 (HomO.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 ) 𝔅 HomO.Cα(-,𝔊-)ArrMap) = 
      (𝔅 ×C op_cat )Arr"
    by (cs_concl cs_simp: cat_cs_simps)
  from op_Hom have ArrMap_dom_rhs:
    "𝒟 (HomO.Cαop_cat (op_cf 𝔊-,-)ArrMap) = (𝔅 ×C op_cat )Arr"
    by (cs_concl cs_simp: cat_cs_simps)

  show 
    "bifunctor_flip (op_cat ) 𝔅 HomO.Cα(-,𝔊-)ObjMap =
      HomO.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 ) 𝔅 HomO.Cα(-,𝔊-)ObjMapbc =
        HomO.Cαop_cat (op_cf 𝔊-,-)ObjMapbc"
      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 ) 𝔅 HomO.Cα(-,𝔊-)ArrMap =
      HomO.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 ) 𝔅 HomO.Cα(-,𝔊-)ArrMapgf =
        HomO.Cαop_cat (op_cf 𝔊-,-)ArrMapgf"
      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 𝔅)  (HomO.Cα(𝔉-,-)) =
      HomO.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" (HomO.Cı_'(/_,-/'))
  where "HomO.Cα(a,-) = HomO.Cα(-,-)op_cat ,(a,-)CF"
definition cf_Hom_fst :: "V  V  V  V" (HomO.Cı_'(/-,_/'))
  where "HomO.Cα(-,b) = HomO.Cα(-,-)op_cat ,(-,b)CF"


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

lemma (in category) cat_cf_Hom_snd_is_functor:
  assumes "a  Obj"
  shows "HomO.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 "HomO.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 "HomO.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 "HomO.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 (HomO.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 (HomO.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 "𝒟 (HomO.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 "𝒟 (HomO.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 "HomO.Cα(a,-)ObjMapb = 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 "HomO.Cα(-,b)ObjMapa = 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 (HomO.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 (HomO.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 "𝒟 (HomO.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 "𝒟 (HomO.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 "HomO.Cα(a,-)ArrMapf = cf_hom  [op_cat CIda, 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 "HomO.Cα(-,b)ArrMapf = cf_hom  [f, CIdb]"
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 "HomO.Cαop_cat (a,-) = HomO.Cα(-,a)"
proof(rule cf_eqI[of α])

  from assms category_axioms show 
    "HomO.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 
    "HomO.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 "HomO.Cαop_cat (a,-)ObjMap = HomO.Cα(-,a)ObjMap"
  proof(rule vsv_eqI)
    from assms category_axioms show "vsv (HomO.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 (HomO.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 
      "𝒟 (HomO.Cαop_cat (a,-)ObjMap) = 𝒟 (HomO.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 "HomO.Cαop_cat (a,-)ObjMapb = HomO.Cα(-,a)ObjMapb"
      if "b  𝒟 (HomO.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 "HomO.Cαop_cat (a,-)ArrMap = HomO.Cα(-,a)ArrMap"
  proof(rule vsv_eqI)
    from assms category_axioms show "vsv (HomO.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 (HomO.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 
      "𝒟 (HomO.Cαop_cat (a,-)ArrMap) = 𝒟 (HomO.Cα(-,a)ArrMap)"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_op_intros
        )
    show "HomO.Cαop_cat (a,-)ArrMapf = HomO.Cα(-,a)ArrMapf"
      if "f  𝒟 (HomO.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 "HomO.Cαop_cat (-,a) = HomO.Cα(a,-)"
proof-
  from assms have a: "a  op_cat Obj" unfolding cat_op_simps .
  have "HomO.Cα(a,-) = HomO.Cαop_cat (op_cat )(a,-)" 
    unfolding cat_op_simps ..
  also have " = HomO.Cα(op_cat )(-,a)"
    unfolding category.cat_op_cat_cf_Hom_snd[OF category_op a] by simp
  finally show "HomO.Cα(op_cat )(-,a) = HomO.Cα(a,-)" by simp
qed

lemmas [cat_op_simps] = category.cat_op_cat_cf_Hom_fst


subsubsectionHom›-functors are injections on objects›

lemma (in category) cat_cf_Hom_snd_inj:
  assumes "HomO.Cα(a,-) = HomO.Cα(b,-)" 
    and "a  Obj"
    and "b  Obj"
  shows "a = b"
proof(rule ccontr)
  assume prems: "a  b"
  from assms(1) have "HomO.Cα(a,-)ObjMapb = HomO.Cα(b,-)ObjMapb" 
    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 "HomO.Cα(-,a) = HomO.Cα(-,b)" and "a  Obj" and "b  Obj"
  shows "a = b"
proof(rule ccontr)
  assume prems: "a  b"
  from assms(1) have "HomO.Cα(-,a)ObjMapb = HomO.Cα(-,b)ObjMapb" 
    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


subsubsectionHom›-functor is an array bifunctor›

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

  show "HomO.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: "HomO.Cα(-,c) : op_cat  ↦↦Cαcat_Set α"
    if "c  Obj" for c
    using that by (rule cat_cf_Hom_fst_is_functor)
  have c5: "HomO.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: "HomO.Cα(b,-)ObjMapc = HomO.Cα(-,c)ObjMapb"
    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: 
    "HomO.Cα(b',-)ArrMapg Acat_Set αHomO.Cα(-,c)ArrMapf =
      HomO.Cα(-,c' )ArrMapf Acat_Set αHomO.Cα(b,- )ArrMapg"
    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 "HomO.Cα(-,-)ObjMap = ?cfaObjMap"
  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 
      "HomO.Cα(-,-)ObjMapaa' = ?cfaObjMapaa'"
      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 "HomO.Cα(-,-)ArrMap = ?cfaArrMap"
  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' = ?cfaArrMapff'"
      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 "HomO.Cα(-,𝔊-)op_cat ,𝔅(a,-)CF = HomO.Cα(a,-) CF 𝔊"
  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 "HomO.Cα(𝔉-,-)op_cat 𝔅,(b,-)CF = HomO.Cα(𝔉ObjMapb,-)"
  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 "HomO.Cα(-,𝔉-)op_cat ,𝔅(-,b)CF = HomO.Cα(-,𝔉ObjMapb)"
proof-

  from category_axioms assms have H𝔉b:
    "HomO.Cα(-,𝔉-)op_cat ,𝔅(-,b)CF : op_cat  ↦↦Cαcat_Set α"
    by (cs_concl cs_intro: cat_cs_intros)
  from category_axioms assms have H𝔉b':
    "HomO.Cα(-,𝔉ObjMapb) : op_cat  ↦↦Cαcat_Set α"
    by (cs_concl cs_intro: cat_cs_intros)

  from category_axioms assms have [cat_cs_simps]:
    "𝒟 ((HomO.Cα(-,𝔉-)op_cat ,𝔅(-,b)CF)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]:
    "𝒟 (HomO.Cα(-,𝔉ObjMapb)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]:
    "𝒟 ((HomO.Cα(-,𝔉-)op_cat ,𝔅(-,b)CF)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]:
    "𝒟 (HomO.Cα(-,𝔉ObjMapb)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 
      "(HomO.Cα(-,𝔉-)op_cat ,𝔅(-,b)CF)ObjMap = 
        HomO.Cα(-,𝔉ObjMapb)ObjMap"
    proof(rule vsv_eqI, unfold cat_cs_simps)
      from category_axioms assms show 
        "vsv ((HomO.Cα(-,𝔉-)op_cat ,𝔅(-,b)CF)ObjMap)"
        by (intro bifunctor_proj_fst_ObjMap_vsv[of α]) 
          (cs_concl cs_intro: cat_cs_intros)+