Theory CZH_SMC_Set

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Set› as a semicategory›
theory CZH_SMC_Set
  imports 
    CZH_DG_Set
    CZH_SMC_Par
    CZH_SMC_Subsemicategory
begin



subsection‹Background›


text‹
The methodology chosen for the exposition 
of ‹Set› as a semicategory is analogous to the 
one used in the previous chapter for the exposition 
of ‹Set› as a digraph. 
›

named_theorems smc_Set_cs_simps
named_theorems smc_Set_cs_intros

lemmas (in arr_Set) [smc_Set_cs_simps] = 
  dg_Rel_shared_cs_simps

lemmas (in arr_Set) [smc_cs_intros, smc_Set_cs_intros] = 
  arr_Set_axioms'

lemmas [smc_Set_cs_simps] =
  dg_Rel_shared_cs_simps
  arr_Set.arr_Set_ArrVal_vdomain
  arr_Set_comp_Set_id_Set_left
  arr_Set_comp_Set_id_Set_right

lemmas [smc_Set_cs_intros] = 
  dg_Rel_shared_cs_intros
  arr_Set_comp_Set



subsection‹‹Set› as a semicategory›


subsubsection‹Definition and elementary properties›

definition smc_Set :: "V ⇒ V"
  where "smc_Set α =
    [
      Vset α,
      set {T. arr_Set α T},
      (λT∈∘set {T. arr_Set α T}. T⦇ArrDom⦈),
      (λT∈∘set {T. arr_Set α T}. T⦇ArrCod⦈),
      (λST∈∘composable_arrs (dg_Set α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)
    ]∘"


text‹Components.›

lemma smc_Set_components:
  shows "smc_Set α⦇Obj⦈ = Vset α"
    and "smc_Set α⦇Arr⦈ = set {T. arr_Set α T}"
    and "smc_Set α⦇Dom⦈ = (λT∈∘set {T. arr_Set α T}. T⦇ArrDom⦈)"
    and "smc_Set α⦇Cod⦈ = (λT∈∘set {T. arr_Set α T}. T⦇ArrCod⦈)"
    and "smc_Set α⦇Comp⦈ = (λST∈∘composable_arrs (dg_Set α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)"
  unfolding smc_Set_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smc_dg_smc_Set: "smc_dg (smc_Set α) = dg_Set α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟∘ (smc_dg (smc_Set α)) = 4ℕ" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ (dg_Set α) = 4ℕ"
    unfolding dg_Set_def by (simp add: nat_omega_simps)
  show "𝒟∘ (smc_dg (smc_Set α)) = 𝒟∘ (dg_Set α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ (smc_dg (smc_Set α)) ⟹ smc_dg (smc_Set α)⦇a⦈ = dg_Set α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral,
        unfold smc_dg_def dg_field_simps smc_Set_def dg_Set_def
      )
      (auto simp: nat_omega_simps)
qed (auto simp: smc_dg_def dg_Set_def)

lemmas_with [folded smc_dg_smc_Set, unfolded slicing_simps]: 
  smc_Set_Obj_iff = dg_Set_Obj_iff
  and smc_Set_Arr_iff[smc_Set_cs_simps] = dg_Set_Arr_iff
  and smc_Set_Dom_vsv[smc_Set_cs_intros] = dg_Set_Dom_vsv
  and smc_Set_Dom_vdomain[smc_Set_cs_simps] = dg_Set_Dom_vdomain
  and smc_Set_Dom_vrange = dg_Set_Dom_vrange
  and smc_Set_Dom_app[smc_Set_cs_simps] = dg_Set_Dom_app
  and smc_Set_Cod_vsv[smc_Set_cs_intros] = dg_Set_Cod_vsv
  and smc_Set_Cod_vdomain[smc_Set_cs_simps] = dg_Set_Cod_vdomain
  and smc_Set_Cod_vrange = dg_Set_Cod_vrange
  and smc_Set_Cod_app[smc_Set_cs_simps] = dg_Set_Cod_app
  and smc_Set_is_arrI = dg_Set_is_arrI
  and smc_Set_is_arrD = dg_Set_is_arrD
  and smc_Set_is_arrE = dg_Set_is_arrE
  and smc_Set_ArrVal_vdomain[smc_Set_cs_simps] = dg_Set_ArrVal_vdomain
  and smc_Set_ArrVal_app_vrange[smc_Set_cs_intros] = dg_Set_ArrVal_app_vrange

lemmas [smc_cs_simps] = smc_Set_is_arrD(2,3)

lemmas_with (in 𝒵) [folded smc_dg_smc_Set, unfolded slicing_simps]: 
  smc_Set_Hom_vifunion_in_Vset = dg_Set_Hom_vifunion_in_Vset
  and smc_Set_incl_Set_is_arr = dg_Set_incl_Set_is_arr

lemmas [smc_Set_cs_intros] = 
  smc_Set_is_arrI

lemma (in 𝒵) smc_Set_incl_Set_is_arr'[smc_cs_intros, smc_Set_cs_intros]:
  assumes "A ∈∘ smc_Set α⦇Obj⦈" 
    and "B ∈∘ smc_Set α⦇Obj⦈" 
    and "A ⊆∘ B"
    and "A' = A"
    and "B' = B"
    and "ℭ' = smc_Set α"
  shows "incl_Set A B : A' ↦⇘ℭ'⇙ B'"
  using assms(1-3) unfolding assms(4-6) by (rule smc_Set_incl_Set_is_arr)

