(* Copyright 2021 (C) Mihails Milehins *)

sectionCAT› as a semicategory\label{sec:smc_CAT}›
theory CZH_SMC_CAT


The subsection presents the theory of the semicategories of α›-categories.
It continues the development that was initiated in section 

named_theorems smc_CAT_simps
named_theorems smc_CAT_intros

subsection‹Definition and elementary properties›

definition smc_CAT :: "V  V"
  where "smc_CAT α =
      set {. category α }, 
      all_cfs α, 
      (λ𝔉all_cfs α. 𝔉HomDom), 
      (λ𝔉all_cfs α. 𝔉HomCod),
      (λ𝔊𝔉composable_arrs (dg_CAT α). 𝔊𝔉0 CF 𝔊𝔉1)


lemma smc_CAT_components:
  shows "smc_CAT αObj = set {. category α }"
    and "smc_CAT αArr = all_cfs α"
    and "smc_CAT αDom = (λ𝔉all_cfs α. 𝔉HomDom)"
    and "smc_CAT αCod = (λ𝔉all_cfs α. 𝔉HomCod)"
    and "smc_CAT αComp = (λ𝔊𝔉composable_arrs (dg_CAT α). 𝔊𝔉0 CF 𝔊𝔉1)"
  unfolding smc_CAT_def dg_field_simps by (simp_all add: nat_omega_simps)


lemma smc_dg_CAT: "smc_dg (smc_CAT α) = dg_CAT α"
proof(rule vsv_eqI)
  show "vsv (smc_dg (smc_CAT α))" unfolding smc_dg_def by auto
  show "vsv (dg_CAT α)" unfolding dg_CAT_def by auto
  have dom_lhs: "𝒟 (smc_dg (smc_CAT α)) = 4" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟 (dg_CAT α) = 4"
    unfolding dg_CAT_def by (simp add: nat_omega_simps)
  show "𝒟 (smc_dg (smc_CAT α)) = 𝒟 (dg_CAT α)"
    unfolding dom_lhs dom_rhs by simp
  show "𝔄  𝒟 (smc_dg (smc_CAT α))  smc_dg (smc_CAT α)𝔄 = dg_CAT α𝔄"
    for 𝔄
        unfold dom_lhs, 
        unfold smc_dg_def dg_field_simps smc_CAT_def dg_CAT_def
      (auto simp: nat_omega_simps)

lemmas_with [folded smc_dg_CAT, unfolded slicing_simps]: 
  smc_CAT_ObjI = dg_CAT_ObjI
  and smc_CAT_ObjD = dg_CAT_ObjD
  and smc_CAT_ObjE = dg_CAT_ObjE
  and smc_CAT_Obj_iff[smc_CAT_simps] = dg_CAT_Obj_iff  
  and smc_CAT_Dom_app[smc_CAT_simps] = dg_CAT_Dom_app
  and smc_CAT_Cod_app[smc_CAT_simps] = dg_CAT_Cod_app
  and smc_CAT_is_arrI = dg_CAT_is_arrI
  and smc_CAT_is_arrD = dg_CAT_is_arrD
  and smc_CAT_is_arrE = dg_CAT_is_arrE
  and smc_CAT_is_arr_iff[smc_CAT_simps] = dg_CAT_is_arr_iff

subsection‹Composable arrows›

lemma smc_CAT_composable_arrs_dg_CAT: 
  "composable_arrs (dg_CAT α) = composable_arrs (smc_CAT α)"
  unfolding composable_arrs_def smc_dg_CAT[symmetric] slicing_simps by auto

lemma smc_CAT_Comp: 
  "smc_CAT αComp = (λ𝔊𝔉composable_arrs (smc_CAT α). 𝔊𝔉0 SMCF 𝔊𝔉1)"
  unfolding smc_CAT_components smc_CAT_composable_arrs_dg_CAT ..


lemma smc_CAT_Comp_app[smc_CAT_simps]:
  assumes "𝔊 : 𝔅 smc_CAT α" and "𝔉 : 𝔄 smc_CAT α𝔅"
  shows "𝔊 Asmc_CAT α𝔉 = 𝔊 SMCF 𝔉"
  from assms have "[𝔊, 𝔉]  composable_arrs (smc_CAT α)" 
    by (auto simp: smc_cs_intros)
  then show "𝔊 Asmc_CAT α𝔉 = 𝔊 SMCF 𝔉"
    unfolding smc_CAT_Comp by (simp add: nat_omega_simps)

