(* Copyright 2021 (C) Mihails Milehins *)

theory CZH_ECAT_SemiCAT


The methodology for the exposition of SemiCAT› as a category 
is analogous to the one used in cite"milehins_category_2021" 
for the exposition of SemiCAT› as a semicategory.

named_theorems cat_SemiCAT_simps
named_theorems cat_SemiCAT_intros

subsection‹Definition and elementary properties›

definition cat_SemiCAT :: "V  V"
  where "cat_SemiCAT α =
      set {. semicategory α }, 
      all_smcfs α, 
      (λ𝔉all_smcfs α. 𝔉HomDom), 
      (λ𝔉all_smcfs α. 𝔉HomCod),
      (λ𝔊𝔉composable_arrs (dg_SemiCAT α). 𝔊𝔉0 SMCF 𝔊𝔉1),
      (λset {. semicategory α }. smcf_id )


lemma cat_SemiCAT_components:
  shows "cat_SemiCAT αObj = set {. semicategory α }"
    and "cat_SemiCAT αArr = all_smcfs α"
    and "cat_SemiCAT αDom = (λ𝔉all_smcfs α. 𝔉HomDom)"
    and "cat_SemiCAT αCod = (λ𝔉all_smcfs α. 𝔉HomCod)"
    and "cat_SemiCAT αComp = 
      (λ𝔊𝔉composable_arrs (dg_SemiCAT α). 𝔊𝔉0 SMCF 𝔊𝔉1)"
    and "cat_SemiCAT αCId = (λset {. semicategory α }. smcf_id )"
  unfolding cat_SemiCAT_def dg_field_simps 
  by (simp_all add: nat_omega_simps)


lemma cat_smc_SemiCAT: "cat_smc (cat_SemiCAT α) = smc_SemiCAT α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟 (cat_smc (cat_SemiCAT α)) = 5" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟 (smc_SemiCAT α) = 5"
    unfolding smc_SemiCAT_def by (simp add: nat_omega_simps)
  show "𝒟 (cat_smc (cat_SemiCAT α)) = 𝒟 (smc_SemiCAT α)"
    unfolding dom_lhs dom_rhs by simp
  show "a  𝒟 (cat_smc (cat_SemiCAT α))  
    cat_smc (cat_SemiCAT α)a = smc_SemiCAT αa"
    for a
        unfold dom_lhs, 
        unfold cat_smc_def dg_field_simps cat_SemiCAT_def smc_SemiCAT_def
      (auto simp: nat_omega_simps)
qed (auto simp: cat_smc_def smc_SemiCAT_def)

lemmas_with [folded cat_smc_SemiCAT, unfolded slicing_simps]: 
  cat_SemiCAT_ObjI = smc_SemiCAT_ObjI
  and cat_SemiCAT_ObjD = smc_SemiCAT_ObjD
  and cat_SemiCAT_ObjE = smc_SemiCAT_ObjE
  and cat_SemiCAT_Obj_iff[cat_SemiCAT_simps] = smc_SemiCAT_Obj_iff  
  and cat_SemiCAT_Dom_app[cat_SemiCAT_simps] = smc_SemiCAT_Dom_app
  and cat_SemiCAT_Cod_app[cat_SemiCAT_simps] = smc_SemiCAT_Cod_app
  and cat_SemiCAT_is_arrI = smc_SemiCAT_is_arrI
  and cat_SemiCAT_is_arrD = smc_SemiCAT_is_arrD
  and cat_SemiCAT_is_arrE = smc_SemiCAT_is_arrE
  and cat_SemiCAT_is_arr_iff[cat_SemiCAT_simps] = smc_SemiCAT_is_arr_iff