lemmas [smc_Set_cs_intros] = 𝒵.smc_Set_incl_Set_is_arr'


subsubsection‹Composable arrows›

lemma smc_Set_composable_arrs_dg_Set: 
  "composable_arrs (dg_Set α) = composable_arrs (smc_Set α)"
  unfolding composable_arrs_def smc_dg_smc_Set[symmetric] slicing_simps by simp

lemma smc_Set_Comp: 
  "smc_Set α⦇Comp⦈ =
    VLambda (composable_arrs (smc_Set α)) (λST. ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)"
  unfolding smc_Set_components smc_Set_composable_arrs_dg_Set ..


subsubsection‹Composition›

lemma smc_Set_Comp_app[smc_Set_cs_simps]:
  assumes "S : b ↦⇘smc_Set α⇙ c" and "T : a ↦⇘smc_Set α⇙ b"
  shows "S ∘A⇘smc_Set α⇙ T = S ∘Set T"
proof-
  from assms have "[S, T]∘ ∈∘ composable_arrs (smc_Set α)" 
    by (auto simp: smc_cs_intros)
  then show "S ∘A⇘smc_Set α⇙ T = S ∘Set T"
    unfolding smc_Set_Comp by (simp add: nat_omega_simps)
qed 

lemma smc_Set_Comp_vdomain: "𝒟∘ (smc_Set α⦇Comp⦈) = composable_arrs (smc_Set α)" 
  unfolding smc_Set_Comp by simp

lemma (in 𝒵) smc_Set_Comp_vrange: 
  "ℛ∘ (smc_Set α⦇Comp⦈) ⊆∘ set {T. arr_Set α T}"
proof(rule vsubsetI)
  interpret digraph α ‹smc_dg (smc_Set α)›
    unfolding smc_dg_smc_Set by (simp add: digraph_dg_Set)
  fix R assume "R ∈∘ ℛ∘ (smc_Set α⦇Comp⦈)"
  then obtain ST 
    where R_def: "R = smc_Set α⦇Comp⦈⦇ST⦈"
      and "ST ∈∘ 𝒟∘ (smc_Set α⦇Comp⦈)"
    unfolding smc_Set_components by (blast dest: rel_VLambda.vrange_atD) 
  then obtain S T a b c 
    where "ST = [S, T]∘" 
      and S: "S : b ↦⇘smc_Set α⇙ c" 
      and T: "T : a ↦⇘smc_Set α⇙ b"
    by (auto simp: smc_Set_Comp_vdomain)
  with R_def have R_def': "R = S ∘A⇘smc_Set α⇙ T" by simp
  interpret S: arr_Set α S + T: arr_Set α T 
    rewrites [simp]: "S⦇ArrDom⦈ = b" 
      and [simp]: "S⦇ArrCod⦈ = c"
      and [simp]: "T⦇ArrDom⦈ = a"
      and [simp]: "T⦇ArrCod⦈ = b"
    using S T by (auto elim!: smc_Set_is_arrD)
  have "ℛ∘ (T⦇ArrVal⦈) ⊆∘ 𝒟∘ (S⦇ArrVal⦈)"
  proof(intro vsubsetI)
    fix y assume prems: "y ∈∘ ℛ∘ (T⦇ArrVal⦈)"
    with T.ArrVal.vrange_atD obtain x 
      where y_def: "y = T⦇ArrVal⦈⦇x⦈" and x: "x ∈∘ 𝒟∘ (T⦇ArrVal⦈)"
      by metis
    from prems x T.arr_Set_ArrVal_vrange show "y ∈∘ 𝒟∘ (S⦇ArrVal⦈)"
      unfolding y_def by (auto simp: smc_Set_cs_simps)
  qed
  with S.arr_Set_axioms T.arr_Set_axioms have "arr_Set α (S ∘Set T)"
    by (simp add: arr_Set_comp_Set)
  from this show "R ∈∘ set {T. arr_Set α T}" 
    unfolding R_def' smc_Set_Comp_app[OF S T] by simp
qed

lemma smc_Set_composable_vrange_vdomain[smc_Set_cs_intros]:
  assumes "g : b ↦⇘smc_Set α⇙ c" and "f : a ↦⇘smc_Set α⇙ b"
  shows "ℛ∘ (f⦇ArrVal⦈) ⊆∘ 𝒟∘ (g⦇ArrVal⦈)"
proof(intro vsubsetI)
  from assms have g: "arr_Set α g" and f: "arr_Set α f" 
    by (auto simp: smc_Set_is_arrD)
  fix y assume "y ∈∘ ℛ∘ (f⦇ArrVal⦈)"
  with assms f have "y ∈∘ b" by (force simp: smc_Set_is_arrD(3))
  with assms g show "y ∈∘ 𝒟∘ (g⦇ArrVal⦈)" 
    by (simp add: smc_Set_is_arrD(2) arr_SetD(5))
qed

