Theory CZH_ECAT_Simple

(* Copyright 2021 (C) Mihails Milehins *)

section‹Simple categories›
theory CZH_ECAT_Simple
  imports 
    CZH_Foundations.CZH_SMC_Simple
    CZH_ECAT_NTCF
    CZH_ECAT_Small_Functor
begin



subsection‹Background›


text‹
The section presents a variety of simple categories, 
(such as the empty category ‹0› and the singleton category ‹1›)
and functors between them (see \<^cite>‹"mac_lane_categories_2010"›
for further information).
›



subsection‹Empty category ‹0››


subsubsection‹Definition and elementary properties›


text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition cat_0 :: "V"
  where "cat_0 = [0, 0, 0, 0, 0, 0]⇩∘"


text‹Components.›

lemma cat_0_components:
  shows "cat_0⦇Obj⦈ = 0"
    and "cat_0⦇Arr⦈ = 0"
    and "cat_0⦇Dom⦈ = 0"
    and "cat_0⦇Cod⦈ = 0"
    and "cat_0⦇Comp⦈ = 0"
    and "cat_0⦇CId⦈ = 0"
  unfolding cat_0_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_cat_0: "cat_smc cat_0 = smc_0"
  unfolding cat_smc_def cat_0_def smc_0_def dg_field_simps
  by (simp add: nat_omega_simps)

lemmas_with (in 𝒵) [folded cat_smc_cat_0, unfolded slicing_simps]: 
  cat_0_is_arr_iff = smc_0_is_arr_iff


subsubsection‹‹0› is a category›

lemma (in 𝒵) category_cat_0[cat_cs_intros]: "category α cat_0"
proof(intro categoryI)
  show "vfsequence cat_0" "vcard cat_0 = 6⇩ℕ" 
    by (simp_all add: cat_0_def nat_omega_simps)
qed 
  (
    auto simp: 
      𝒵_axioms
      cat_0_components 
      cat_0_is_arr_iff 
      cat_smc_cat_0 
      𝒵.semicategory_smc_0
  )

lemmas [cat_cs_intros] = 𝒵.category_cat_0


subsubsection‹Opposite of the category ‹0››

lemma op_cat_cat_0[cat_op_simps]: "op_cat (cat_0) = cat_0"
proof(rule cat_smc_eqI)
  define β where "β = ω + ω"
  interpret β: 𝒵 β unfolding β_def by (rule 𝒵_ωω)
  show "category β (op_cat cat_0)"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  show "category β cat_0" by (cs_concl cs_shallow cs_intro: cat_cs_intros)
qed 
  (
    simp_all add:
      cat_0_components op_cat_components cat_smc_cat_0 
      slicing_commute[symmetric] smc_op_simps
  )



subsection‹Empty functors›


subsubsection‹Definition and elementary properties›

definition cf_0 :: "V ⇒ V"
  where "cf_0 𝔄 = [0, 0, cat_0, 𝔄]⇩∘"


text‹Components.›

lemma cf_0_components:
  shows "cf_0 𝔄⦇ObjMap⦈ = 0"
    and "cf_0 𝔄⦇ArrMap⦈ = 0"
    and "cf_0 𝔄⦇HomDom⦈ = cat_0"
    and "cf_0 𝔄⦇HomCod⦈ = 𝔄"
  unfolding cf_0_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cf_smcf_cf_0: "cf_smcf (cf_0 𝔄) = smcf_0 (cat_smc 𝔄)"
  unfolding 
    dg_field_simps dghm_field_simps 
    cf_smcf_def cf_0_def smc_0_def cat_0_def smcf_0_def cat_smc_def 
  by (simp add: nat_omega_simps)


text‹Opposite empty category homomorphism.›

lemma op_cf_cf_0: "op_cf (cf_0 ℭ) = cf_0 (op_cat ℭ)"
  unfolding 
    cf_0_def op_cat_def op_cf_def cat_0_def dghm_field_simps dg_field_simps
  by (simp add: nat_omega_simps)


subsubsection‹Object map›

lemma cf_0_ObjMap_vsv[cat_cs_intros]: "vsv (cf_0 ℭ⦇ObjMap⦈)"
  unfolding cf_0_components by simp


subsubsection‹Arrow map›