lemmas_with [
    folded cat_smc_SemiCAT, unfolded slicing_simps, unfolded cat_smc_SemiCAT
  cat_SemiCAT_Comp_vdomain = smc_SemiCAT_Comp_vdomain
  and cat_SemiCAT_composable_arrs_dg_SemiCAT = 
  and cat_SemiCAT_Comp = smc_SemiCAT_Comp
  and cat_SemiCAT_Comp_app[cat_SemiCAT_simps] = smc_SemiCAT_Comp_app
  and cat_SemiCAT_Comp_vrange = smc_SemiCAT_Comp_vrange

lemmas_with (in 𝒵) [folded cat_smc_SemiCAT, unfolded slicing_simps]: 
  cat_SemiCAT_obj_initialI = smc_SemiCAT_obj_initialI
  and cat_SemiCAT_obj_initialD = smc_SemiCAT_obj_initialD
  and cat_SemiCAT_obj_initialE = smc_SemiCAT_obj_initialE
  and cat_SemiCAT_obj_initial_iff[cat_SemiCAT_simps] = 
  and cat_SemiCAT_obj_terminalI = smc_SemiCAT_obj_terminalI
  and cat_SemiCAT_obj_terminalE = smc_SemiCAT_obj_terminalE


lemma cat_SemiCAT_CId_app[cat_SemiCAT_simps]: 
  assumes "semicategory α "
  shows "cat_SemiCAT αCId = smcf_id "
  using assms unfolding cat_SemiCAT_components by simp

lemma cat_SemiCAT_CId_vdomain[cat_SemiCAT_simps]: 
  "𝒟 (cat_SemiCAT αCId) = set {. semicategory α }"
  unfolding cat_SemiCAT_components by auto

lemma cat_SemiCAT_CId_vrange: " (cat_SemiCAT αCId)  all_smcfs α"
proof(rule vsubsetI)
  fix  assume "   (cat_SemiCAT αCId)"
  then obtain 𝔄 
    where ℌ_def: " = cat_SemiCAT αCId𝔄" 
      and 𝔄: "𝔄  𝒟 (cat_SemiCAT αCId)"
    unfolding cat_SemiCAT_components by auto
  from 𝔄 have ℌ_def': " = smcf_id 𝔄" 
    unfolding ℌ_def cat_SemiCAT_CId_vdomain by (auto simp: cat_SemiCAT_CId_app)
  from 𝔄 semicategory.smc_smcf_id_is_semifunctor show "  all_smcfs α"
    unfolding ℌ_def' cat_SemiCAT_CId_vdomain by force

subsectionSemiCAT› is a category›

lemma (in 𝒵) tiny_category_cat_SemiCAT: 
  assumes "𝒵 β" and "α  β"
  shows "tiny_category β (cat_SemiCAT α)"
proof(intro tiny_categoryI)
  interpret β: 𝒵 β by (rule assms(1))
  show "vfsequence (cat_SemiCAT α)" unfolding cat_SemiCAT_def by simp
  show "vcard (cat_SemiCAT α) = 6"
    unfolding cat_SemiCAT_def by (simp add: nat_omega_simps)
  show "cat_SemiCAT αCId𝔅 Acat_SemiCAT α𝔉 = 𝔉"
    if "𝔉 : 𝔄 cat_SemiCAT α𝔅" for 𝔉 𝔄 𝔅
    using that 
    unfolding cat_SemiCAT_is_arr_iff
    by (cs_concl cs_simp: smc_cs_simps cat_SemiCAT_simps cs_intro: smc_cs_intros)
  show "𝔉 Acat_SemiCAT αcat_SemiCAT αCId𝔅 = 𝔉"
    if "𝔉 : 𝔅 cat_SemiCAT α" for 𝔉 𝔅 
    using that 
    unfolding cat_SemiCAT_is_arr_iff
    by (cs_concl cs_simp: smc_cs_simps cat_SemiCAT_simps cs_intro: smc_cs_intros)
    simp_all add: 


lemma cat_SemiCAT_is_iso_arrI: 
  assumes "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  shows "𝔉 : 𝔄 isocat_SemiCAT α𝔅"
proof(intro is_iso_arrI is_inverseI)
  interpret is_iso_semifunctor α 𝔄 𝔅 𝔉 by (rule assms)
  from assms show 𝔉: "𝔉 : 𝔄 cat_SemiCAT α𝔅"
    unfolding cat_SemiCAT_is_arr_iff by auto
  note iso_thms = is_iso_semifunctor_is_iso_arr[OF assms]
  from iso_thms(1) show inv_𝔉: "inv_smcf 𝔉 : 𝔅 cat_SemiCAT α𝔄"
    unfolding cat_SemiCAT_is_arr_iff by auto
  from assms show "𝔉 : 𝔄 cat_SemiCAT α𝔅"
    unfolding cat_SemiCAT_is_arr_iff by auto
  from assms have 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅" by auto
  show "inv_smcf 𝔉 Acat_SemiCAT α𝔉 = cat_SemiCAT αCId𝔄"
    unfolding cat_SemiCAT_CId_app[OF 𝔄] cat_SemiCAT_Comp_app[OF inv_𝔉 𝔉]
    by (rule iso_thms(2))
  show "𝔉 Acat_SemiCAT αinv_smcf 𝔉 = cat_SemiCAT αCId𝔅"
    unfolding cat_SemiCAT_CId_app[OF 𝔅] cat_SemiCAT_Comp_app[OF 𝔉 inv_𝔉]
    by (rule iso_thms(3))

lemma cat_SemiCAT_is_iso_arrD: 
  assumes "𝔉 : 𝔄 isocat_SemiCAT α𝔅"
  shows "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  from is_iso_arrD[OF assms] have 𝔉: "𝔉 : 𝔄 cat_SemiCAT α𝔅" 
    and "(𝔊. is_inverse (cat_SemiCAT α) 𝔊 𝔉)"
    by simp_all
  then obtain 𝔊 where 𝔊𝔉: "is_inverse (cat_SemiCAT α) 𝔊 𝔉" by clarsimp
  then obtain 𝔄' 𝔅' where 𝔊': "𝔊 : 𝔅' cat_SemiCAT α𝔄'"
    and 𝔉': "𝔉 : 𝔄' cat_SemiCAT α𝔅'"
    and 𝔊𝔉: "𝔊 Acat_SemiCAT α𝔉 = cat_SemiCAT αCId𝔄'"
    and 𝔉𝔊: "𝔉 Acat_SemiCAT α𝔊 = cat_SemiCAT αCId𝔅'"
    by auto
  from 𝔉 𝔉' have 𝔄': "𝔄' = 𝔄" and 𝔅': "𝔅' = 𝔅" by auto  
  from 𝔉 have 𝔉: "𝔉 : 𝔄 ↦↦SMCα𝔅" unfolding cat_SemiCAT_is_arr_iff by simp
  interpret is_semifunctor α 𝔄 𝔅 𝔉 by (rule 𝔉)
  have 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅" 
    by (cs_concl cs_intro: smc_cs_intros)+
  from 𝔊' have 𝔊: "𝔊 : 𝔅 ↦↦SMCα𝔄" 
    unfolding 𝔄' 𝔅' cat_SemiCAT_is_arr_iff by simp
  moreover from 𝔊𝔉 have "𝔊 SMCF 𝔉 = smcf_id 𝔄"
    unfolding 𝔄' cat_SemiCAT_Comp_app[OF 𝔊' 𝔉'] cat_SemiCAT_CId_app[OF 𝔄] 
    by simp
  moreover from 𝔉𝔊 have "𝔉 SMCF 𝔊 = smcf_id 𝔅"
    unfolding 𝔅' cat_SemiCAT_Comp_app[OF 𝔉' 𝔊'] cat_SemiCAT_CId_app[OF 𝔅] 
    by simp
  ultimately show ?thesis 
    using 𝔉 by (elim is_iso_arr_is_iso_semifunctor)

lemma cat_SemiCAT_is_iso_arrE: 
  assumes "𝔉 : 𝔄 isocat_SemiCAT α𝔅"
  obtains "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  using assms by (auto dest: cat_SemiCAT_is_iso_arrD)

lemma cat_SemiCAT_is_iso_arr_iff[cat_SemiCAT_simps]: 
  "𝔉 : 𝔄 isocat_SemiCAT α𝔅  𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
  using cat_SemiCAT_is_iso_arrI cat_SemiCAT_is_iso_arrD by auto

subsection‹Isomorphic objects›

lemma cat_SemiCAT_obj_isoI: 
  assumes "𝔄 SMCα𝔅"
  shows "𝔄 objcat_SemiCAT α𝔅"
  from iso_semicategoryD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 ↦↦SMC.isoα𝔅"
    by clarsimp
  from cat_SemiCAT_is_iso_arrI[OF this] show ?thesis by (rule obj_isoI)

lemma cat_SemiCAT_obj_isoD: 
  assumes "𝔄 objcat_SemiCAT α𝔅"
  shows "𝔄 SMCα𝔅"
  from obj_isoD[OF assms] obtain 𝔉 where "𝔉 : 𝔄 isocat_SemiCAT α𝔅" 
    by clarsimp
  from cat_SemiCAT_is_iso_arrD[OF this] show ?thesis
    by (rule iso_semicategoryI)

lemma cat_SemiCAT_obj_isoE: 
  assumes "𝔄 objcat_SemiCAT α𝔅"
  obtains "𝔄 SMCα𝔅"
  using assms by (auto simp: cat_SemiCAT_obj_isoD)

lemma cat_SemiCAT_obj_iso_iff[cat_SemiCAT_simps]: 
  "𝔄 objcat_SemiCAT α𝔅  𝔄 SMCα𝔅"
  using cat_SemiCAT_obj_isoI cat_SemiCAT_obj_isoD by (intro iffI) auto