lemma smc_Set_Comp_ArrVal[smc_cs_simps]:
  assumes "S : y ↦⇘smc_Set α⇙ z" and "T : x ↦⇘smc_Set α⇙ y" and "a ∈∘ x"
  shows "(S ∘A⇘smc_Set α⇙ T)⦇ArrVal⦈⦇a⦈ = S⦇ArrVal⦈⦇T⦇ArrVal⦈⦇a⦈⦈"
proof-
  interpret S: arr_Set α S + T: arr_Set α T
    using assms by (auto simp: smc_Set_is_arrD)
  have Ta: "T⦇ArrVal⦈⦇a⦈ ∈∘ y"
  proof-
    from assms have "a ∈∘ T⦇ArrDom⦈" by (auto simp: smc_Set_is_arrD)
    with assms T.arr_Set_ArrVal_vrange show ?thesis
      by 
        (
          simp add: 
            T.ArrVal.vsv_vimageI2 vsubset_iff smc_Set_is_arrD smc_Set_cs_simps
        )
  qed
  from Ta assms S.arr_Set_axioms T.arr_Set_axioms show ?thesis
    by ((cs_concl_step smc_Set_cs_simps)+, intro arr_Set_comp_Set_ArrVal_app[of α])
      (simp_all add: smc_Set_is_arrD smc_Set_cs_simps)
qed


subsubsection‹‹Set› is a semicategory›

lemma (in 𝒵) semicategory_smc_Set: "semicategory α (smc_Set α)"
proof(rule semicategoryI, unfold smc_dg_smc_Set)

  interpret wide_subdigraph α ‹dg_Set α› ‹dg_Par α› 
    by (rule wide_subdigraph_dg_Set_dg_Par)
  interpret smc_Par: semicategory α ‹smc_Par α› by (rule semicategory_smc_Par)

  show "vfsequence (smc_Set α)" unfolding smc_Set_def by simp
  show "vcard (smc_Set α) = 5ℕ"
    unfolding smc_Set_def by (simp add: nat_omega_simps)

  show "(gf ∈∘ 𝒟∘ (smc_Set α⦇Comp⦈)) ⟷ 
    (∃g f b c a. gf = [g, f]∘ ∧ g : b ↦⇘smc_Set α⇙ c ∧ f : a ↦⇘smc_Set α⇙ b)"
    for gf
    unfolding smc_Set_Comp_vdomain by (auto intro: composable_arrsI)

  show [intro]: "g ∘A⇘smc_Set α⇙ f : a ↦⇘smc_Set α⇙ c"
    if "g : b ↦⇘smc_Set α⇙ c" "f : a ↦⇘smc_Set α⇙ b" for g b c f a
  proof-
    from that have g: "arr_Set α g" and f: "arr_Set α f" 
      by (auto simp: smc_Set_is_arrD)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_Set_cs_simps 
            cs_intro: smc_Set_cs_intros
        )
  qed
    
  show "h ∘A⇘smc_Set α⇙ g ∘A⇘smc_Set α⇙ f = h ∘A⇘smc_Set α⇙ (g ∘A⇘smc_Set α⇙ f)"
    if "h : c ↦⇘smc_Set α⇙ d" 
      and "g : b ↦⇘smc_Set α⇙ c"
      and "f : a ↦⇘smc_Set α⇙ b"
    for h c d g b f a
  proof-
    from that have "arr_Set α h" "arr_Set α g" "arr_Set α f" 
      by (auto simp: smc_Set_is_arrD)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_Set_cs_simps 
            cs_intro: smc_Set_cs_intros
        )      
  qed

qed (auto simp: digraph_dg_Set smc_Set_components)


subsubsection‹‹Set› is a wide subsemicategory of ‹Par››

lemma (in 𝒵) wide_subsemicategory_smc_Set_smc_Par: 
  "smc_Set α ⊆SMC.wide⇘α⇙ smc_Par α"
proof-
  interpret Par: semicategory α ‹smc_Par α› by (rule semicategory_smc_Par)
  interpret Set: semicategory α ‹smc_Set α› by (rule semicategory_smc_Set)
  show ?thesis
  proof
    (
      intro wide_subsemicategoryI subsemicategoryI, 
      unfold smc_dg_smc_Par smc_dg_smc_Set
    )
    from wide_subdigraph_dg_Set_dg_Par show wsd:  
      "dg_Set α ⊆DG⇘α⇙ dg_Par α" 
      "dg_Set α ⊆DG.wide⇘α⇙ dg_Par α"
      by auto
    interpret wide_subdigraph α ‹dg_Set α› ‹dg_Par α› by (rule wsd(2))
    show "g ∘A⇘smc_Set α⇙ f = g ∘A⇘smc_Par α⇙ f"
      if "g : b ↦⇘smc_Set α⇙ c" and "f : a ↦⇘smc_Set α⇙ b" for g b c f a
    proof-
      from that have "g : b ↦⇘dg_Set α⇙ c" and "f : a ↦⇘dg_Set α⇙ b" 
        by 
          (
            cs_concl cs_shallow 
              cs_simp: smc_dg_smc_Set[symmetric] cs_intro: slicing_intros
          )+
      then have "g : b ↦⇘dg_Par α⇙ c" and "f : a ↦⇘dg_Par α⇙ b" 
        by (cs_concl cs_shallow cs_intro: dg_sub_fw_cs_intros)+
      then have "g : b ↦⇘smc_Par α⇙ c" and "f : a ↦⇘smc_Par α⇙ b" 
        unfolding smc_dg_smc_Par[symmetric] slicing_simps by simp_all
      from that this show "g ∘A⇘smc_Set α⇙ f = g ∘A⇘smc_Par α⇙ f"
        by (cs_concl cs_shallow cs_simp: smc_Set_cs_simps smc_Par_cs_simps)
    qed
  qed (auto simp: smc_cs_intros)