lemma cf_0_ArrMap_vsv[cat_cs_intros]: "vsv (cf_0 ℭ⦇ArrMap⦈)"
  unfolding cf_0_components by simp


subsubsection‹Empty functor is a faithful functor›

lemma cf_0_is_ft_functor: 
  assumes "category α 𝔄"
  shows "cf_0 𝔄 : cat_0 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔄"
proof(rule is_ft_functorI)
  interpret 𝔄: category α 𝔄 by (rule assms(1))
  show "cf_0 𝔄 : cat_0 ↦↦⇩C⇘α⇙ 𝔄"
  proof(rule is_functorI, unfold cat_smc_cat_0 cf_smcf_cf_0)
    show "vfsequence (cf_0 𝔄)" unfolding cf_0_def by simp
    show "vcard (cf_0 𝔄) = 4⇩ℕ"
      unfolding cf_0_def by (simp add: nat_omega_simps)
    from 𝒵.smcf_0_is_ft_semifunctor assms show 
      "smcf_0 (cat_smc 𝔄) : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔄"   
      by auto
  qed (auto simp: assms 𝔄.category_cat_0 cat_0_components cf_0_components)
  show "cf_smcf (cf_0 𝔄) : cat_smc cat_0 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ cat_smc 𝔄"
    by 
      (
        auto simp:
          assms 
          𝔄.𝒵_axioms
          𝔄.smcf_0_is_ft_semifunctor  
          category.cat_semicategory 
          cf_smcf_cf_0 
          cat_smc_cat_0
      )
qed

lemma cf_0_is_ft_functor'[cf_cs_intros]:
  assumes "category α 𝔄"
    and "𝔅' = 𝔄"
    and "𝔄' = cat_0"
  shows "cf_0 𝔄 : 𝔄' ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
  using assms(1) unfolding assms(2,3) by (rule cf_0_is_ft_functor)

lemma cf_0_is_functor: 
  assumes "category α 𝔄"
  shows "cf_0 𝔄 : cat_0 ↦↦⇩C⇘α⇙ 𝔄"
  using cf_0_is_ft_functor[OF assms] by auto

lemma cf_0_is_functor'[cat_cs_intros]: 
  assumes "category α 𝔄"
    and "𝔅' = 𝔄"
    and "𝔄' = cat_0"
  shows "cf_0 𝔄 : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
  using assms(1) unfolding assms(2,3) by (rule cf_0_is_functor)


subsubsection‹Further properties›

lemma is_functor_is_cf_0_if_cat_0:
  assumes "𝔉 : cat_0 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝔉 = cf_0 ℭ"
proof(rule cf_smcf_eqI)
  interpret 𝔉: is_functor α cat_0 ℭ 𝔉 by (rule assms(1))
  show "𝔉 : cat_0 ↦↦⇩C⇘α⇙ ℭ" by (rule assms(1))
  then have dom_lhs: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 0" "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 0" 
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_0_components)+
  show "cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "cf_smcf 𝔉 = cf_smcf (cf_0 ℭ)"
    unfolding cf_smcf_cf_0
    by 
      (
        rule is_semifunctor_is_smcf_0_if_smc_0, 
        rule 𝔉.cf_is_semifunctor[unfolded slicing_simps cat_smc_cat_0]
      )
qed simp_all 