lemma smc_CAT_Comp_vdomain: "𝒟 (smc_CAT αComp) = composable_arrs (smc_CAT α)" 
  unfolding smc_CAT_Comp by auto                      

lemma smc_CAT_Comp_vrange: " (smc_CAT αComp)  all_cfs α"
proof(rule vsubsetI)
  fix  assume "   (smc_CAT αComp)"
  then obtain 𝔊𝔉 
    where ℌ_def: " = smc_CAT αComp𝔊𝔉"
      and "𝔊𝔉  𝒟 (smc_CAT αComp)"
    by (auto simp: smc_CAT_components intro: smc_cs_intros)
  then obtain 𝔊 𝔉 𝔄 𝔅  
    where "𝔊𝔉 = [𝔊, 𝔉]" 
      and 𝔊: "𝔊 : 𝔅 smc_CAT α" 
      and 𝔉: "𝔉 : 𝔄 smc_CAT α𝔅"
    by (auto simp: smc_CAT_Comp_vdomain) 
  with ℌ_def have ℌ_def': " = 𝔊 Asmc_CAT α𝔉" by simp
  from 𝔊 𝔉 show "  all_cfs α" 
    unfolding ℌ_def' by (auto simp: smc_CAT_simps intro: cat_cs_intros)

subsectionCAT› is a category›

lemma (in 𝒵) tiny_semicategory_smc_CAT: 
  assumes "𝒵 β" and "α  β"
  shows "tiny_semicategory β (smc_CAT α)"
proof(intro tiny_semicategoryI, unfold smc_CAT_is_arr_iff)
  show "vfsequence (smc_CAT α)" unfolding smc_CAT_def by auto
  show "vcard (smc_CAT α) = 5"
    unfolding smc_CAT_def by (simp add: nat_omega_simps)
  show "(𝔊𝔉  𝒟 (smc_CAT αComp)) 
    (𝔊 𝔉 𝔅  𝔄. 𝔊𝔉 = [𝔊, 𝔉]  𝔊 : 𝔅 ↦↦Cα  𝔉 : 𝔄 ↦↦Cα𝔅)"
    for 𝔊𝔉
    unfolding smc_CAT_Comp_vdomain
    show "𝔊𝔉  composable_arrs (smc_CAT α)  
      𝔊 𝔉 𝔅  𝔄. 𝔊𝔉 = [𝔊, 𝔉]  𝔊 : 𝔅 ↦↦Cα  𝔉 : 𝔄 ↦↦Cα𝔅"
      by (elim composable_arrsE) (auto simp: smc_CAT_is_arr_iff)
    assume "𝔊 𝔉 𝔅  𝔄. 𝔊𝔉 = [𝔊, 𝔉]  𝔊 : 𝔅 ↦↦Cα  𝔉 : 𝔄 ↦↦Cα𝔅"
    with smc_CAT_is_arr_iff show "𝔊𝔉  composable_arrs (smc_CAT α)"
      unfolding smc_CAT_Comp_vdomain by (auto intro: smc_cs_intros)
  show " 𝔊 : 𝔅 ↦↦Cα; 𝔉 : 𝔄 ↦↦Cα𝔅   
    𝔊 Asmc_CAT α𝔉 : 𝔄 ↦↦Cα"
    for 𝔊 𝔅  𝔉 𝔄
    by (cs_concl cs_simp: smc_CAT_simps cs_intro: cat_cs_intros)

  fix   𝔇 𝔊 𝔅 𝔉 𝔄
  assume " :  ↦↦Cα𝔇" "𝔊 : 𝔅 ↦↦Cα" "𝔉 : 𝔄 ↦↦Cα𝔅"
  moreover then have "𝔊 CF 𝔉 : 𝔄 ↦↦Cα" " CF 𝔊 : 𝔅 ↦↦Cα𝔇" 
    by (cs_concl cs_simp: smc_CAT_simps cs_intro: cat_cs_intros)+
  ultimately show 
    " Asmc_CAT α𝔊 Asmc_CAT α𝔉 =  Asmc_CAT α(𝔊 Asmc_CAT α𝔉)"
    by (simp add: smc_CAT_is_arr_iff smc_CAT_Comp_app cf_comp_assoc)