qed



subsection‹Monic arrow and epic arrow›

lemma smc_Set_is_monic_arrI:
  ―‹See Chapter I-5 in \cite{mac_lane_categories_2010}).›
  assumes "T : A ↦⇘smc_Set α⇙ B" and "v11 (T⦇ArrVal⦈)" and "𝒟∘ (T⦇ArrVal⦈) = A"
  shows "T : A ↦mon⇘smc_Set α⇙ B"
proof(rule is_monic_arrI)

  interpret T: arr_Set α T by (intro smc_Set_is_arrD[OF assms(1)])+
  interpret wide_subsemicategory α ‹smc_Set α› ‹smc_Par α›
    by (rule T.wide_subsemicategory_smc_Set_smc_Par)
  interpret v11 ‹T⦇ArrVal⦈› by (rule assms(2))

  show T: "T : A ↦⇘smc_Set α⇙ B" by (rule assms(1))
  fix S R A'
  assume S: "S : A' ↦⇘smc_Set α⇙ A" 
    and R: "R : A' ↦⇘smc_Set α⇙ A" 
    and TS_TR: "T ∘A⇘smc_Set α⇙ S = T ∘A⇘smc_Set α⇙ R"
  from assms(3) T have "T : A ↦mon⇘smc_Par α⇙ B" 
    by (intro smc_Par_is_monic_arrI) 
      (auto simp: v11_axioms dest: subsmc_is_arrD)
  moreover from S subsemicategory_axioms have "S : A' ↦⇘smc_Par α⇙ A" 
    by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)
  moreover from R subsemicategory_axioms have "R : A' ↦⇘smc_Par α⇙ A" 
    by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)
  moreover from T S R TS_TR subsemicategory_axioms have 
    "T ∘A⇘smc_Par α⇙ S = T ∘A⇘smc_Par α⇙ R" 
    by (auto simp: smc_sub_bw_cs_simps)
  ultimately show "S = R" by (rule is_monic_arrD(2))

qed

lemma smc_Set_is_monic_arrD:
  assumes "T : A ↦mon⇘smc_Set α⇙ B"
  shows "T : A ↦⇘smc_Set α⇙ B" and "v11 (T⦇ArrVal⦈)" and "𝒟∘ (T⦇ArrVal⦈) = A"