lemma (in is_functor) cf_comp_cf_cf_0[cat_cs_simps]: "𝔉 ∘⇩C⇩F cf_0 𝔄 = cf_0 𝔅"
proof(rule cf_eqI)
  show "𝔉 ∘⇩C⇩F cf_0 𝔄 : cat_0 ↦↦⇩C⇘α⇙ 𝔅" by (cs_concl cs_intro: cat_cs_intros)
  then have ObjMap_dom_lhs: "𝒟⇩∘ ((𝔉 ∘⇩C⇩F cf_0 𝔄)⦇ObjMap⦈) = cat_0⦇Obj⦈"
    and ArrMap_dom_lhs: "𝒟⇩∘ ((𝔉 ∘⇩C⇩F cf_0 𝔄)⦇ArrMap⦈) = cat_0⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps)+
  show "cf_0 𝔅 : cat_0 ↦↦⇩C⇘α⇙ 𝔅" 
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  then have ObjMap_dom_rhs: "𝒟⇩∘ (cf_0 𝔅⦇ObjMap⦈) = cat_0⦇Obj⦈"
    and ArrMap_dom_rhs: "𝒟⇩∘ (cf_0 𝔅⦇ArrMap⦈) = cat_0⦇Arr⦈"
    by (cs_concl cs_simp: cat_cs_simps)+
  show "(𝔉 ∘⇩C⇩F cf_0 𝔄)⦇ObjMap⦈ = cf_0 𝔅⦇ObjMap⦈"
    by 
      (
        rule vsv_eqI, 
        unfold ObjMap_dom_lhs ObjMap_dom_rhs ArrMap_dom_lhs ArrMap_dom_rhs
      )
      (auto simp: cat_0_components intro: cat_cs_intros)
  show "(𝔉 ∘⇩C⇩F cf_0 𝔄)⦇ArrMap⦈ = cf_0 𝔅⦇ArrMap⦈"
    by 
      (
        rule vsv_eqI, 
        unfold ObjMap_dom_lhs ObjMap_dom_rhs ArrMap_dom_lhs ArrMap_dom_rhs
      )
      (auto simp: cat_0_components intro: cat_cs_intros)
qed simp_all

lemmas [cat_cs_simps] = is_functor.cf_comp_cf_cf_0



subsection‹Empty natural transformation›


subsubsection‹Definition and elementary properties›


text‹See Chapter X-1 in \<^cite>‹"mac_lane_categories_2010"›.›

definition ntcf_0 :: "V ⇒ V" 
  where "ntcf_0 ℭ = [0, cf_0 ℭ, cf_0 ℭ, cat_0, ℭ]⇩∘"


text‹Components.›

lemma ntcf_0_components:
  shows "ntcf_0 ℭ⦇NTMap⦈ = 0"
    and [cat_cs_simps]: "ntcf_0 ℭ⦇NTDom⦈ = cf_0 ℭ"
    and [cat_cs_simps]: "ntcf_0 ℭ⦇NTCod⦈ = cf_0 ℭ"
    and [cat_cs_simps]: "ntcf_0 ℭ⦇NTDGDom⦈ = cat_0"
    and [cat_cs_simps]: "ntcf_0 ℭ⦇NTDGCod⦈ = ℭ"
  unfolding ntcf_0_def nt_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma ntcf_ntsmcf_ntcf_0: "ntcf_ntsmcf (ntcf_0 𝔄) = ntsmcf_0 (cat_smc 𝔄)"
  unfolding 
    ntcf_ntsmcf_def ntcf_0_def ntsmcf_0_def cat_smc_def
    cf_smcf_def smcf_0_def cf_0_def cat_0_def smc_0_def
    dg_field_simps dghm_field_simps nt_field_simps
  by (simp add: nat_omega_simps)


text‹Duality.›

lemma op_ntcf_ntcf_0: "op_ntcf (ntcf_0 ℭ) = ntcf_0 (op_cat ℭ)"
  by
    (
      simp_all add:
        op_ntcf_def ntcf_0_def op_cat_def op_cf_cf_0 cat_0_def
        nt_field_simps dg_field_simps nat_omega_simps
    )


subsubsection‹Natural transformation map›

lemma ntcf_0_NTMap_vsv[cat_cs_intros]: "vsv (ntcf_0 ℭ⦇NTMap⦈)"
  unfolding ntcf_0_components by simp

lemma ntcf_0_NTMap_vdomain[cat_cs_simps]: "𝒟⇩∘ (ntcf_0 ℭ⦇NTMap⦈) = 0"
  unfolding ntcf_0_components by simp

lemma ntcf_0_NTMap_vrange[cat_cs_simps]: "ℛ⇩∘ (ntcf_0 ℭ⦇NTMap⦈) = 0"
  unfolding ntcf_0_components by simp


subsubsection‹Empty natural transformation is a natural transformation›

