Theory CZH_SMC_SemiCAT

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹SemiCAT› as a semicategory›
theory CZH_SMC_SemiCAT
  imports 
    CZH_DG_SemiCAT
    CZH_SMC_Simple
    CZH_SMC_Small_Semicategory
begin



subsection‹Background›


text‹
The subsection presents the theory of the semicategories of 
‹α›-semicategories.
It continues the development that was initiated in section 
\ref{sec:dg_SemiCAT}.
›

named_theorems smc_SemiCAT_simps
named_theorems smc_SemiCAT_intros



subsection‹Definition and elementary properties›

definition smc_SemiCAT :: "V ⇒ V"
  where "smc_SemiCAT α =
    [
      set {ℭ. semicategory α ℭ},
      all_smcfs α,
      (λ𝔉∈∘all_smcfs α. 𝔉⦇HomDom⦈),
      (λ𝔉∈∘all_smcfs α. 𝔉⦇HomCod⦈),
      (λ𝔊𝔉∈∘composable_arrs (dg_SemiCAT α). 𝔊𝔉⦇0⦈ ∘SMCF 𝔊𝔉⦇1ℕ⦈)
    ]∘"


text‹Components.›

lemma smc_SemiCAT_components:
  shows "smc_SemiCAT α⦇Obj⦈ = set {ℭ. semicategory α ℭ}"
    and "smc_SemiCAT α⦇Arr⦈ = all_smcfs α"
    and "smc_SemiCAT α⦇Dom⦈ = (λ𝔉∈∘all_smcfs α. 𝔉⦇HomDom⦈)"
    and "smc_SemiCAT α⦇Cod⦈ = (λ𝔉∈∘all_smcfs α. 𝔉⦇HomCod⦈)"
    and "smc_SemiCAT α⦇Comp⦈ =
      (λ𝔊𝔉∈∘composable_arrs (dg_SemiCAT α). 𝔊𝔉⦇0⦈ ∘SMCF 𝔊𝔉⦇1ℕ⦈)"
  unfolding smc_SemiCAT_def dg_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smc_dg_SemiCAT[smc_SemiCAT_simps]: "smc_dg (smc_SemiCAT α) = dg_SemiCAT α"
proof(rule vsv_eqI)
  show "vsv (smc_dg (smc_SemiCAT α))" unfolding smc_dg_def by auto
  show "vsv (dg_SemiCAT α)" unfolding dg_SemiCAT_def by auto
  have dom_lhs: "𝒟∘ (smc_dg (smc_SemiCAT α)) = 4ℕ" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ (dg_SemiCAT α) = 4ℕ"
    unfolding dg_SemiCAT_def by (simp add: nat_omega_simps)
  show "𝒟∘ (smc_dg (smc_SemiCAT α)) = 𝒟∘ (dg_SemiCAT α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ (smc_dg (smc_SemiCAT α)) ⟹ 
    smc_dg (smc_SemiCAT α)⦇a⦈ = dg_SemiCAT α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold smc_dg_def dg_field_simps smc_SemiCAT_def dg_SemiCAT_def
      )
      (auto simp: nat_omega_simps)
qed

lemmas_with [folded smc_dg_SemiCAT, unfolded slicing_simps]: 
  smc_SemiCAT_ObjI = dg_SemiCAT_ObjI
  and smc_SemiCAT_ObjD = dg_SemiCAT_ObjD
  and smc_SemiCAT_ObjE = dg_SemiCAT_ObjE
  and smc_SemiCAT_Obj_iff[smc_SemiCAT_simps] = dg_SemiCAT_Obj_iff  
  and smc_SemiCAT_Dom_app[smc_SemiCAT_simps] = dg_SemiCAT_Dom_app
  and smc_SemiCAT_Cod_app[smc_SemiCAT_simps] = dg_SemiCAT_Cod_app
  and smc_SemiCAT_is_arrI = dg_SemiCAT_is_arrI
  and smc_SemiCAT_is_arrD = dg_SemiCAT_is_arrD
  and smc_SemiCAT_is_arrE = dg_SemiCAT_is_arrE
  and smc_SemiCAT_is_arr_iff[smc_SemiCAT_simps] = dg_SemiCAT_is_arr_iff



subsection‹Composable arrows›