proof-

  from assms show T: "T : A ↦⇘smc_Set α⇙ B" by auto
  interpret T: arr_Set α T 
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    by (intro smc_Set_is_arrD[OF T])+

  interpret wide_subdigraph α ‹dg_Set α› ‹dg_Par α› 
    by (rule T.wide_subdigraph_dg_Set_dg_Par)
  interpret Par: semicategory α ‹smc_Par α› by (rule T.semicategory_smc_Par)
  
  show "v11 (T⦇ArrVal⦈)"
  proof(rule v11I)
  
    show "vsv ((T⦇ArrVal⦈)¯∘)"
    proof(rule vsvI)

      fix a b c assume "⟨a, b⟩ ∈∘ (T⦇ArrVal⦈)¯∘" and "⟨a, c⟩ ∈∘ (T⦇ArrVal⦈)¯∘"

      then have bar: "⟨b, a⟩ ∈∘ T⦇ArrVal⦈" and car: "⟨c, a⟩ ∈∘ T⦇ArrVal⦈"
        by auto
      with T.arr_Set_ArrVal_vdomain have [intro]: "b ∈∘ A" "c ∈∘ A" by blast+

      define R where "R = [set {⟨0, b⟩}, set {0}, A]∘"
      define S where "S = [set {⟨0, c⟩}, set {0}, A]∘"

      have R: "R : set {0} ↦⇘smc_Set α⇙ A"
      proof(rule smc_Set_is_arrI)
        show "arr_Set α R"
          unfolding R_def
          by (rule T.arr_Set_vfsequenceI) (auto simp: T.arr_Rel_ArrDom_in_Vset)
      qed (simp_all add: R_def arr_Rel_components)
      interpret R: arr_Set α R 
        rewrites [simp]: "R⦇ArrDom⦈ = set {0}" and [simp]: "R⦇ArrCod⦈ = A"
        by (intro smc_Set_is_arrD[OF R])+

      have S: "S : set {0} ↦⇘smc_Set α⇙ A"
      proof(rule smc_Set_is_arrI)
        show "arr_Set α S"
          unfolding S_def
          by (rule T.arr_Set_vfsequenceI) (auto simp: T.arr_Rel_ArrDom_in_Vset)
      qed (simp_all add: S_def arr_Rel_components)
      interpret S: arr_Set α S 
        rewrites [simp]: "S⦇ArrDom⦈ = set {0}" and [simp]: "S⦇ArrCod⦈ = A"
        by (intro smc_Set_is_arrD[OF S])+

      have "T ∘A⇘smc_Set α⇙ R = [set {⟨0, a⟩}, set {0}, B]∘"        
        unfolding smc_Set_Comp_app[OF T R]
      proof
        (
          rule arr_Set_eqI[of α], 
          unfold comp_Rel_components arr_Rel_components
        )
        from R T show "arr_Set α (T ∘Set R)"
          by (intro arr_Set_comp_Set) 
            (auto elim!: smc_Set_is_arrE simp: smc_Set_cs_simps)
        show "arr_Set α [set {⟨0, a⟩}, set {0}, B]∘"
        proof(rule T.arr_Set_vfsequenceI)
          from T.arr_Rel_ArrVal_vrange bar show "ℛ∘ (set {⟨0, a⟩}) ⊆∘ B" by auto
        qed (auto simp: T.arr_Rel_ArrCod_in_Vset T.Axiom_of_Powers)
        show "T⦇ArrVal⦈ ∘∘ R⦇ArrVal⦈ = set {⟨0, a⟩}"
          unfolding R_def arr_Rel_components
        proof(rule vsv_eqI, unfold vdomain_vsingleton)
          from bar show "𝒟∘ (T⦇ArrVal⦈ ∘∘ set {⟨0, b⟩}) = set {0}" by auto
          with bar show "a' ∈∘ 𝒟∘ (T⦇ArrVal⦈ ∘∘ set {⟨0, b⟩}) ⟹ 
            (T⦇ArrVal⦈ ∘∘ set {⟨0, b⟩})⦇a'⦈ = set {⟨0, a⟩}⦇a'⦈"
            for a'
            by auto
        qed (auto intro: vsv_vcomp)
      qed (simp_all add: R_def arr_Rel_components)
      moreover have "T ∘A⇘smc_Set α⇙ S = [set {⟨0, a⟩}, set {0}, B]∘" 
        unfolding smc_Set_Comp_app[OF T S]
      proof
        (
          rule arr_Set_eqI[of α],
          unfold comp_Rel_components arr_Rel_components
        )
        from T S show "arr_Set α (T ∘Set S)"  
          by (intro arr_Set_comp_Set)
            (
              auto simp: 
                T.arr_Set_axioms 
                smc_Set_is_arrD 
                S.arr_Set_ArrVal_vrange 
                smc_Set_cs_simps
            )
        show "arr_Set α [set {⟨0, a⟩}, set {0}, B]∘"
        proof(rule T.arr_Set_vfsequenceI)
          from T.arr_Rel_ArrVal_vrange bar show "ℛ∘ (set {⟨0, a⟩}) ⊆∘ B" by auto
        qed (auto simp: T.arr_Rel_ArrCod_in_Vset T.Axiom_of_Powers)
        show "T⦇ArrVal⦈ ∘∘ S⦇ArrVal⦈ = set {⟨0, a⟩}"
          unfolding S_def arr_Rel_components
        proof(rule vsv_eqI, unfold vdomain_vsingleton)
          from car show "𝒟∘ (T⦇ArrVal⦈ ∘∘ set {⟨0, c⟩}) = set {0}" by auto
          with car show "a' ∈∘ 𝒟∘ (T⦇ArrVal⦈ ∘∘ set {⟨0, c⟩}) ⟹ 
            (T⦇ArrVal⦈ ∘∘ set {⟨0, c⟩})⦇a'⦈ = set {⟨0, a⟩}⦇a'⦈"
            for a'
            by auto
        qed (auto intro: vsv_vcomp)
      qed (simp_all add: S_def arr_Rel_components)
      ultimately have "T ∘A⇘smc_Set α⇙ R = T ∘A⇘smc_Set α⇙ S" by simp
      from R S assms this have "R = S" by clarsimp
      then have "R⦇ArrVal⦈ = S⦇ArrVal⦈" by simp
      then show "b = c" unfolding R_def S_def arr_Rel_components by simp
    qed clarsimp

  qed auto

  show "𝒟∘ (T⦇ArrVal⦈) = A" by (simp add: smc_Set_cs_simps)

qed

lemma smc_Set_is_monic_arr: 
  "T : A ↦mon⇘smc_Set α⇙ B ⟷  
    T : A ↦⇘smc_Set α⇙ B ∧ v11 (T⦇ArrVal⦈) ∧ 𝒟∘ (T⦇ArrVal⦈) = A"
  by (rule iffI) (auto simp: smc_Set_is_monic_arrD smc_Set_is_monic_arrI)


text‹
An epic arrow in ‹Set› is a total surjective function (see Chapter I-5 
in cite‹"mac_lane_categories_2010"›).
›

lemma smc_Set_is_epic_arrI:
  assumes "T : A ↦⇘smc_Set α⇙ B" and "ℛ∘ (T⦇ArrVal⦈) = B"
  shows "T : A ↦epi⇘smc_Set α⇙ B"