lemma (in category) cat_ntcf_0_is_ntcfI: 
  "ntcf_0 ℭ : cf_0 ℭ ↦⇩C⇩F cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_ntcfI)
  show "vfsequence (ntcf_0 ℭ)" unfolding ntcf_0_def by simp
  show "vcard (ntcf_0 ℭ) = 5⇩ℕ"
    unfolding ntcf_0_def by (simp add: nat_omega_simps)
  show "ntcf_ntsmcf (ntcf_0 ℭ) :
    cf_smcf (cf_0 ℭ) ↦⇩S⇩M⇩C⇩F cf_smcf (cf_0 ℭ) :
    cat_smc cat_0 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
    unfolding ntcf_ntsmcf_ntcf_0 cf_smcf_cf_0 cat_smc_cat_0
    by (cs_concl cs_shallow cs_intro: smc_cs_intros slicing_intros)
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+

lemma (in category) cat_ntcf_0_is_ntcfI'[cat_cs_intros]:
  assumes "𝔉' = cf_0 ℭ"
    and "𝔊' = cf_0 ℭ"
    and "𝔄' = cat_0"
    and "𝔅' = ℭ"
    and "𝔉' = 𝔉"
    and "𝔊' = 𝔊"
  shows "ntcf_0 ℭ : 𝔉' ↦⇩C⇩F 𝔊' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
  unfolding assms by (rule cat_ntcf_0_is_ntcfI)

lemmas [cat_cs_intros] = category.cat_ntcf_0_is_ntcfI'

lemma is_ntcf_is_ntcf_0_if_cat_0:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : cat_0 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝔑 = ntcf_0 ℭ" and "𝔉 = cf_0 ℭ" and "𝔊 = cf_0 ℭ"
proof-
  interpret 𝔑: is_ntcf α cat_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  note is_ntsmcf_is_ntsmcf_0_if_smc_0 = is_ntsmcf_is_ntsmcf_0_if_smc_0
    [
      OF 𝔑.ntcf_is_ntsmcf[unfolded cat_smc_cat_0], 
      folded smcf_dghm_smcf_0 ntsmcf_tdghm_ntsmcf_0
    ]
  show 𝔉_def: "𝔉 = cf_0 ℭ" and 𝔊_def: "𝔊 = cf_0 ℭ"
    by (all‹intro is_functor_is_cf_0_if_cat_0›)
      (cs_concl cs_shallow cs_intro: cat_cs_intros)+
  show "𝔑 = ntcf_0 ℭ" 
  proof(rule ntcf_ntsmcf_eqI)
    show "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : cat_0 ↦↦⇩C⇘α⇙ ℭ" by (rule assms(1))
    show "ntcf_0 ℭ : 𝔉 ↦⇩C⇩F 𝔊 : cat_0 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_shallow cs_simp: 𝔉_def 𝔊_def cs_intro: cat_cs_intros)
  qed 
    (
      simp_all add: 
        𝔉_def 𝔊_def is_ntsmcf_is_ntsmcf_0_if_smc_0 ntcf_ntsmcf_ntcf_0
    )
qed


subsubsection‹Further properties›

lemma ntcf_vcomp_ntcf_ntcf_0[cat_cs_simps]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : cat_0 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_0 ℭ = ntcf_0 ℭ"
proof(rule ntcf_ntsmcf_eqI)
  interpret 𝔑: is_ntcf α cat_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  show "𝔑 ∙⇩N⇩T⇩C⇩F ntcf_0 ℭ : cf_0 ℭ ↦⇩C⇩F cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ"
    unfolding is_ntcf_is_ntcf_0_if_cat_0[OF assms]
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_0 ℭ : cf_0 ℭ ↦⇩C⇩F cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_ntsmcf (𝔑 ∙⇩N⇩T⇩S⇩M⇩C⇩F ntcf_0 ℭ) = ntcf_ntsmcf (ntcf_0 ℭ)"
    unfolding 
      slicing_commute[symmetric]
      ntsmcf_vcomp_ntsmcf_ntsmcf_0
        [
          OF 𝔑.ntcf_is_ntsmcf[unfolded cat_smc_cat_0], 
          folded ntcf_ntsmcf_ntcf_0
        ]
      ..
qed simp_all

lemma ntcf_vcomp_ntcf_0_ntcf[cat_cs_simps]:
  assumes "𝔑 : 𝔉 ↦⇩C⇩F 𝔊 : cat_0 ↦↦⇩C⇘α⇙ ℭ"
  shows "ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F 𝔑 = ntcf_0 ℭ"