lemma smc_SemiCAT_composable_arrs_dg_SemiCAT: 
  "composable_arrs (dg_SemiCAT α) = composable_arrs (smc_SemiCAT α)"
  unfolding composable_arrs_def smc_dg_SemiCAT[symmetric] slicing_simps by auto

lemma smc_SemiCAT_Comp: 
  "smc_SemiCAT α⦇Comp⦈ = 
    (λ𝔊𝔉∈∘composable_arrs (smc_SemiCAT α). 𝔊𝔉⦇0⦈ ∘DGHM 𝔊𝔉⦇1ℕ⦈)"
  unfolding smc_SemiCAT_components smc_SemiCAT_composable_arrs_dg_SemiCAT ..



subsection‹Composition›

lemma smc_SemiCAT_Comp_app[smc_SemiCAT_simps]:
  assumes "𝔊 : 𝔅 ↦⇘smc_SemiCAT α⇙ ℭ" and "𝔉 : 𝔄 ↦⇘smc_SemiCAT α⇙ 𝔅"
  shows "𝔊 ∘A⇘smc_SemiCAT α⇙ 𝔉 = 𝔊 ∘SMCF 𝔉"
proof-
  from assms have "[𝔊, 𝔉]∘ ∈∘ composable_arrs (smc_SemiCAT α)" 
    by (auto simp: composable_arrsI)
  then show "𝔊 ∘A⇘smc_SemiCAT α⇙ 𝔉 = 𝔊 ∘SMCF 𝔉"
    unfolding smc_SemiCAT_Comp by (simp add: nat_omega_simps)
qed 

lemma smc_SemiCAT_Comp_vdomain[smc_SemiCAT_simps]: 
  "𝒟∘ (smc_SemiCAT α⦇Comp⦈) = composable_arrs (smc_SemiCAT α)" 
  unfolding smc_SemiCAT_Comp by auto                      

lemma smc_SemiCAT_Comp_vrange: "ℛ∘ (smc_SemiCAT α⦇Comp⦈) ⊆∘ all_smcfs α"
proof(rule vsubsetI)
  fix ℌ assume "ℌ ∈∘ ℛ∘ (smc_SemiCAT α⦇Comp⦈)"
  then obtain 𝔊𝔉 
    where ℌ_def: "ℌ = smc_SemiCAT α⦇Comp⦈⦇𝔊𝔉⦈"
      and "𝔊𝔉 ∈∘ 𝒟∘ (smc_SemiCAT α⦇Comp⦈)"
    unfolding smc_SemiCAT_components by (auto intro: composable_arrsI)
  then obtain 𝔊 𝔉 𝔄 𝔅 ℭ 
    where "𝔊𝔉 = [𝔊, 𝔉]∘" 
      and 𝔊: "𝔊 : 𝔅 ↦⇘smc_SemiCAT α⇙ ℭ" 
      and 𝔉: "𝔉 : 𝔄 ↦⇘smc_SemiCAT α⇙ 𝔅"
    by (auto simp: smc_SemiCAT_Comp_vdomain) 
  with ℌ_def have ℌ_def': "ℌ = 𝔊 ∘A⇘smc_SemiCAT α⇙ 𝔉" by simp
  from 𝔊 𝔉 show "ℌ ∈∘ all_smcfs α" 
    unfolding ℌ_def' by (auto intro: smc_cs_intros simp: smc_SemiCAT_simps)
qed



subsection‹‹SemiCAT› is a semicategory›

lemma (in 𝒵) tiny_semicategory_smc_SemiCAT: 
  assumes "𝒵 β" and "α ∈∘ β"
  shows "tiny_semicategory β (smc_SemiCAT α)"