proof-

  interpret T: arr_Set α T 
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    by (intro smc_Set_is_arrD[OF assms(1)])+

  interpret wide_subsemicategory α ‹smc_Set α› ‹smc_Par α›
    by (rule T.wide_subsemicategory_smc_Set_smc_Par)
  have epi_T: "T : A ↦epi⇘smc_Par α⇙ B"
    using assms by (meson smc_Par_is_epic_arr subsmc_is_arrD)

  show ?thesis
  proof(rule sdg.is_epic_arrI)
    show T: "T : A ↦⇘smc_Set α⇙ B" by (rule assms(1))
    fix f g a
    assume prems: 
      "f : B ↦⇘smc_Set α⇙ a" 
      "g : B ↦⇘smc_Set α⇙ a"
      "f ∘A⇘smc_Set α⇙ T = g ∘A⇘smc_Set α⇙ T" 
    from prems(1) subsemicategory_axioms have "f : B ↦⇘smc_Par α⇙ a" 
      by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)
    moreover from prems(2) subsemicategory_axioms have "g : B ↦⇘smc_Par α⇙ a" 
      by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)
    moreover from prems T subsemicategory_axioms have 
      "f ∘A⇘smc_Par α⇙ T = g ∘A⇘smc_Par α⇙ T"
      by (auto simp: smc_sub_bw_cs_simps)
    ultimately show "f = g"
      by (rule dg.is_epic_arrD(2)[OF epi_T])
  qed

qed

lemma smc_Set_is_epic_arrD:
  assumes "T : A ↦epi⇘smc_Set α⇙ B"
  shows "T : A ↦⇘smc_Set α⇙ B" and "ℛ∘ (T⦇ArrVal⦈) = B"
proof-

  from assms show T: "T : A ↦⇘smc_Set α⇙ B" by auto
  interpret T: arr_Set α T
    rewrites "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = B"
    by (intro smc_Set_is_arrD[OF T])+

  interpret semicategory α ‹smc_Set α› by (rule T.semicategory_smc_Set)

  show "ℛ∘ (T⦇ArrVal⦈) = B"
  proof(intro vsubset_antisym vsubsetI)
    fix b assume [intro]: "b ∈∘ B" 
    show "b ∈∘ ℛ∘ (T⦇ArrVal⦈)"
    proof(rule ccontr)
      assume b: "b ∉∘ ℛ∘ (T⦇ArrVal⦈)"
      define R 
        where "R = [vinsert ⟨b, 0⟩ ((B -∘ set {b}) ×∘ set {1}), B, set {0, 1}]∘"
      define S where "S = [B ×∘ set {1}, B, set {0, 1}]∘"
      have R: "R : B ↦⇘smc_Set α⇙ set {0, 1}" 
        unfolding R_def
      proof
        (
          intro smc_Set_is_arrI T.arr_Set_vfsequenceI, 
          unfold arr_Rel_components
        )
        from T.Axiom_of_Infinity vone_in_omega show "set {0, 1} ∈∘ Vset α" 
          by blast
      qed (auto simp: T.arr_Rel_ArrCod_in_Vset)
      have S: "S : B ↦⇘smc_Set α⇙ set {0, 1}"
        unfolding S_def
      proof
        (
          intro smc_Set_is_arrI T.arr_Set_vfsequenceI,
          unfold arr_Rel_components
        )
        from T.Axiom_of_Infinity vone_in_omega show "set {0, 1} ∈∘ Vset α" 
          by blast
      qed (auto simp: T.arr_Rel_ArrCod_in_Vset)
      from b have "R⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈ = S⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈" 
        unfolding S_def R_def arr_Rel_components 
        by (auto intro!: vsubset_antisym vsubsetI)
      then have "R ∘A⇘smc_Set α⇙ T = S ∘A⇘smc_Set α⇙ T"
        unfolding smc_Set_Comp_app[OF R T] smc_Set_Comp_app[OF S T]
        by (simp add: R_def S_def arr_Rel_components comp_Rel_def)
      from R S this have "R = S" by (rule is_epic_arrD(2)[OF assms])
      with zero_neq_one show False unfolding R_def S_def by blast
    qed
  qed (use T.arr_Set_ArrVal_vrange in auto)

qed

lemma smc_Set_is_epic_arr: 
  "T : A ↦epi⇘smc_Set α⇙ B ⟷ T : A ↦⇘smc_Set α⇙ B ∧ ℛ∘ (T⦇ArrVal⦈) = B" 
  by (rule iffI) (simp_all add: smc_Set_is_epic_arrD smc_Set_is_epic_arrI)



subsection‹Terminal object, initial object and null object›


text‹
An object in ‹Set› is terminal if and only if it is a singleton 
set (see Chapter I-5 in cite‹"mac_lane_categories_2010"›).
›

lemma (in 𝒵) smc_Set_obj_terminal: 
  "obj_terminal (smc_Set α) A ⟷ (∃B∈∘Vset α. A = set {B})"