proof(rule ntcf_ntsmcf_eqI)
  interpret 𝔑: is_ntcf α cat_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
  show "ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F 𝔑 : cf_0 ℭ ↦⇩C⇩F cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ"
    unfolding is_ntcf_is_ntcf_0_if_cat_0[OF assms]
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_0 ℭ : cf_0 ℭ ↦⇩C⇩F cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "ntcf_ntsmcf (ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F 𝔑) = ntcf_ntsmcf (ntcf_0 ℭ)"
    unfolding 
      slicing_commute[symmetric]
      ntsmcf_vcomp_ntsmcf_0_ntsmcf
        [
          OF 𝔑.ntcf_is_ntsmcf[unfolded cat_smc_cat_0], 
          folded ntcf_ntsmcf_ntcf_0
        ]
      ..
  qed simp_all

lemma (in is_functor) cf_ntcf_comp_cf_ntcf_0[cat_cs_simps]: 
  "𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_0 𝔄 = ntcf_0 𝔅"
proof(rule ntcf_eqI)
  show "𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_0 𝔄 : cf_0 𝔅 ↦⇩C⇩F cf_0 𝔅 : cat_0 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟⇩∘ ((𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_0 𝔄)⦇NTMap⦈) = cat_0⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  show "ntcf_0 𝔅 : cf_0 𝔅 ↦⇩C⇩F cf_0 𝔅 : cat_0 ↦↦⇩C⇘α⇙ 𝔅"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  then have dom_rhs: "𝒟⇩∘ (ntcf_0 𝔅⦇NTMap⦈) = cat_0⦇Obj⦈"
    by (cs_concl cs_simp: cat_cs_simps)
  show "(𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_0 𝔄)⦇NTMap⦈ = ntcf_0 𝔅⦇NTMap⦈"
    by (rule vsv_eqI, unfold dom_lhs dom_rhs)
      (auto simp: cat_0_components intro!: cat_cs_intros)+
qed simp_all

lemmas [cat_cs_simps] = is_functor.cf_ntcf_comp_cf_ntcf_0



subsection‹‹1›: category with one object and one arrow›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition cat_1 :: "V ⇒ V ⇒ V"
  where "cat_1 𝔞 𝔣 =
    [
      set {𝔞},
      set {𝔣},
      set {⟨𝔣, 𝔞⟩},
      set {⟨𝔣, 𝔞⟩},
      set {⟨[𝔣, 𝔣]⇩∘, 𝔣⟩},
      set {⟨𝔞, 𝔣⟩}
    ]⇩∘"


text‹Components.›

lemma cat_1_components:
  shows "cat_1 𝔞 𝔣⦇Obj⦈ = set {𝔞}"
    and "cat_1 𝔞 𝔣⦇Arr⦈ = set {𝔣}"
    and "cat_1 𝔞 𝔣⦇Dom⦈ = set {⟨𝔣, 𝔞⟩}"
    and "cat_1 𝔞 𝔣⦇Cod⦈ = set {⟨𝔣, 𝔞⟩}"
    and "cat_1 𝔞 𝔣⦇Comp⦈ = set {⟨[𝔣, 𝔣]⇩∘, 𝔣⟩}"
    and "cat_1 𝔞 𝔣⦇CId⦈ = set {⟨𝔞, 𝔣⟩}"
  unfolding cat_1_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smc_cat_1: "cat_smc (cat_1 𝔞 𝔣) = smc_1 𝔞 𝔣"
  unfolding cat_smc_def cat_1_def smc_1_def dg_field_simps
  by (simp add: nat_omega_simps)

lemmas_with [folded smc_cat_1, unfolded slicing_simps]: 
  cat_1_is_arrI = smc_1_is_arrI
  and cat_1_is_arrD = smc_1_is_arrD
  and cat_1_is_arrE = smc_1_is_arrE
  and cat_1_is_arr_iff = smc_1_is_arr_iff
  and cat_1_Comp_app[cat_cs_simps] = smc_1_Comp_app


subsubsection‹Object›

lemma cat_1_ObjI[cat_cs_intros]:
  assumes "a = 𝔞"
  shows "a ∈⇩∘ cat_1 𝔞 𝔣 ⦇Obj⦈"
  unfolding cat_1_components(1) assms by simp


subsubsection‹Identity›

lemma cat_1_CId_app: "cat_1 𝔞 𝔣⦇CId⦈⦇𝔞⦈ = 𝔣" 
  unfolding cat_1_components by simp