proof(intro tiny_semicategoryI, unfold smc_SemiCAT_is_arr_iff)
  show "vfsequence (smc_SemiCAT α)" unfolding smc_SemiCAT_def by auto
  show "vcard (smc_SemiCAT α) = 5ℕ"
    unfolding smc_SemiCAT_def by (simp add: nat_omega_simps)
  show "(𝔊𝔉 ∈∘ 𝒟∘ (smc_SemiCAT α⦇Comp⦈)) ⟷
    (∃𝔊 𝔉 𝔅 ℭ 𝔄. 𝔊𝔉 = [𝔊, 𝔉]∘ ∧ 𝔊 : 𝔅 ↦↦SMC⇘α⇙ ℭ ∧ 𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅)"
    for 𝔊𝔉
    unfolding smc_SemiCAT_Comp_vdomain
  proof
    show "𝔊𝔉 ∈∘ composable_arrs (smc_SemiCAT α) ⟹ 
      ∃𝔊 𝔉 𝔅 ℭ 𝔄. 𝔊𝔉 = [𝔊, 𝔉]∘ ∧ 𝔊   : 𝔅 ↦↦SMC⇘α⇙ ℭ ∧ 𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅"
      by (elim composable_arrsE) (auto simp: smc_SemiCAT_is_arr_iff)
  next
    assume "∃𝔊 𝔉 𝔅 ℭ 𝔄. 𝔊𝔉 = [𝔊, 𝔉]∘ ∧ 𝔊 : 𝔅 ↦↦SMC⇘α⇙ ℭ ∧ 𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅"
    with smc_SemiCAT_is_arr_iff show "𝔊𝔉 ∈∘ composable_arrs (smc_SemiCAT α)"
      unfolding smc_SemiCAT_Comp_vdomain by (auto intro: smc_cs_intros)
  qed
  show "⟦ 𝔊 : 𝔅 ↦↦SMC⇘α⇙ ℭ; 𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅 ⟧ ⟹ 
    𝔊 ∘A⇘smc_SemiCAT α⇙ 𝔉 : 𝔄 ↦↦SMC⇘α⇙ ℭ"
    for 𝔊 𝔅 ℭ 𝔉 𝔄
    by (auto simp: smc_SemiCAT_simps intro: smc_cs_intros)
  fix ℌ ℭ 𝔇 𝔊 𝔅 𝔉 𝔄
  assume "ℌ : ℭ ↦↦SMC⇘α⇙ 𝔇" "𝔊 : 𝔅 ↦↦SMC⇘α⇙ ℭ" "𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅"
  moreover then have "𝔊 ∘SMCF 𝔉 : 𝔄 ↦↦SMC⇘α⇙ ℭ" "ℌ ∘SMCF 𝔊 : 𝔅 ↦↦SMC⇘α⇙ 𝔇" 
    by (auto intro: smc_cs_intros)
  ultimately show "ℌ ∘A⇘smc_SemiCAT α⇙ 𝔊 ∘A⇘smc_SemiCAT α⇙ 𝔉 = 
    ℌ ∘A⇘smc_SemiCAT α⇙ (𝔊 ∘A⇘smc_SemiCAT α⇙ 𝔉)"
    by 
      (
        simp add: 
          smc_SemiCAT_is_arr_iff smc_SemiCAT_Comp_app smcf_comp_assoc
      )
qed 
  (
    auto simp: 
      assms smc_dg_SemiCAT tiny_digraph_dg_SemiCAT smc_SemiCAT_components
  )



subsection‹Initial object›

lemma (in 𝒵) smc_SemiCAT_obj_initialI: "obj_initial (smc_SemiCAT α) smc_0"
  unfolding obj_initial_def
proof
  (
    intro obj_terminalI, 
    unfold smc_op_simps smc_SemiCAT_is_arr_iff smc_SemiCAT_Obj_iff
  )
  show "semicategory α smc_0" by (intro semicategory_smc_0)
  fix 𝔄 assume prems: "semicategory α 𝔄"
  interpret semicategory α 𝔄 using prems .
  show "∃!𝔉. 𝔉 : smc_0 ↦↦SMC⇘α⇙ 𝔄"
  proof
    show smcf_0: "smcf_0 𝔄 : smc_0 ↦↦SMC⇘α⇙ 𝔄"
      by 
        (
          simp add: 
            smcf_0_is_ft_semifunctor semicategory_axioms is_ft_semifunctor.axioms(1)
        )
    fix 𝔉 assume prems: "𝔉 : smc_0 ↦↦SMC⇘α⇙ 𝔄" 
    then interpret 𝔉: is_semifunctor α smc_0 𝔄 𝔉 .
    show "𝔉 = smcf_0 𝔄"
    proof(rule smcf_eqI)
      show "𝔉 : smc_0 ↦↦SMC⇘α⇙ 𝔄" by (auto simp: smc_cs_intros)
      from smcf_0 show "smcf_0 𝔄 : smc_0 ↦↦SMC⇘α⇙ 𝔄"
        unfolding smc_SemiCAT_is_arr_iff by simp
      have "𝒟∘ (𝔉⦇ObjMap⦈) = 0" by (auto simp: smc_0_components smc_cs_simps)
      with 𝔉.ObjMap.vdomain_vrange_is_vempty show "𝔉⦇ObjMap⦈ = smcf_0 𝔄⦇ObjMap⦈"
        unfolding smcf_0_components by (auto intro: 𝔉.ObjMap.vsv_vrange_vempty)
      have "𝒟∘ (𝔉⦇ArrMap⦈) = 0" by (auto simp: smc_0_components smc_cs_simps)
      with 𝔉.ArrMap.vdomain_vrange_is_vempty show "𝔉⦇ArrMap⦈ = smcf_0 𝔄⦇ArrMap⦈"
        unfolding smcf_0_components by (auto intro: 𝔉.ArrMap.vsv_vrange_vempty)
    qed (simp_all add: smcf_0_components)
  qed