proof-

  interpret semicategory α ‹smc_Set α› by (rule semicategory_smc_Set)
  
  have "(∀A∈∘Vset α. ∃!T. T : A ↦⇘smc_Set α⇙ B) ⟷ (∃C∈∘Vset α. B = set {C})" 
    for B
  proof(intro iffI ballI)

    assume prems[rule_format]: "∀A∈∘Vset α. ∃!T. T : A ↦⇘smc_Set α⇙ B"

    then obtain T where T0B: "T : 0 ↦⇘smc_Set α⇙ B" by (meson vempty_is_zet)
    then have B[simp]: "B ∈∘ Vset α" by (fastforce simp: smc_Set_components(1))

    show "∃C∈∘Vset α. B = set {C}"
    proof(rule ccontr, cases ‹B = 0›)
      case True
      from prems have "∃!T. T : A ↦⇘smc_Set α⇙ 0" if "A ∈∘ Vset α" for A
        using that unfolding True by simp
      then obtain T where T: "T : set {0} ↦⇘smc_Set α⇙ 0" 
        by (metis Axiom_of_Pairing insert_absorb2 vempty_is_zet)
      interpret T: arr_Set α T
        rewrites "T⦇ArrDom⦈ = set {0}" and "T⦇ArrCod⦈ = 0"
        by (intro smc_Set_is_arrD[OF T])+
      from 
        T.vdomain_vrange_is_vempty
        T.ArrVal.vdomain_vrange_is_vempty 
        T.arr_Set_ArrVal_vrange
      show False  
        by (auto simp: smc_Set_cs_simps)
    next
      case False 
      assume "¬(∃C∈∘Vset α. B = set {C})"
      with B have "∄C. B = set {C}" by blast
      with False obtain a b where ab: "a ≠ b" "a ∈∘ B" "b ∈∘ B"
        by (metis V_equalityI vemptyE vintersection_vsingleton vsingletonD)
      have "[set {⟨0, a⟩}, set {0}, B]∘ : set {0} ↦⇘smc_Set α⇙ B"
        by (intro smc_Set_is_arrI arr_SetI, unfold arr_Rel_components)
          (auto simp: ab(2) nat_omega_simps)
      moreover from ab have 
        "[set {⟨0, b⟩}, set {0}, B]∘ : set {0} ↦⇘smc_Set α⇙ B"
        by (intro smc_Set_is_arrI arr_SetI, unfold arr_Rel_components)
          (auto simp: ab(2) nat_omega_simps)
      moreover with ab have 
        "[set {⟨0, a⟩}, set {0}, B]∘ ≠ [set {⟨0, b⟩}, set {0}, B]∘"
        by simp
      ultimately show False
        by (metis prems smc_is_arrE smc_Set_components(1))
    qed

  next
    
    fix A assume prems: "∃b∈∘Vset α. B = set {b}" "A ∈∘ Vset α"
    then obtain b where B_def: "B = set {b}" and b: "b ∈∘ Vset α" by blast

    have "vconst_on A b = A ×∘ set {b}" by (simp add: vconst_on_eq_vtimes)

    show "∃!T. T : A ↦⇘smc_Set α⇙ B"
      unfolding B_def
    proof(rule ex1I[of _ ‹[A ×∘ set {b}, A, set {b}]∘›])
      
      show "[A ×∘ set {b}, A, set {b}]∘ : A ↦⇘smc_Set α⇙ set {b}"
        using b 
        by 
          ( 
            intro smc_Set_is_arrI arr_Set_vfsequenceI, 
            unfold arr_Rel_components
          )
          (auto simp: prems(2) vconst_on_eq_vtimes[symmetric])
      
      fix T assume prems: "T : A ↦⇘smc_Set α⇙ set {b}"

      interpret T: arr_Set α T
        rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = set {b}"
        by (intro smc_Set_is_arrD[OF prems])+

      have [simp]: "T⦇ArrVal⦈ = A ×∘ set {b}"
      proof(intro vsubset_antisym vsubsetI)
        fix x assume prems: "x ∈∘ T⦇ArrVal⦈"
        with T.vbrelation_axioms app_vdomainI obtain a b' 
          where "x = ⟨a, b'⟩" and "a ∈∘ A"
          by (metis T.ArrVal.vbrelation_vinE T.arr_Set_ArrVal_vdomain)
        with prems T.arr_Set_ArrVal_vrange show "x ∈∘ A ×∘ set {b}" by auto
      next
        fix x assume "x ∈∘ A ×∘ set {b}" 
        then obtain a where x_def: "x = ⟨a, b⟩" and "a ∈∘ A" by clarsimp
        have "𝒟∘ (T⦇ArrVal⦈) = A" by (simp add: smc_Set_cs_simps)
        moreover with 
          T.arr_Set_ArrVal_vrange T.ArrVal.vdomain_vrange_is_vempty ‹a ∈∘ A›   
        have "ℛ∘ (T⦇ArrVal⦈) = set {b}"
          by auto
        ultimately show "x ∈∘ T⦇ArrVal⦈"
          using ‹a ∈∘ A›
          unfolding x_def 
          by 
            (
              metis 
                T.ArrVal.vsv_ex1_app1 
                T.ArrVal.vsv_vimageI1 
                vimage_vdomain 
                vsingletonD
            )
      qed
      
      show "T = [A ×∘ set {b}, A, set {b}]∘"
      proof(rule arr_Set_eqI[of α], unfold arr_Rel_components)
        show "arr_Set α [A ×∘ set {b}, A, set {b}]∘"
          using T.arr_Rel_def T.arr_Set_axioms by auto
      qed (auto simp: T.arr_Set_axioms)

    qed
  qed

  then show ?thesis
    apply(intro iffI obj_terminalI)
    subgoal by (metis smc_is_arrD(2) obj_terminalE)
    subgoal by blast
    subgoal by (metis smc_Set_components(1))
    done

qed


text‹
An object in ‹Set› is initial if and only if it is the empty 
set (see Chapter I-5 in cite‹"mac_lane_categories_2010"›).
›