subsubsection‹‹1› is a category›

lemma (in 𝒵) category_cat_1: 
  assumes "𝔞 ∈⇩∘ Vset α" and "𝔣 ∈⇩∘ Vset α" 
  shows "category α (cat_1 𝔞 𝔣)"
proof(intro categoryI, unfold smc_cat_1)
  show "vfsequence (cat_1 𝔞 𝔣)"
    unfolding cat_1_def by (simp add: nat_omega_simps)
  show "vcard (cat_1 𝔞 𝔣) = 6⇩ℕ"
    unfolding cat_1_def by (simp add: nat_omega_simps)
qed (auto simp: assms semicategory_smc_1 cat_1_is_arr_iff cat_1_components)

lemmas [cat_cs_intros] = 𝒵.category_cat_1

lemma (in 𝒵) finite_category_cat_1: 
  assumes "𝔞 ∈⇩∘ Vset α" and "𝔣 ∈⇩∘ Vset α" 
  shows "finite_category α (cat_1 𝔞 𝔣)"
  by (intro finite_categoryI')
    (auto simp: cat_1_components intro: category_cat_1[OF assms])

lemmas [cat_small_cs_intros] = 𝒵.finite_category_cat_1


subsubsection‹Opposite of the category ‹1››

lemma (in 𝒵) cat_1_op[cat_op_simps]:
  assumes "𝔞 ∈⇩∘ Vset α" and "𝔣 ∈⇩∘ Vset α"
  shows "op_cat (cat_1 𝔞 𝔣) = cat_1 𝔞 𝔣"
proof(rule cat_eqI, unfold cat_op_simps)
  from assms show "category α (op_cat (cat_1 𝔞 𝔣))"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
  from assms show "category α (cat_1 𝔞 𝔣)"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show "op_cat (cat_1 𝔞 𝔣)⦇Comp⦈ = cat_1 𝔞 𝔣⦇Comp⦈"
    unfolding cat_1_components op_cat_components fflip_vsingleton ..
qed (simp_all add: cat_1_components)

lemma (in 𝒵) cat_1_op_0[cat_op_simps]: "op_cat (cat_1 0 0) = cat_1 0 0"
  by 
    (
      cs_concl cs_shallow 
        cs_simp: cat_op_simps cs_intro: V_cs_intros cat_cs_intros
    )


subsubsection‹Further properties›

lemma cf_const_if_HomCod_is_cat_1:
  assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ cat_1 𝔞 𝔣"
  shows "𝔎 = cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞"
proof(rule cf_eqI)
  interpret 𝔎: is_functor α 𝔅 ‹cat_1 𝔞 𝔣› 𝔎 by (rule assms(1))
  show "cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞 : 𝔅 ↦↦⇩C⇘α⇙ cat_1 𝔞 𝔣"
    by (cs_concl cs_intro: cat_cs_intros)
  have ObjMap_dom_lhs: "𝒟⇩∘ (𝔎⦇ObjMap⦈) = 𝔅⦇Obj⦈" by (simp add: cat_cs_simps)
  have ObjMap_dom_rhs: "𝒟⇩∘ (cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞⦇ObjMap⦈) = 𝔅⦇Obj⦈"
    by (simp add: cat_cs_simps)
  have ArrMap_dom_lhs: "𝒟⇩∘ (𝔎⦇ArrMap⦈) = 𝔅⦇Arr⦈" by (simp add: cat_cs_simps)
  have ArrMap_dom_rhs: "𝒟⇩∘ (cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞⦇ArrMap⦈) = 𝔅⦇Arr⦈"
    by (simp add: cat_cs_simps)
  show "𝔎⦇ObjMap⦈ = cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞⦇ObjMap⦈"
  proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
    fix a assume prems: "a ∈⇩∘ 𝔅⦇Obj⦈"
    then have "𝔎⦇ObjMap⦈⦇a⦈ ∈⇩∘ cat_1 𝔞 𝔣⦇Obj⦈"
      by (auto intro: 𝔎.cf_ObjMap_app_in_HomCod_Obj)
    then have "𝔎⦇ObjMap⦈⦇a⦈ = 𝔞" by (auto simp: cat_1_components)
    with prems show "𝔎⦇ObjMap⦈⦇a⦈ = cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞⦇ObjMap⦈⦇a⦈"
      by (auto simp: cat_cs_simps)
  qed (auto intro: cat_cs_intros)
  show "𝔎⦇ArrMap⦈ = cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞⦇ArrMap⦈"
  proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
    fix a assume prems: "a ∈⇩∘ 𝔅⦇Arr⦈"
    then have "𝔎⦇ArrMap⦈⦇a⦈ ∈⇩∘ cat_1 𝔞 𝔣⦇Arr⦈"
      by (auto intro: 𝔎.cf_ArrMap_app_in_HomCod_Arr)
    then have "𝔎⦇ArrMap⦈⦇a⦈ = 𝔣" by (auto simp: cat_1_components)
    with prems show "𝔎⦇ArrMap⦈⦇a⦈ = cf_const 𝔅 (cat_1 𝔞 𝔣) 𝔞⦇ArrMap⦈⦇a⦈"
      by (auto simp: cat_1_CId_app cat_cs_simps)
  qed (auto intro: cat_cs_intros)
qed (simp_all add: assms)

lemma cf_const_if_HomDom_is_cat_1:
  assumes "𝔎 : cat_1 𝔞 𝔣 ↦↦⇩C⇘α⇙ ℭ"
  shows "𝔎 = cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)"
proof-

  interpret 𝔎: is_functor α ‹cat_1 𝔞 𝔣› ℭ 𝔎 by (rule assms(1))

  from cat_1_components(1) have 𝔞: "𝔞 ∈⇩∘ Vset α" 
    by (auto simp: 𝔎.HomDom.cat_in_Obj_in_Vset)
  from cat_1_components(2) have 𝔣: "𝔣 ∈⇩∘ Vset α" 
    by (auto simp: 𝔎.HomDom.cat_in_Arr_in_Vset)

  from 𝔞 𝔣 interpret cf_1: 
    is_tm_functor α ‹cat_1 𝔞 𝔣› ℭ ‹cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)›
    by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
  
  show ?thesis
  proof(rule cf_eqI)
    show "cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈) : cat_1 𝔞 𝔣 ↦↦⇩C⇘α⇙ ℭ"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    have ObjMap_dom_lhs: "𝒟⇩∘ (𝔎⦇ObjMap⦈) = set {𝔞}" 
      by (simp add: cat_cs_simps cat_1_components)
    have ObjMap_dom_rhs: 
      "𝒟⇩∘ (cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)⦇ObjMap⦈) = set {𝔞}"
      by (simp add: cat_cs_simps cat_1_components)
    show "𝔎⦇ObjMap⦈ = cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)⦇ObjMap⦈"
    proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      fix a assume "a ∈⇩∘ set {𝔞}"
      then have a_def: "a = 𝔞" by simp
      show "𝔎⦇ObjMap⦈⦇a⦈ = cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)⦇ObjMap⦈⦇a⦈"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_1_components(1) cat_cs_simps a_def 
              cs_intro: V_cs_intros
          )
    qed auto

    have ArrMap_dom_lhs: "𝒟⇩∘ (𝔎⦇ArrMap⦈) = set {𝔣}" 
      by (simp add: cat_cs_simps cat_1_components)
    have ArrMap_dom_rhs: 
      "𝒟⇩∘ (cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)⦇ArrMap⦈) = set {𝔣}"
      by (simp add: cat_cs_simps cat_1_components)
    
    show "𝔎⦇ArrMap⦈ = cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)⦇ArrMap⦈"
    proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      fix f assume "f ∈⇩∘ set {𝔣}"
      then have f_def: "f = 𝔣" by simp
      show "𝔎⦇ArrMap⦈⦇f⦈ = cf_const (cat_1 𝔞 𝔣) ℭ (𝔎⦇ObjMap⦈⦇𝔞⦈)⦇ArrMap⦈⦇f⦈"
        unfolding f_def
        by (subst cat_1_CId_app[symmetric, of 𝔣 𝔞])
          (
            cs_concl cs_shallow
              cs_simp: cat_1_components(1,2) cat_cs_simps 
              cs_intro: V_cs_intros cat_cs_intros
          )
    qed auto

  qed (simp_all add: assms)

qed

text‹\newpage›

end