qed

lemma (in 𝒵) smc_SemiCAT_obj_initialD:
  assumes "obj_initial (smc_SemiCAT α) 𝔄"
  shows "𝔄 = smc_0" 
  using assms unfolding obj_initial_def
proof
  (
    elim obj_terminalE,
    unfold smc_op_simps smc_SemiCAT_is_arr_iff smc_SemiCAT_Obj_iff
  )
  assume prems: 
    "semicategory α 𝔄" 
    "semicategory α 𝔅 ⟹ ∃!𝔉. 𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅" 
    for 𝔅
  from prems(2)[OF semicategory_smc_0] obtain 𝔉 where "𝔉 : 𝔄 ↦↦SMC⇘α⇙ smc_0" 
    by meson
  then interpret 𝔉: is_semifunctor α 𝔄 smc_0 𝔉 .
  have "ℛ∘ (𝔉⦇ObjMap⦈) ⊆∘ 0"
    unfolding smc_0_components(1)[symmetric]
    by (simp add: 𝔉.smcf_ObjMap_vrange)
  then have "𝔉⦇ObjMap⦈ = 0" by (auto intro: 𝔉.ObjMap.vsv_vrange_vempty)
  with 𝔉.smcf_ObjMap_vdomain have Obj[simp]: "𝔄⦇Obj⦈ = 0" by auto
  have "ℛ∘ (𝔉⦇ArrMap⦈) ⊆∘ 0"
    unfolding smc_0_components(2)[symmetric]
    by (simp add: 𝔉.smcf_ArrMap_vrange)
  then have "𝔉⦇ArrMap⦈ = 0" by (auto intro: 𝔉.ArrMap.vsv_vrange_vempty)
  with 𝔉.smcf_ArrMap_vdomain have Arr[simp]: "𝔄⦇Arr⦈ = 0" by auto
  from 𝔉.HomDom.Dom.vdomain_vrange_is_vempty have [simp]: "𝔄⦇Dom⦈ = 0"  
    by (auto simp: smc_cs_simps intro: 𝔉.HomDom.Dom.vsv_vrange_vempty)
  from 𝔉.HomDom.Cod.vdomain_vrange_is_vempty have [simp]: "𝔄⦇Cod⦈ = 0"
    by (auto simp: smc_cs_simps intro: 𝔉.HomDom.Cod.vsv_vrange_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)
  show "𝔄 = smc_0"
    by (rule smc_eqI[of α])
      (simp_all add: prems(1) smc_0_components semicategory_smc_0)
qed

lemma (in 𝒵) smc_SemiCAT_obj_initialE:
  assumes "obj_initial (smc_SemiCAT α) 𝔄"
  obtains "𝔄 = smc_0" 
  using assms by (auto dest: smc_SemiCAT_obj_initialD)

lemma (in 𝒵) smc_SemiCAT_obj_initial_iff[smc_SemiCAT_simps]:
  "obj_initial (smc_SemiCAT α) 𝔄 ⟷ 𝔄 = smc_0"
  using smc_SemiCAT_obj_initialI smc_SemiCAT_obj_initialD by auto



subsection‹Terminal object›