lemma (in 𝒵) smc_Set_obj_initial: "obj_initial (smc_Set α) A ⟷ A = 0"
proof-

  interpret semicategory α ‹smc_Set α› by (rule semicategory_smc_Set)

  have "(∀B∈∘Vset α. ∃!T. T : A ↦⇘smc_Set α⇙ B) ⟷ A = 0" for A
  proof(intro iffI ballI)

    assume prems[rule_format]: "∀B∈∘Vset α. ∃!T. T : A ↦⇘smc_Set α⇙ B" 

    then obtain T where T0B: "T : A ↦⇘smc_Set α⇙ 0" by (meson vempty_is_zet)
    then have A[simp]: "A ∈∘ Vset α" by (fastforce simp: smc_Set_components(1))

    show "A = 0"
    proof(rule ccontr)
      assume "A ≠ 0"
      then obtain a where a: "a ∈∘ A" by (auto dest: trad_foundation)
      from Axiom_of_Powers a have A0: 
        "[A ×∘ set {0}, A, set {0}]∘ : A ↦⇘smc_Set α⇙ set {0}"
        by 
          ( 
            intro smc_Set_is_arrI arr_Set_vfsequenceI, 
            unfold arr_Rel_components
          )
          auto
      have A1: "[A ×∘ set {1}, A, set {1}]∘ : A ↦⇘smc_Set α⇙ set {1}"
      proof
          ( 
            intro smc_Set_is_arrI arr_Set_vfsequenceI, 
            unfold arr_Rel_components
          )
        show "set {1} ∈∘ Vset α" by (blast intro: vone_in_omega Axiom_of_Infinity)
      qed auto
      have "[A ×∘ set {0}, A, set {0, 1}]∘ : A ↦⇘smc_Set α⇙ set {0, 1}"
      proof
        (
          intro smc_Set_is_arrI arr_Set_vfsequenceI, 
          unfold arr_Rel_components
        )
        show "set {0, 1} ∈∘ Vset α"
          by (intro Limit_vdoubleton_in_VsetI) (force simp: nat_omega_simps)+
      qed auto
      moreover have 
        "[A ×∘ set {1}, A, set {0, 1}]∘ : A ↦⇘smc_Set α⇙ set {0, 1}"
      proof
        (
          intro smc_Set_is_arrI arr_Set_vfsequenceI, 
          unfold arr_Rel_components
        )
        show "set {0, 1} ∈∘ Vset α"
          by (intro Limit_vdoubleton_in_VsetI) (force simp: nat_omega_simps)+
      qed auto
      moreover from ‹A ≠ 0› one_neq_zero have 
        "[A ×∘ set {0}, A, set {0, 1}]∘ ≠ [A ×∘ set {1}, A, set {0, 1}]∘" 
        by (blast intro!: vsubset_antisym)
      ultimately show False 
        by (metis prems smc_is_arrE smc_Set_components(1))
    qed
  next
    fix B assume prems: "A = 0" "B ∈∘ Vset α"
    show "∃!T. T : A ↦⇘smc_Set α⇙ B"
    proof(rule ex1I[of _ ‹[0, 0, B]∘›], unfold prems(1))
      show zzB: "[0, 0, B]∘ : 0 ↦⇘smc_Set α⇙ B"
        by 
          (
            intro smc_Set_is_arrI arr_Set_vfsequenceI, 
            unfold arr_Rel_components
          )
          (simp_all add: prems)
      fix T assume prems': "T : 0 ↦⇘smc_Set α⇙ B"
      interpret T: arr_Set α T
        rewrites [simp]: "T⦇ArrDom⦈ = 0" and [simp]: "T⦇ArrCod⦈ = B"
        by (intro smc_Set_is_arrD[OF prems'])+
      show "T = [0, 0, B]∘"  
      proof(rule arr_Set_eqI[of α], unfold arr_Rel_components)
        show "arr_Set α T" by (rule T.arr_Set_axioms)
        from zzB show "arr_Set α [0, 0, B]∘" by (meson smc_Set_is_arrE)
        from T.ArrVal.vdomain_vrange_is_vempty show "T⦇ArrVal⦈ = 0"
          by (auto intro: T.ArrVal.vsv_vrange_vempty simp: smc_Set_cs_simps)
      qed simp_all
    qed
  qed

  then show ?thesis 
    apply(intro iffI obj_initialI, elim obj_initialE)
    subgoal by (metis smc_Set_components(1))
    subgoal by (simp add: smc_Set_components(1))
    subgoal by (metis smc_Set_components(1))
    done

qed


text‹
There are no null objects in ‹Set› (this is a trivial corollary of the above).
›

lemma (in 𝒵) smc_Set_obj_null: "obj_null (smc_Set α) A ⟷ False"
  unfolding obj_null_def smc_Set_obj_terminal smc_Set_obj_initial by simp



subsection‹Zero arrow›


text‹
There are no zero arrows in ‹Set› (this result is a trivial 
corollary of the absence of null objects).
›

lemma (in 𝒵) smc_Set_is_zero_arr: "T : A ↦0⇘smc_Set α⇙ B ⟷ False"
  using smc_Set_obj_null unfolding is_zero_arr_def by auto

text‹\newpage›

end