qed (auto simp: assms smc_dg_CAT tiny_category_dg_CAT smc_CAT_components)

subsection‹Initial object›

lemma (in 𝒵) smc_CAT_obj_initialI: "obj_initial (smc_CAT α) cat_0"
  See \cite{noauthor_nlab_nodate}\footnote{\url{
  unfolding obj_initial_def
proof(intro obj_terminalI, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
  show "category α cat_0" by (intro category_cat_0)
  fix 𝔄 assume "category α 𝔄"
  then interpret category α 𝔄 .
  show "∃!f. f : cat_0 ↦↦Cα𝔄"
    show cf_0: "cf_0 𝔄 : cat_0 ↦↦Cα𝔄"
      by (simp add: cf_0_is_ft_functor category_axioms is_ft_functor.axioms(1))
    fix 𝔉 assume prems: "𝔉 : cat_0 ↦↦Cα𝔄" 
    interpret 𝔉: is_functor α cat_0 𝔄 𝔉 using prems .
    show "𝔉 = cf_0 𝔄"
    proof(rule cf_eqI)
      show "𝔉 : cat_0 ↦↦Cα𝔄" by (simp add: prems)
      from cf_0 show "cf_0 𝔄 : cat_0 ↦↦Cα𝔄" 
        unfolding smc_CAT_is_arr_iff by simp
      have "𝒟 (𝔉ObjMap) = 0" by (auto simp: cat_0_components cat_cs_simps)
      then show "𝔉ObjMap = cf_0 𝔄ObjMap"
        using 𝔉.ObjMap.vbrelation_vintersection_vdomain 
        by (auto simp: cf_0_components)
      have "𝒟 (𝔉ArrMap) = 0" by (auto simp: cat_0_components cat_cs_simps)
      with 𝔉.ArrMap.vbrelation_vintersection_vdomain show 
        "𝔉ArrMap = cf_0 𝔄ArrMap"
        by (auto simp: cf_0_components)
    qed (simp_all add: cf_0_components)

lemma (in 𝒵) smc_CAT_obj_initialD:
  assumes "obj_initial (smc_CAT α) 𝔄"
  shows "𝔄 = cat_0" 
  using assms unfolding obj_initial_def
proof(elim obj_terminalE, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
  assume prems: 
    "category α 𝔄" 
    "category α 𝔅  ∃!𝔉. 𝔉 : 𝔄 ↦↦Cα𝔅" 
    for 𝔅
  from prems(2)[OF category_cat_0] obtain 𝔉 where 𝔉: "𝔉 : 𝔄 ↦↦Cαcat_0" 
    by meson
  interpret 𝔉: is_functor α 𝔄 cat_0 𝔉 by (rule 𝔉) 
  have " (𝔉ObjMap)  0"
    unfolding cat_0_components(1)[symmetric] by (simp add: 𝔉.cf_ObjMap_vrange)
  then have "𝔉ObjMap = 0" by (auto intro: 𝔉.ObjMap.vsv_vrange_vempty)
  with 𝔉.cf_ObjMap_vdomain have Obj[simp]: "𝔄Obj = 0" by auto
  have " (𝔉ArrMap)  0"
    unfolding cat_0_components(2)[symmetric] by (simp add: 𝔉.cf_ArrMap_vrange)
  then have "𝔉ArrMap = 0" by (auto intro: 𝔉.ArrMap.vsv_vrange_vempty)
  with 𝔉.cf_ArrMap_vdomain have Arr[simp]: "𝔄Arr = 0" by auto
  from 𝔉.HomDom.Dom.vdomain_vrange_is_vempty have [simp]: "𝔄Dom = 0"  
    by (fastforce simp: 𝔉.HomDom.cat_Dom_vempty_if_Arr_vempty)
  from 𝔉.HomDom.Cod.vdomain_vrange_is_vempty have [simp]: "𝔄Cod = 0"
    by (fastforce simp: 𝔉.HomDom.cat_Cod_vempty_if_Arr_vempty)
  from Arr have "𝔄Arr ^× 2 = 0" by (simp add: vcpower_of_vempty)
  with 𝔉.HomDom.Comp.pnop_vdomain have "𝒟 (𝔄Comp) = 0" by simp
  with 𝔉.HomDom.Comp.vdomain_vrange_is_vempty have [simp]: "𝔄Comp = 0"
    by (auto intro: 𝔉.HomDom.Comp.vsv_vrange_vempty)
  have "𝒟 (𝔄CId) = 0"
    by (simp add: 𝔉.HomDom.cat_CId_vdomain)
  with 𝔉.HomDom.CId.vdomain_vrange_is_vempty 𝔉.HomDom.CId.vsv_vrange_vempty 
  have [simp]: "𝔄CId = 0"
    by simp
  show "𝔄 = cat_0"
    by (rule cat_eqI[of α])  
      (simp_all add: prems(1) cat_0_components category_cat_0)

lemma (in 𝒵) smc_CAT_obj_initialE:
  assumes "obj_initial (smc_CAT α) 𝔄"
  obtains "𝔄 = cat_0" 
  using assms by (auto dest: smc_CAT_obj_initialD)

lemma (in 𝒵) smc_CAT_obj_initial_iff[smc_CAT_simps]: 
  "obj_initial (smc_CAT α) 𝔄  𝔄 = cat_0"
  using smc_CAT_obj_initialI smc_CAT_obj_initialD by auto

subsection‹Terminal object›

lemma (in 𝒵) smc_CAT_obj_terminalI: 
  ―‹See \cite{noauthor_nlab_nodate}\footnote{\url{
  assumes "a  Vset α" and "f  Vset α"
  shows "obj_terminal (smc_CAT α) (cat_1 a f)"
proof(intro obj_terminalI, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
  fix 𝔄 assume prems: "category α 𝔄"
  then interpret category α 𝔄 .
  show "∃!𝔉'. 𝔉' : 𝔄 ↦↦Cαcat_1 a f"
    show cf_1: "cf_const 𝔄 (cat_1 a f) a : 𝔄 ↦↦Cαcat_1 a f"
      by (rule cf_const_is_functor)
        (auto simp: assms prems category_cat_1 cat_1_components)
    fix 𝔉' assume "𝔉' : 𝔄 ↦↦Cαcat_1 a f"
    then interpret 𝔉': is_functor α 𝔄 cat_1 a f 𝔉' .
    show "𝔉' = cf_const 𝔄 (cat_1 a f) a"
    proof(rule cf_eqI, unfold dghm_const_components)
      from cf_1 show "cf_const 𝔄 (cat_1 a f) a : 𝔄 ↦↦Cαcat_1 a f" by simp
      show "𝔉'ObjMap = vconst_on (𝔄Obj) a"
      proof(cases𝔄Obj = 0)
        case True
        with 𝔉'.ObjMap.vbrelation_vintersection_vdomain have "𝔉'ObjMap = 0"
          by (auto simp: cat_cs_simps)
        with True show ?thesis by simp
        case False
        then have "𝒟 (𝔉'ObjMap)  0" by (auto simp: cat_cs_simps)
        then have " (𝔉'ObjMap)  0"
          by (simp add: 𝔉'.ObjMap.vsv_vdomain_vempty_vrange_vempty)
        moreover from 𝔉'.cf_ObjMap_vrange have " (𝔉'ObjMap)  set {a}"
          by (simp add: cat_1_components)
        ultimately have " (𝔉'ObjMap) = set {a}" by auto
        then show ?thesis 
          by (intro vsv.vsv_is_vconst_onI) (auto simp: cat_cs_simps) 
      show "𝔉'ArrMap = vconst_on (𝔄Arr) (cat_1 a fCIda)"
      proof(cases𝔄Arr = 0)
        case True
          vsv.vsv_vrange_vempty[OF 𝔉'.cf_ArrMap_vsv] 
        have "𝔉'ArrMap = 0"
          by (auto simp: cat_cs_simps)
        with True show ?thesis by simp
        case False
        then have "𝒟 (𝔉'ArrMap)  0" by (auto simp: cat_cs_simps)
        then have " (𝔉'ArrMap)  0" 
          by (simp add: 𝔉'.ArrMap.vsv_vdomain_vempty_vrange_vempty)
        moreover from 𝔉'.cf_ArrMap_vrange have " (𝔉'ArrMap)  set {f}"
          by (simp add: cat_1_components)
        ultimately have " (𝔉'ArrMap) = set {f}" by auto
        then show ?thesis 
              cs_concl cs_shallow 
                cs_simp: V_cs_simps cat_cs_simps cat_1_components
                cs_intro: V_cs_intros vsv.vsv_is_vconst_onI
    qed (auto intro: cat_cs_intros)
qed (simp add: assms category_cat_1)

lemma (in 𝒵) smc_CAT_obj_terminalE: 
  assumes "obj_terminal (smc_CAT α) 𝔅"
  obtains a f where "a  Vset α" and "f  Vset α" and "𝔅 = cat_1 a f"
  using assms
proof(elim obj_terminalE, unfold cat_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)

  assume prems: "category α 𝔅" "category α 𝔄  ∃!𝔉. 𝔉 : 𝔄 ↦↦Cα𝔅" for 𝔄
  interpret 𝔅: category α 𝔅 by (rule prems(1))

  obtain a where 𝔅_Obj: "𝔅Obj = set {a}" and a: "a  Vset α"
    have cat_1: "category α (cat_1 0 0)" by (rule category_cat_1) auto
    from prems(2)[OF cat_1] obtain 𝔉 
      where 𝔉: "𝔉 : cat_1 0 0 ↦↦Cα𝔅" 
        and 𝔊𝔉: "𝔊 : cat_1 0 0 ↦↦Cα𝔅  𝔊 = 𝔉" for 𝔊
      by fastforce
    interpret 𝔉: is_functor α cat_1 0 0 𝔅 𝔉 by (rule 𝔉)
    have "𝒟 (𝔉ObjMap) = set {0}" by (simp add: cat_1_components cat_cs_simps)
    then obtain a where vrange_𝔉[simp]: " (𝔉ObjMap) = set {a}"
      by (auto intro: 𝔉.ObjMap.vsv_vdomain_vsingleton_vrange_vsingleton)
    with 𝔅.cat_Obj_vsubset_Vset 𝔉.cf_ObjMap_vrange have [simp]: "a  Vset α"
      by auto
    from 𝔉.cf_ObjMap_vrange have "set {a}  𝔅Obj" by simp
    moreover have "𝔅Obj  set {a}"
    proof(rule ccontr)
      assume "¬𝔅Obj  set {a}"
      then obtain b where ba: "b  a" and b: "b  𝔅Obj" by force
      have "cf_const (cat_1 0 0) 𝔅 b : cat_1 0 0 ↦↦Cα𝔅"
        by (rule cf_const_is_functor)
          (simp_all add: 𝔅.category_axioms category_cat_1 b)
      then have 𝔊_def: "cf_const (cat_1 0 0) 𝔅 b = 𝔉" by (rule 𝔊𝔉) 
      have " (cf_const (cat_1 0 0) 𝔅 bObjMap) = set {b}" 
        unfolding dghm_const_components cat_1_components by simp
      with vrange_𝔉 ba show False unfolding 𝔊_def by simp  
    ultimately have "𝔅Obj = set {a}" by simp
    with that show ?thesis by simp

  have 𝔅_Arr: "𝔅Arr = set {𝔅CIda}"
  proof(rule vsubset_antisym)
    from 𝔅_Obj show "set {𝔅CIda}  𝔅Arr" 
      by (blast intro: 𝔅.cat_is_arrD(1) cat_cs_intros)
    show "𝔅Arr  set {𝔅CIda}"
    proof(intro vsubsetI)
      fix f assume "f  𝔅Arr" 
      with 𝔅_Obj have f: "f : a 𝔅a"
        by (metis 𝔅.cat_is_arrD(2,3) is_arrI vsingleton_iff)
      from f have "cf_const 𝔅 𝔅 a : 𝔅 ↦↦Cα𝔅"
        by (intro cf_const_is_functor) (auto simp: 𝔅.category_axioms)
      moreover from f have "cf_id 𝔅 : 𝔅 ↦↦Cα𝔅"
        by (intro category.cat_cf_id_is_functor)
          (auto simp: 𝔅.category_axioms)
      ultimately have "cf_const 𝔅 𝔅 a = cf_id 𝔅"
        by (metis prems(2) 𝔅.category_axioms)
      moreover from f have "cf_const 𝔅 𝔅 aArrMapf = 𝔅CIda" 
        by (simp add: f  𝔅Arr dghm_const_ArrMap_app)
      moreover from f have "cf_id 𝔅ArrMapf = f" 
        unfolding dghm_id_components by (simp add: cat_cs_intros)
      ultimately show "f  set {𝔅CIda}" by simp

  have "𝔅 = cat_1 a (𝔅CIda)"
  proof(rule cat_eqI[of α], unfold cat_1_components)
    from 𝔅.cat_Arr_vsubset_Vset 𝔅_Arr show "category α (cat_1 a (𝔅CIda))"
      by (intro category_cat_1) (auto simp: a)
    show "𝔅Arr = set {𝔅CIda}" by (simp add: 𝔅_Arr)
    then have "𝒟 (𝔅Dom) = set {𝔅CIda}" 
      by (simp add: cat_cs_simps cat_cs_intros)
    moreover have " (𝔅Dom) = set {a}"
      using 𝔅.cat_Dom_vrange 𝔅.cat_CId_is_arr 𝔅.cat_Dom_vdomain
      by (auto simp: 𝔅_Obj elim: 𝔅.Dom.vbrelation_vinE) (*slow*)
    ultimately show "𝔅Dom = set {𝔅CIda, a}"
      using 𝔅.Dom.vsv_vdomain_vrange_vsingleton by simp
    have "𝒟 (𝔅Cod) = set {𝔅CIda}" 
      by (simp add: 𝔅_Arr cat_cs_simps)
    moreover have " (𝔅Cod) = set {a}"
      using 𝔅.cat_Cod_vrange 𝔅.cat_CId_is_arr 𝔅.cat_Cod_vdomain 
      by (auto simp: 𝔅_Obj elim: 𝔅.Cod.vbrelation_vinE) (*slow*)
    ultimately show "𝔅Cod = set {𝔅CIda, a}"
      by (auto intro: 𝔅.Cod.vsv_vdomain_vrange_vsingleton)
    show "𝔅Comp = set {[𝔅CIda, 𝔅CIda], 𝔅CIda}"
    proof(rule vsv_eqI)
      show dom: 
        "𝒟 (𝔅Comp) = 𝒟 (set {[𝔅CIda, 𝔅CIda], 𝔅CIda})"
        unfolding vdomain_vsingleton
      proof(rule vsubset_antisym)
         show "𝒟 (𝔅Comp)  set {[𝔅CIda, 𝔅CIda]}"
           by (intro vsubsetI) 
             (metis 𝔅.cat_Comp_vdomain 𝔅_Arr vsingleton_iff 𝔅.cat_is_arrD(1))
        show "set {[𝔅CIda, 𝔅CIda]}  𝒟 (𝔅Comp)"
                𝔅_Obj vsingleton_iff 
      have "𝔅CIda A𝔅𝔅CIda = 𝔅CIda" 
        by (metis 𝔅_Obj 𝔅.cat_CId_is_arr 𝔅.cat_CId_left_left vsingletonI)
      then show "a'  𝒟 (𝔅Comp) 
        𝔅Compa' = set {[𝔅CIda, 𝔅CIda], 𝔅CIda}a'"
        for a'
        unfolding dom by simp
    qed (auto simp: 𝔅_Obj 𝔅_Arr)
    have "𝒟 (𝔅CId) = set {a}" by (simp add: 𝔅_Obj 𝔅.cat_CId_vdomain)
    moreover then have " (𝔅CId) = set {𝔅CIda}"
    ultimately show "𝔅CId = set {a, 𝔅CIda}"
      by (blast intro: 𝔅.CId.vsv_vdomain_vrange_vsingleton)
  qed (auto simp: 𝔅_Obj cat_cs_intros)

  with a that 𝔅.cat_Arr_vsubset_Vset 𝔅_Arr show ?thesis by auto