lemma (in 𝒵) smc_SemiCAT_obj_terminalI[smc_SemiCAT_intros]: 
  assumes "a ∈∘ Vset α" and "f ∈∘ Vset α"
  shows "obj_terminal (smc_SemiCAT α) (smc_1 a f)"
proof
  (
    intro obj_terminalI,
    unfold smc_op_simps smc_SemiCAT_is_arr_iff smc_SemiCAT_Obj_iff
  )
  fix 𝔄 assume "semicategory α 𝔄"
  then interpret semicategory α 𝔄 .
  show "∃!𝔉'. 𝔉' : 𝔄 ↦↦SMC⇘α⇙ smc_1 a f"
  proof
    show smcf_1: "smcf_const 𝔄 (smc_1 a f) a f : 𝔄 ↦↦SMC⇘α⇙ smc_1 a f"
      by 
        (
          auto 
            intro: smc_cs_intros smc_1_is_arrI smcf_const_is_semifunctor
            simp: assms semicategory_smc_1
        )
    fix 𝔉' assume "𝔉' : 𝔄 ↦↦SMC⇘α⇙ smc_1 a f"
    then interpret 𝔉': is_semifunctor α 𝔄 ‹smc_1 a f› 𝔉' .
    show "𝔉' = smcf_const 𝔄 (smc_1 a f) a f"
    proof(rule smcf_eqI, unfold dghm_const_components)
      show "smcf_const 𝔄 (smc_1 a f) a f : 𝔄 ↦↦SMC⇘α⇙ smc_1 a f" 
        by (rule smcf_1)
      show "𝔉'⦇ObjMap⦈ = vconst_on (𝔄⦇Obj⦈) a"
      proof(cases‹𝔄⦇Obj⦈ = 0›)
        case True
        with 𝔉'.ObjMap.vbrelation_vintersection_vdomain have "𝔉'⦇ObjMap⦈ = 0"
          by (auto simp: smc_cs_simps)
        with True show ?thesis by simp
      next
        case False
        then have "𝒟∘ (𝔉'⦇ObjMap⦈) ≠ 0" by (auto simp: smc_cs_simps)
        then have "ℛ∘ (𝔉'⦇ObjMap⦈) ≠ 0"
          by (simp add: 𝔉'.ObjMap.vsv_vdomain_vempty_vrange_vempty)
        moreover from 𝔉'.smcf_ObjMap_vrange have "ℛ∘ (𝔉'⦇ObjMap⦈) ⊆∘ set {a}"
          by (simp add: smc_1_components)
        ultimately have "ℛ∘ (𝔉'⦇ObjMap⦈) = set {a}" by auto
        then show ?thesis 
          by (intro vsv.vsv_is_vconst_onI) (auto simp: smc_cs_simps) 
      qed
      show "𝔉'⦇ArrMap⦈ = vconst_on (𝔄⦇Arr⦈) f"
      proof(cases‹𝔄⦇Arr⦈ = 0›)
        case True
        with 𝔉'.ArrMap.vdomain_vrange_is_vempty have "𝔉'⦇ArrMap⦈ = 0"
          by (simp add: smc_cs_simps 𝔉'.smcf_ArrMap_vsv vsv.vsv_vrange_vempty)
        with True show ?thesis by simp
      next
        case False
        then have "𝒟∘ (𝔉'⦇ArrMap⦈) ≠ 0" by (auto simp: smc_cs_simps)
        then have "ℛ∘ (𝔉'⦇ArrMap⦈) ≠ 0" 
          by (simp add: 𝔉'.ArrMap.vsv_vdomain_vempty_vrange_vempty)
        moreover from 𝔉'.smcf_ArrMap_vrange have "ℛ∘ (𝔉'⦇ArrMap⦈) ⊆∘ set {f}"
          by (simp add: smc_1_components)
        ultimately have "ℛ∘ (𝔉'⦇ArrMap⦈) = set {f}" by auto
        then show ?thesis 
          by (intro vsv.vsv_is_vconst_onI) (auto simp: smc_cs_simps)
      qed
    qed (auto intro: smc_cs_intros)
  qed 
qed (simp add: assms semicategory_smc_1)

lemma (in 𝒵) smc_SemiCAT_obj_terminalE: 
  assumes "obj_terminal (smc_SemiCAT α) 𝔅"
  obtains a f where "a ∈∘ Vset α" and "f ∈∘ Vset α" and "𝔅 = smc_1 a f"
  using assms
proof
  (
    elim obj_terminalE, 
    unfold smc_op_simps smc_SemiCAT_is_arr_iff smc_SemiCAT_Obj_iff
  )

  assume prems: 
    "semicategory α 𝔅" 
    "semicategory α 𝔄 ⟹ ∃!𝔉. 𝔉 : 𝔄 ↦↦SMC⇘α⇙ 𝔅" 
    for 𝔄
  interpret 𝔅: semicategory α 𝔅 by (rule prems(1))

  obtain a where 𝔅_Obj: "𝔅⦇Obj⦈ = set {a}" and a: "a ∈∘ Vset α"
  proof-
    have semicategory_smc_10: "semicategory α (smc_10 0)"
      by (intro semicategory_smc_10) auto
    from prems(2)[OF semicategory_smc_10] obtain 𝔉 
      where 𝔉: "𝔉 : smc_10 0 ↦↦SMC⇘α⇙ 𝔅" 
        and 𝔊𝔉: "𝔊 : smc_10 0 ↦↦SMC⇘α⇙ 𝔅 ⟹ 𝔊 = 𝔉" for 𝔊
      by fastforce
    interpret 𝔉: is_semifunctor α ‹smc_10 0› 𝔅 𝔉 by (rule 𝔉)
    have "𝒟∘ (𝔉⦇ObjMap⦈) = set {0}" 
      by (auto simp add: smc_10_components smc_cs_simps)
    then obtain a where vrange_𝔉[simp]: "ℛ∘ (𝔉⦇ObjMap⦈) = set {a}"
      by (auto intro: 𝔉.ObjMap.vsv_vdomain_vsingleton_vrange_vsingleton)
    with 𝔅.smc_Obj_vsubset_Vset 𝔉.smcf_ObjMap_vrange have [simp]: "a ∈∘ Vset α"
      by auto
    from 𝔉.smcf_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
      define 𝔊 where "𝔊 = [set {⟨0, b⟩}, 0, smc_10 0, 𝔅]∘"
      have 𝔊_components: 
        "𝔊⦇ObjMap⦈ = set {⟨0, b⟩}"
        "𝔊⦇ArrMap⦈ = 0"
        "𝔊⦇HomDom⦈ = smc_10 0"
        "𝔊⦇HomCod⦈ = 𝔅"
        unfolding 𝔊_def dghm_field_simps by (simp_all add: nat_omega_simps)
      have 𝔊: "𝔊 : smc_10 0 ↦↦SMC⇘α⇙ 𝔅"
      proof(rule is_semifunctorI, unfold 𝔊_components smc_10_components)
        show "vfsequence 𝔊" unfolding 𝔊_def by auto
        show "vcard 𝔊 = 4ℕ"
          unfolding 𝔊_def by (auto simp: nat_omega_simps)
        show "smcf_dghm 𝔊 : smc_dg (smc_10 0) ↦↦DG⇘α⇙ smc_dg 𝔅"
        proof(intro is_dghmI, unfold 𝔊_components dg_10_components smc_dg_smc_10)
          show "vfsequence (smcf_dghm 𝔊)" unfolding smcf_dghm_def by simp
          show "vcard (smcf_dghm 𝔊) = 4ℕ"
            unfolding smcf_dghm_def by (simp add: nat_omega_simps)
        qed 
          (
            auto simp: 
              slicing_simps slicing_intros slicing_commute smc_dg_smc_10 
              b 𝔊_components dg_10_is_arr_iff digraph_dg_10 
          )
      qed (auto simp: smc_cs_intros smc_10_is_arr_iff b vsubset_vsingleton_leftI)
      then have 𝔊_def: "𝔊 = 𝔉" by (rule 𝔊𝔉)
      have "ℛ∘ (𝔊⦇ObjMap⦈) = set {b}" unfolding 𝔊_components by simp
      with vrange_𝔉 ba show False unfolding 𝔊_def by simp  
    qed
    ultimately have "𝔅⦇Obj⦈ = set {a}" by simp
    with that show ?thesis by simp
  qed

  obtain f 
    where 𝔅_Arr: "𝔅⦇Arr⦈ = set {f}" 
      and f: "f ∈∘ Vset α"
      and ff_f: "f ∘A⇘𝔅⇙ f = f"
  proof-
    from prems(2)[OF semicategory_smc_1, of 0 0] obtain 𝔉 
      where "𝔉 : smc_1 0 0 ↦↦SMC⇘α⇙ 𝔅" 
        and "𝔊 : smc_1 0 0 ↦↦SMC⇘α⇙ 𝔅 ⟹ 𝔊 = 𝔉" 
      for 𝔊
      by fastforce
    then interpret 𝔉: is_semifunctor α ‹smc_1 0 0› 𝔅 𝔉 by force
    have "𝒟∘ (𝔉⦇ObjMap⦈) = set {0}" 
      by (simp add: smc_cs_simps smc_1_components)
    then obtain a' where "ℛ∘ (𝔉⦇ObjMap⦈) = set {a'}"
      by (auto intro: 𝔉.ObjMap.vsv_vdomain_vsingleton_vrange_vsingleton)
    with 𝔉.smcf_ObjMap_vrange have "ℛ∘ (𝔉⦇ObjMap⦈) = set {a}" 
      by (auto simp: 𝔅_Obj)
    have vdomain_𝔉: "𝒟∘ (𝔉⦇ArrMap⦈) = set {0}"
      by (simp add: smc_cs_simps smc_1_components)
    then obtain f where vrange_𝔉[simp]: "ℛ∘ (𝔉⦇ArrMap⦈) = set {f}"
      by (auto intro: 𝔉.ArrMap.vsv_vdomain_vsingleton_vrange_vsingleton)
    with 𝔅.smc_Arr_vsubset_Vset 𝔉.smcf_ArrMap_vrange have [simp]: "f ∈∘ Vset α"
      by auto
    from 𝔉.smcf_ArrMap_vrange have f_ss_𝔅: "set {f} ⊆∘ 𝔅⦇Arr⦈" by simp
    then have "f ∈∘ 𝔅⦇Arr⦈" by auto
    then have f: "f : a ↦⇘𝔅⇙ a"
      by (metis 𝔅_Obj 𝔅.smc_is_arrD(2,3) is_arrI vsingleton_iff)
    from vdomain_𝔉 𝔉.ArrMap.vsv_value have [simp]: "𝔉⦇ArrMap⦈⦇0⦈ = f" by auto
    from 𝔉.smcf_is_arr_HomCod(2) have [simp]: "𝔉⦇ObjMap⦈⦇0⦈ = a"
      by (auto simp: smc_1_is_arr_iff 𝔅_Obj)
    have "𝔉⦇ArrMap⦈⦇0⦈ ∘A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇0⦈ = 𝔉⦇ArrMap⦈⦇0⦈"
      by (metis smc_1_Comp_app 𝔉.smcf_ArrMap_Comp smc_1_is_arr_iff)
    then have ff_f[simp]: "f ∘A⇘𝔅⇙ f = f" by simp
    have id_𝔅: "smcf_id 𝔅 : 𝔅 ↦↦SMC⇘α⇙ 𝔅"
      by (simp add: 𝔅.smc_smcf_id_is_semifunctor)
    interpret id_𝔅: is_semifunctor α 𝔅 𝔅 ‹smcf_id 𝔅› by (rule id_𝔅)
    from prems(2)[OF 𝔅.semicategory_axioms] have 
      "𝔊 : 𝔅 ↦↦SMC⇘α⇙ 𝔅 ⟹ 𝔊 = smcf_id 𝔅" for 𝔊
      by (clarsimp simp: id_𝔅.is_semifunctor_axioms)
    moreover from f have "smcf_const 𝔅 𝔅 a f : 𝔅 ↦↦SMC⇘α⇙ 𝔅"
      by (intro smcf_const_is_semifunctor) (auto intro: smc_cs_intros)
    ultimately have const_eq_id: "smcf_const 𝔅 𝔅 a f = smcf_id 𝔅" by simp
    have "𝔅⦇Arr⦈ ⊆∘ set {f}"
    proof(rule ccontr)
      assume "¬𝔅⦇Arr⦈ ⊆∘ set {f}"
      then obtain g where gf: "g ≠ f" and g: "g ∈∘ 𝔅⦇Arr⦈" by force
      have g: "g : a ↦⇘𝔅⇙ a"
      proof(intro is_arrI)
        from g 𝔅_Obj show "𝔅⦇Dom⦈⦇g⦈ = a"
          by (metis 𝔅.smc_is_arrD(2) is_arr_def vsingleton_iff)
        from g 𝔅_Obj show "𝔅⦇Cod⦈⦇g⦈ = a"
          by (metis 𝔅.smc_is_arrD(3) is_arr_def vsingleton_iff)
      qed (auto simp: g)
      then have "smcf_const 𝔅 𝔅 a f⦇ArrMap⦈⦇g⦈ = f" 
        by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)       
      moreover from g have "smcf_id 𝔅⦇ArrMap⦈⦇g⦈ = g"
        by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)       
      ultimately show False using const_eq_id by (simp add: gf)
    qed
    with f_ss_𝔅 have "𝔅⦇Arr⦈ = set {f}" by simp
    with that show ?thesis by simp
  qed

  have "𝔅 = smc_1 a f"
  proof(rule smc_eqI [of α], unfold smc_1_components)
    show "𝔅⦇Obj⦈ = set {a}" by (simp add: 𝔅_Obj)
    moreover show "𝔅⦇Arr⦈ = set {f}" by (simp add: 𝔅_Arr)
    ultimately have dom: "𝔅⦇Dom⦈⦇f⦈ = a" and cod: "𝔅⦇Cod⦈⦇f⦈ = a"
      by (metis 𝔅.smc_is_arrE is_arr_def vsingleton_iff)+
    have "𝒟∘ (𝔅⦇Dom⦈) = set {f}" by (simp add: 𝔅_Arr smc_cs_simps)
    moreover from 𝔅.Dom.vsv_vrange_vempty 𝔅.smc_Dom_vdomain 𝔅.smc_Dom_vrange  
    have "ℛ∘ (𝔅⦇Dom⦈) = set {a}" 
      by (fastforce simp: 𝔅_Arr 𝔅_Obj)
    ultimately show "𝔅⦇Dom⦈ = set {⟨f, a⟩}"  
      using assms 𝔅.Dom.vsv_vdomain_vrange_vsingleton by simp
    have "𝒟∘ (𝔅⦇Cod⦈) = set {f}" by (simp add: 𝔅_Arr smc_cs_simps)
    moreover from 𝔅.Cod.vsv_vrange_vempty 𝔅.smc_Cod_vdomain 𝔅.smc_Cod_vrange  
    have "ℛ∘ (𝔅⦇Cod⦈) = set {a}" 
      by (fastforce simp: 𝔅_Arr 𝔅_Obj)
    ultimately show "𝔅⦇Cod⦈ = set {⟨f, a⟩}"  
      using assms 𝔅.Cod.vsv_vdomain_vrange_vsingleton by simp
    show "𝔅⦇Comp⦈ = set {⟨[f, f]∘, f⟩}"
    proof(rule vsv_eqI)
      show [simp]: "𝒟∘ (𝔅⦇Comp⦈) = 𝒟∘ (set {⟨[f, f]∘, f⟩})"
        unfolding vdomain_vsingleton
      proof(rule vsubset_antisym)
        from 𝔅.Comp.pnop_vdomain show "𝒟∘ (𝔅⦇Comp⦈) ⊆∘ set {[f, f]∘}"
          by (auto simp: 𝔅_Arr intro: smc_cs_intros) (*slow*)
        from 𝔅_Arr dom cod is_arrI show "set {[f, f]∘} ⊆∘ 𝒟∘ (𝔅⦇Comp⦈)"
          by (metis 𝔅.smc_Comp_vdomainI vsingletonI vsubset_vsingleton_leftI)
      qed
      from ff_f show "a ∈∘ 𝒟∘ (𝔅⦇Comp⦈) ⟹ 𝔅⦇Comp⦈⦇a⦈ = set {⟨[f, f]∘, f⟩}⦇a⦈" 
        for a
        by simp
    qed auto
  qed (auto intro: smc_cs_intros a f semicategory_smc_1)
  with a f that show ?thesis by auto

qed

text‹\newpage›

end