Theory CZH_SMC_Par

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Par› as a semicategory›
theory CZH_SMC_Par
  imports 
    CZH_DG_Par
    CZH_SMC_Rel
    CZH_SMC_Subsemicategory
begin



subsection‹Background›


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

named_theorems smc_Par_cs_simps
named_theorems smc_Par_cs_intros

lemmas (in arr_Par) [smc_Par_cs_simps] = 
  dg_Rel_shared_cs_simps

lemmas (in arr_Par) [smc_cs_intros, smc_Par_cs_intros] = 
  arr_Par_axioms'

lemmas [smc_Par_cs_simps] = 
  dg_Rel_shared_cs_simps
  arr_Par.arr_Par_length
  arr_Par_comp_Par_id_Par_left
  arr_Par_comp_Par_id_Par_right

lemmas [smc_Par_cs_intros] = 
  dg_Rel_shared_cs_intros
  arr_Par_comp_Par



subsection‹‹Par› as a semicategory›


subsubsection‹Definition and elementary properties›

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


text‹Components.›

lemma smc_Par_components:
  shows "smc_Par α⦇Obj⦈ = Vset α"
    and "smc_Par α⦇Arr⦈ = set {T. arr_Par α T}"
    and "smc_Par α⦇Dom⦈ = (λT∈∘set {T. arr_Par α T}. T⦇ArrDom⦈)"
    and "smc_Par α⦇Cod⦈ = (λT∈∘set {T. arr_Par α T}. T⦇ArrCod⦈)"
    and "smc_Par α⦇Comp⦈ = (λST∈∘composable_arrs (dg_Par α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)"
  unfolding smc_Par_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smc_dg_smc_Par: "smc_dg (smc_Par α) = dg_Par α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟∘ (smc_dg (smc_Par α)) = 4ℕ" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ (dg_Par α) = 4ℕ"
    unfolding dg_Par_def by (simp add: nat_omega_simps)
  show "𝒟∘ (smc_dg (smc_Par α)) = 𝒟∘ (dg_Par α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ (smc_dg (smc_Par α)) ⟹ smc_dg (smc_Par α)⦇a⦈ = dg_Par α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        unfold smc_dg_def dg_field_simps smc_Par_def dg_Par_def
      )
      (auto simp: nat_omega_simps)
qed (auto simp: dg_Par_def smc_dg_def)

lemmas_with [folded smc_dg_smc_Par, unfolded slicing_simps]: 
  smc_Par_Obj_iff = dg_Par_Obj_iff
  and smc_Par_Arr_iff[smc_Par_cs_simps] = dg_Par_Arr_iff
  and smc_Par_Dom_vsv[smc_Par_cs_intros] = dg_Par_Dom_vsv
  and smc_Par_Dom_vdomain[smc_Par_cs_simps] = dg_Par_Dom_vdomain
  and smc_Par_Dom_vrange = dg_Par_Dom_vrange
  and smc_Par_Dom_app[smc_Par_cs_simps] = dg_Par_Dom_app
  and smc_Par_Cod_vsv[smc_Par_cs_intros] = dg_Par_Cod_vsv
  and smc_Par_Cod_vdomain[smc_Par_cs_simps] = dg_Par_Cod_vdomain
  and smc_Par_Cod_vrange = dg_Par_Cod_vrange
  and smc_Par_Cod_app[smc_Par_cs_simps] = dg_Par_Cod_app
  and smc_Par_is_arrI = dg_Par_is_arrI
  and smc_Par_is_arrD = dg_Par_is_arrD
  and smc_Par_is_arrE = dg_Par_is_arrE

lemmas [smc_cs_simps] = smc_Par_is_arrD(2,3)

lemmas [smc_Par_cs_intros] = smc_Par_is_arrI

lemmas_with (in 𝒵) [folded smc_dg_smc_Par, unfolded slicing_simps]: 
  smc_Par_Hom_vifunion_in_Vset = dg_Par_Hom_vifunion_in_Vset
  and smc_Par_incl_Par_is_arr = dg_Par_incl_Par_is_arr
  and smc_Par_incl_Par_is_arr'[smc_Par_cs_intros] = dg_Par_incl_Par_is_arr'

lemmas [smc_Par_cs_intros] = 𝒵.smc_Par_incl_Par_is_arr'


subsubsection‹Composable arrows›

lemma smc_Par_composable_arrs_dg_Par: 
  "composable_arrs (dg_Par α) = composable_arrs (smc_Par α)"
  unfolding composable_arrs_def smc_dg_smc_Par[symmetric] slicing_simps by simp

lemma smc_Par_Comp: 
  "smc_Par α⦇Comp⦈ = (λST∈∘composable_arrs (smc_Par α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)"
  unfolding smc_Par_components smc_Par_composable_arrs_dg_Par ..


subsubsection‹Composition›

lemma smc_Par_Comp_app[smc_Par_cs_simps]:
  assumes "S : B ↦⇘smc_Par α⇙ C" and "T : A ↦⇘smc_Par α⇙ B"
  shows "S ∘A⇘smc_Par α⇙ T = S ∘Rel T"
proof-
  from assms have "[S, T]∘ ∈∘ composable_arrs (smc_Par α)" 
    by (auto simp: smc_cs_intros)
  then show "S ∘A⇘smc_Par α⇙ T = S ∘Rel T"
    unfolding smc_Par_Comp by (simp add: nat_omega_simps)
qed 

lemma smc_Par_Comp_vdomain: "𝒟∘ (smc_Par α⦇Comp⦈) = composable_arrs (smc_Par α)" 
  unfolding smc_Par_Comp by simp

lemma (in 𝒵) smc_Par_Comp_vrange: "ℛ∘ (smc_Par α⦇Comp⦈) ⊆∘ set {T. arr_Par α T}"
proof(rule vsubsetI)
  interpret digraph α ‹smc_dg (smc_Par α)›
    unfolding smc_dg_smc_Par by (simp add: digraph_dg_Par)
  fix R assume "R ∈∘ ℛ∘ (smc_Par α⦇Comp⦈)"
  then obtain ST 
    where R_def: "R = smc_Par α⦇Comp⦈⦇ST⦈"
      and "ST ∈∘ 𝒟∘ (smc_Par α⦇Comp⦈)"
    unfolding smc_Par_components by (blast dest: rel_VLambda.vrange_atD)
  then obtain S T A B C 
    where "ST = [S, T]∘" 
      and S: "S : B ↦⇘smc_Par α⇙ C" 
      and T: "T : A ↦⇘smc_Par α⇙ B"
    by (auto simp: smc_Par_Comp_vdomain)
  with R_def have R_def': "R = S ∘A⇘smc_Par α⇙ T" by simp
  note S_D = dg_is_arrD(1)[unfolded slicing_simps, OF S]
    and T_D = dg_is_arrD(1)[unfolded slicing_simps, OF T]
  from S_D T_D have "arr_Par α S" "arr_Par α T" 
    by (simp_all add: smc_Par_components)
  from this show "R ∈∘ set {T. arr_Par α T}" 
    unfolding R_def' smc_Par_Comp_app[OF S T] by (auto simp: arr_Par_comp_Par)
qed


subsubsection‹‹Par› is a semicategory›

lemma (in 𝒵) semicategory_smc_Par: "semicategory α (smc_Par α)"
proof(intro semicategoryI, unfold smc_dg_smc_Par)
  show "vfsequence (smc_Par α)" unfolding smc_Par_def by simp
  show "vcard (smc_Par α) = 5ℕ"
    unfolding smc_Par_def by (simp add: nat_omega_simps)
  show "(GF ∈∘ 𝒟∘ (smc_Par α⦇Comp⦈)) ⟷
    (∃G F B C A. GF = [G, F]∘ ∧ G : B ↦⇘smc_Par α⇙ C ∧ F : A ↦⇘smc_Par α⇙ B)"
    for GF
    unfolding smc_Par_Comp_vdomain by (auto intro: composable_arrsI)
  show [intro]: "G ∘A⇘smc_Par α⇙ F : A ↦⇘smc_Par α⇙ C"
    if "G : B ↦⇘smc_Par α⇙ C" and "F : A ↦⇘smc_Par α⇙ B" for G B C F A
  proof-
    from that have "arr_Par α G" "arr_Par α F" by (auto elim: smc_Par_is_arrE)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_Par_cs_simps 
            cs_intro: smc_Par_cs_intros
        )
  qed 
  show "H ∘A⇘smc_Par α⇙ G ∘A⇘smc_Par α⇙ F = H ∘A⇘smc_Par α⇙ (G ∘A⇘smc_Par α⇙ F)"
    if "H : C ↦⇘smc_Par α⇙ D" 
      and "G : B ↦⇘smc_Par α⇙ C"
      and "F : A ↦⇘smc_Par α⇙ B"
    for H C D G B F A
  proof-
    from that have "arr_Par α H" "arr_Par α G" "arr_Par α F" 
      by (auto simp: smc_Par_is_arrD)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_Par_cs_simps 
            cs_intro: smc_Par_cs_intros
        )
  qed
qed (auto simp: digraph_dg_Par smc_Par_components)


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

lemma (in 𝒵) wide_subsemicategory_smc_Par_smc_Rel: 
  "smc_Par α ⊆SMC.wide⇘α⇙ smc_Rel α"
proof-
  interpret Rel: semicategory α ‹smc_Rel α› by (rule semicategory_smc_Rel)
  interpret Par: semicategory α ‹smc_Par α› by (rule semicategory_smc_Par)
  show ?thesis
  proof
    (
      intro wide_subsemicategoryI subsemicategoryI,
      unfold smc_dg_smc_Par smc_dg_smc_Rel
    )
    from wide_subdigraph_dg_Par_dg_Rel show wsd:
      "dg_Par α ⊆DG⇘α⇙ dg_Rel α" "dg_Par α ⊆DG.wide⇘α⇙ dg_Rel α"
      by auto
    interpret wide_subdigraph α ‹dg_Par α› ‹dg_Rel α› by (rule wsd(2))
    show "G ∘A⇘smc_Par α⇙ F = G ∘A⇘smc_Rel α⇙ F"
      if "G : B ↦⇘smc_Par α⇙ C" and "F : A ↦⇘smc_Par α⇙ B" for G B C F A
    proof-
      from that have "G : B ↦⇘dg_Par α⇙ C" and "F : A ↦⇘dg_Par α⇙ B" 
        by 
          (
            cs_concl cs_shallow 
              cs_simp: smc_dg_smc_Par[symmetric] cs_intro: slicing_intros
          )+
      then have "G : B ↦⇘dg_Rel α⇙ C" and "F : A ↦⇘dg_Rel α⇙ B" 
        by (cs_concl cs_shallow cs_intro: dg_sub_fw_cs_intros)+
      then have "G : B ↦⇘smc_Rel α⇙ C" and "F : A ↦⇘smc_Rel α⇙ B" 
        unfolding smc_dg_smc_Rel[symmetric] slicing_simps by simp_all
      from that this show "G ∘A⇘smc_Par α⇙ F = G ∘A⇘smc_Rel α⇙ F"
        by (cs_concl cs_shallow cs_simp: smc_Par_cs_simps smc_Rel_cs_simps)
    qed
  qed (auto simp: smc_cs_intros)
qed



subsection‹Monic arrow and epic arrow›

lemma smc_Par_is_monic_arrI[intro]:
  assumes "T : A ↦⇘smc_Par α⇙ B" and "v11 (T⦇ArrVal⦈)" and "𝒟∘ (T⦇ArrVal⦈) = A"
  shows "T : A ↦mon⇘smc_Par α⇙ B"
proof(intro is_monic_arrI)

  interpret T: arr_Par α T by (intro smc_Par_is_arrD(1)[OF assms(1)])
  interpret Par_Rel: wide_subsemicategory α ‹smc_Par α› ‹smc_Rel α›
    by (rule T.wide_subsemicategory_smc_Par_smc_Rel)
  interpret v11: v11 ‹T⦇ArrVal⦈› by (rule assms(2))

  show T: "T : A ↦⇘smc_Par α⇙ B" by (rule assms(1))
  fix S R A'
  assume S: "S : A' ↦⇘smc_Par α⇙ A" 
    and R: "R : A' ↦⇘smc_Par α⇙ A"
    and TS_TR: "T ∘A⇘smc_Par α⇙ S = T ∘A⇘smc_Par α⇙ R"
  from assms(3) T Par_Rel.subsemicategory_axioms have "T : A ↦mon⇘smc_Rel α⇙ B"
    by (intro smc_Rel_is_monic_arrI)
      (auto dest: v11.v11_vimage_vpsubset_neq elim!: smc_sub_fw_cs_intros)
  moreover from S Par_Rel.subsemicategory_axioms have "S : A' ↦⇘smc_Rel α⇙ A"
    by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)
  moreover from R Par_Rel.subsemicategory_axioms have "R : A' ↦⇘smc_Rel α⇙ A" 
    by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)
  moreover from T S R TS_TR Par_Rel.subsemicategory_axioms have 
    "T ∘A⇘smc_Rel α⇙ S = T ∘A⇘smc_Rel α⇙ R" 
    by (auto simp: smc_sub_bw_cs_simps)
  ultimately show "S = R" by (rule is_monic_arrD(2))
qed

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

  from assms show T: "T : A ↦⇘smc_Par α⇙ B" by auto
  interpret T: arr_Par α T 
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    using T by (auto dest: smc_Par_is_arrD)

  show "v11 (T⦇ArrVal⦈)"
  proof(intro v11I)

    show "vsv ((T⦇ArrVal⦈)¯∘)"
    proof(intro 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_Rel_ArrVal_vdomain have [intro]: "b ∈∘ A" "c ∈∘ A" by auto

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

      have R_components: 
        "R⦇ArrVal⦈ = set {⟨0, b⟩}" "R⦇ArrDom⦈ = set {0}" "R⦇ArrCod⦈ = A"
        unfolding R_def by (simp_all add: arr_Rel_components)

      have S_components: 
        "S⦇ArrVal⦈ = set {⟨0, c⟩}" "S⦇ArrDom⦈ = set {0}" "S⦇ArrCod⦈ = A"
        unfolding S_def by (simp_all add: arr_Rel_components)

      have R: "R : set {0} ↦⇘smc_Par α⇙ A"
      proof(rule smc_Par_is_arrI)
        show "arr_Par α R"
          unfolding R_def
          by (rule T.arr_Par_vfsequenceI) (auto simp: T.arr_Rel_ArrDom_in_Vset)
      qed (simp_all add: R_components)

      have S: "S : set {0} ↦⇘smc_Par α⇙ A"
      proof(rule smc_Par_is_arrI)
        show "arr_Par α S"
          unfolding S_def
          by (rule T.arr_Par_vfsequenceI) (auto simp: T.arr_Rel_ArrDom_in_Vset)
      qed (simp_all add: S_components)

      have "T ∘A⇘smc_Par α⇙ R = [set {⟨0, a⟩}, set {0}, B]∘"
        unfolding smc_Par_Comp_app[OF T R]
      proof
        (
          rule arr_Par_eqI[of α],
          unfold comp_Rel_components arr_Rel_components R_components
        )
        from R T show "arr_Par α (T ∘Rel R)"
          by (intro arr_Par_comp_Par) (auto elim!: smc_Par_is_arrE)
        show "arr_Par α [set {⟨0, a⟩}, set {0}, B]∘"
        proof(rule T.arr_Par_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⦈ ∘∘ set {⟨0, b⟩} = set {⟨0, a⟩}"
        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

      moreover have "T ∘A⇘smc_Par α⇙ S = [set {⟨0, a⟩}, set {0}, B]∘" 
        unfolding smc_Par_Comp_app[OF T S]
      proof
        (
          rule arr_Par_eqI[of α],
          unfold comp_Rel_components arr_Rel_components S_components
        )
        from T S show "arr_Par α (T ∘Rel S)"
          by (intro arr_Par_comp_Par) (auto elim!: smc_Par_is_arrE)
        show "arr_Par α [set {⟨0, a⟩}, set {0}, B]∘"
        proof(rule T.arr_Par_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⦈ ∘∘ set {⟨0, c⟩} = set {⟨0, a⟩}"
        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
      ultimately have "T ∘A⇘smc_Par α⇙ R = T ∘A⇘smc_Par α⇙ S" by simp
      from assms R S this have "R = S" by blast
      with R_components(1) S_components(1) show "b = c" by simp
    qed auto

  qed auto

  show "𝒟∘ (T⦇ArrVal⦈) = A"
  proof(intro vsubset_antisym vsubsetI)
    from T.arr_Rel_ArrVal_vdomain show "x ∈∘ 𝒟∘ (T⦇ArrVal⦈) ⟹ x ∈∘ A" for x
      by auto
    fix a assume [simp]: "a ∈∘ A" show "a ∈∘ 𝒟∘ (T⦇ArrVal⦈)"
    proof(rule ccontr)
      assume a: "a ∉∘ 𝒟∘ (T⦇ArrVal⦈)"
      define R where "R = [set {⟨0, a⟩}, set {0, 1}, A]∘"
      define S where "S = [set {⟨1, a⟩}, set {0, 1}, A]∘"
      have R: "R : set {0, 1} ↦⇘smc_Par α⇙ A"
      proof(rule smc_Par_is_arrI)
        show "arr_Par α R"
          unfolding R_def
        proof(rule T.arr_Par_vfsequenceI)
          from T.Axiom_of_Infinity vone_in_omega show "set {0, 1} ∈∘ Vset α" 
            by blast
        qed (auto simp: T.arr_Rel_ArrDom_in_Vset)
      qed (auto simp: R_def arr_Rel_components)
      have S: "S : set {0, 1} ↦⇘smc_Par α⇙ A"
      proof(rule smc_Par_is_arrI)
        show "arr_Par α S"
          unfolding S_def
        proof(rule T.arr_Par_vfsequenceI)
          from T.Axiom_of_Infinity vone_in_omega show "set {0, 1} ∈∘ Vset α" 
            by blast
        qed (auto simp: T.arr_Rel_ArrDom_in_Vset)
      qed (auto simp: S_def arr_Rel_components)
      with a have "T⦇ArrVal⦈ ∘∘ R⦇ArrVal⦈ = 0" 
        unfolding R_def arr_Rel_components
        by (intro vsubset_antisym vsubsetI) auto
      moreover with a have "T⦇ArrVal⦈ ∘∘ S⦇ArrVal⦈ = 0" 
        unfolding S_def arr_Rel_components
        by (intro vsubset_antisym vsubsetI) auto
      ultimately have "T ∘A⇘smc_Par α⇙ R = T ∘A⇘smc_Par α⇙ S" 
        using R T S
        by
          (
            intro arr_Par_eqI[of α ‹T ∘A⇘smc_Par α⇙ R› ‹T ∘A⇘smc_Par α⇙ S›]; 
            elim smc_Par_is_arrE
          )
          (
            auto simp:
              dg_Par_cs_intros
              smc_Par_Comp_app[OF T R] 
              smc_Par_Comp_app[OF T S] 
              comp_Rel_components
          )
      from R S this assms have "R = S" by blast
      then show False unfolding R_def S_def by simp
    qed 
  qed

qed 

lemma smc_Par_is_monic_arr: 
  "T : A ↦mon⇘smc_Par α⇙ B ⟷
    T : A ↦⇘smc_Par α⇙ B ∧ v11 (T⦇ArrVal⦈) ∧ 𝒟∘ (T⦇ArrVal⦈) = A"
  by (intro iffI) (auto simp: smc_Par_is_monic_arrD smc_Par_is_monic_arrI)

context
begin

private lemma smc_Par_is_epic_arr_vsubset:
  assumes "T : A ↦⇘smc_Par α⇙ B"
    and "ℛ∘ (T⦇ArrVal⦈) = B"
    and "R : B ↦⇘smc_Par α⇙ C" 
    and "S : B ↦⇘smc_Par α⇙ C" 
    and "R ∘A⇘smc_Par α⇙ T = S ∘A⇘smc_Par α⇙ T" 
  shows "R⦇ArrVal⦈ ⊆∘ S⦇ArrVal⦈"
proof
  interpret T: arr_Par α T
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    using assms smc_Par_is_arrD by auto
  interpret R: arr_Par α R 
    rewrites [simp]: "R⦇ArrDom⦈ = B" and [simp]: "R⦇ArrCod⦈ = C"
    using assms smc_Par_is_arrD by auto
  from assms(5) have "(R ∘A⇘smc_Par α⇙ T)⦇ArrVal⦈ = (S ∘A⇘smc_Par α⇙ T)⦇ArrVal⦈"
    by simp
  then have eq: "R⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈ = S⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈" 
    unfolding 
      smc_Par_Comp_app[OF assms(3,1)] 
      smc_Par_Comp_app[OF assms(4,1)]
      comp_Rel_components
    by simp
  fix bc assume prems: "bc ∈∘ R⦇ArrVal⦈"
  moreover with R.ArrVal.vbrelation obtain b c where bc_def: "bc = ⟨b, c⟩" by auto
  ultimately have [simp]: "b ∈∘ B" and "c ∈∘ C"
    using R.arr_Rel_ArrVal_vdomain R.arr_Rel_ArrVal_vrange by auto
  note [intro] = prems[unfolded bc_def]
  have "b ∈∘ ℛ∘ (T⦇ArrVal⦈)" by (simp add: assms(2))
  then obtain a where ab: "⟨a, b⟩ ∈∘ T⦇ArrVal⦈" by auto
  then have "⟨a, c⟩ ∈∘ S⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈" unfolding eq[symmetric] by auto
  then obtain b' where ab': "⟨b', c⟩ ∈∘ S⦇ArrVal⦈" and "⟨a, b'⟩ ∈∘ T⦇ArrVal⦈" 
    by clarsimp
  with ab ab' T.vsv T.ArrVal.vsv show "bc ∈∘ S⦇ArrVal⦈" unfolding bc_def by blast
qed

lemma smc_Par_is_epic_arrI:
  assumes "T : A ↦⇘smc_Par α⇙ B" and "ℛ∘ (T⦇ArrVal⦈) = B"
  shows "T : A ↦epi⇘smc_Par α⇙ B"
  unfolding is_epic_arr_def
proof
  (
    intro is_monic_arrI[
      of ‹op_smc (smc_Par α)›, unfolded smc_op_simps, OF assms(1)
      ]
  )

  interpret T: arr_Par α T
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    using assms smc_Par_is_arrD by auto

  interpret semicategory α ‹smc_Par α› by (rule T.semicategory_smc_Par)

  fix R S a 
  assume prems: 
    "R : B ↦⇘smc_Par α⇙ a" 
    "S : B ↦⇘smc_Par α⇙ a" 
    "T ∘A⇘op_smc (smc_Par α)⇙ R = T ∘A⇘op_smc (smc_Par α)⇙ S"

  from prems(3) have RT_ST: "R ∘A⇘smc_Par α⇙ T = S ∘A⇘smc_Par α⇙ T"
    unfolding 
      op_smc_Comp[OF prems(1) assms(1)]
      op_smc_Comp[OF prems(2) assms(1)]
    by simp
  from smc_Par_is_epic_arr_vsubset[OF assms(1,2) prems(1,2) this] 
  have RS: "R⦇ArrVal⦈ ⊆∘ S⦇ArrVal⦈".

  from smc_Par_is_epic_arr_vsubset[OF assms(1,2) prems(2,1) RT_ST[symmetric]]
  have SR: "S⦇ArrVal⦈ ⊆∘ R⦇ArrVal⦈".
  
  from prems show "R = S"    
    by (intro arr_Par_eqI[of α R S])
      (auto simp: RS SR vsubset_antisym elim!: smc_Par_is_arrE)

qed

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

  from assms show T: "T : A ↦⇘smc_Par α⇙ B" 
    unfolding is_epic_arr_def by (auto simp: op_smc_is_arr)

  interpret T: arr_Par α T
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    using T by (auto elim: smc_Par_is_arrE)

  interpret semicategory α ‹smc_Par α› by (rule T.semicategory_smc_Par)

  show "ℛ∘ (T⦇ArrVal⦈) = B"
  proof(intro vsubset_antisym vsubsetI)
    from T.arr_Rel_ArrVal_vrange show "y ∈∘ ℛ∘ (T⦇ArrVal⦈) ⟹ y ∈∘ B" for y
      by auto
    fix b assume [intro]: "b ∈∘ B" show "b ∈∘ ℛ∘ (T⦇ArrVal⦈)"
    proof(rule ccontr)
      assume prems: "b ∉∘ ℛ∘ (T⦇ArrVal⦈)"
      define R where "R = [set {⟨b, 0⟩}, B, set {0, 1}]∘"
      define S where "S = [set {⟨b, 1⟩}, B, set {0, 1}]∘"
      have R: "R : B ↦⇘smc_Par α⇙ set {0, 1}" 
        unfolding R_def
      proof
        (
          intro smc_Par_is_arrI T.arr_Par_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_Par α⇙ set {0, 1}"
        unfolding S_def
      proof
        (
          intro smc_Par_is_arrI T.arr_Par_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 prems have "R⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈ = 0"
        unfolding R_def arr_Rel_components
        by (auto intro!: vsubset_antisym vsubsetI)
      moreover from prems have "S⦇ArrVal⦈ ∘∘ T⦇ArrVal⦈ = 0" 
        unfolding S_def arr_Rel_components
        by (auto intro!: vsubset_antisym vsubsetI)
      ultimately have "R ∘A⇘smc_Par α⇙ T = S ∘A⇘smc_Par α⇙ T" 
        unfolding smc_Par_Comp_app[OF R T] smc_Par_Comp_app[OF S T]
        by (simp add: R_def S_def arr_Rel_components comp_Rel_def)
      from is_epic_arrD(2)[OF assms R S this] show False 
        unfolding R_def S_def by simp
    qed
  qed

qed

end

lemma smc_Par_is_epic_arr: 
  "T : A ↦epi⇘smc_Par α⇙ B ⟷ T : A ↦⇘smc_Par α⇙ B ∧ ℛ∘ (T⦇ArrVal⦈) = B" 
  by (intro iffI) (simp_all add: smc_Par_is_epic_arrD smc_Par_is_epic_arrI)



subsection‹Terminal object, initial object and null object›

lemma (in 𝒵) smc_Par_obj_terminal: "obj_terminal (smc_Par α) A ⟷ A = 0"
proof-

  interpret semicategory α ‹smc_Par α› by (rule semicategory_smc_Par)

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

    assume prems[rule_format]: "∀A∈∘Vset α. ∃!T. T : A ↦⇘smc_Par α⇙ B" 
    
    then obtain T where "T : 0 ↦⇘smc_Par α⇙ B" by (meson vempty_is_zet)
    then have [simp]: "B ∈∘ Vset α" by (fastforce simp: smc_Par_components(1))
    
    show "B = 0"
    proof(rule ccontr)
      assume "B ≠ 0"
      then obtain b where "b ∈∘ B" using trad_foundation by auto
      have "[set {⟨0, b⟩}, set {0}, B]∘ : set {0} ↦⇘smc_Par α⇙ B"
        by (intro smc_Par_is_arrI arr_Par_vfsequenceI, unfold arr_Rel_components)
          (auto simp: ‹b ∈∘ B› vsubset_vsingleton_leftI)
      moreover have "[0, set {0}, B]∘ : set {0} ↦⇘smc_Par α⇙ B"
        by (intro smc_Par_is_arrI arr_Par_vfsequenceI, unfold arr_Rel_components)
          (auto simp: ‹b ∈∘ B› vsubset_vsingleton_leftI)
      moreover have "[set {⟨0, b⟩}, set {0}, B]∘ ≠ [0, set {0}, B]∘" by simp
      ultimately show False
        by (metis prems smc_is_arrE smc_Par_components(1))
    qed

  next

    fix A assume [simp]: "B = 0" "A ∈∘ Vset α"
    show "∃!T. T : A ↦⇘smc_Par α⇙ B"
    proof(intro ex1I [of _ ‹[0, A, 0]∘›])
      show zAz: "[0, A, 0]∘ : A ↦⇘smc_Par α⇙ B"
        by 
          ( 
            intro smc_Par_is_arrI arr_Par_vfsequenceI, 
            unfold arr_Rel_components
          ) 
          simp_all
      show "T = [0, A, 0]∘" if "T : A ↦⇘smc_Par α⇙ B" for T
      proof(rule arr_Par_eqI[of α], unfold arr_Rel_components)
        interpret arr_Par α T using that by (simp add: smc_Par_is_arrD(1))
        from zAz show "arr_Par α [0, A, 0]∘" by (auto elim: smc_Par_is_arrE)
        from arr_Par_axioms that show "T⦇ArrVal⦈ = 0"
          by (clarsimp simp: vsv.vsv_vrange_vempty smc_Par_is_arrD(3))
      qed (use that in ‹auto dest: smc_Par_is_arrD›)
    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_Par_components(1))
    done

qed

lemma (in 𝒵) smc_Par_obj_initial: "obj_initial (smc_Par α) A ⟷ A = 0"
proof-

  interpret Par: semicategory α ‹smc_Par α› by (rule semicategory_smc_Par)

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

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

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

    show "A = 0"
    proof(rule ccontr)
      assume "A ≠ 0"
      then obtain a where "a ∈∘ A" using trad_foundation by auto
      have "[set {⟨a, 0⟩}, A, set {0}]∘ : A ↦⇘smc_Par α⇙ set {0}"
        by (intro smc_Par_is_arrI arr_Par_vfsequenceI, unfold arr_Rel_components)
          (auto simp: ‹a ∈∘ A› vsubset_vsingleton_leftI)
      moreover have "[0, A, set {0}]∘ : A ↦⇘smc_Par α⇙ set {0}"
        by (intro smc_Par_is_arrI arr_Par_vfsequenceI, unfold arr_Rel_components)
          (auto simp: ‹a ∈∘ A› vsubset_vsingleton_leftI)
      moreover have "[set {⟨a, 0⟩}, A, set {0}]∘ ≠ [0, A, set {0}]∘" by simp
      ultimately show False 
        by (metis prems Par.smc_is_arrE smc_Par_components(1))
    qed

  next

    fix B assume prems[simp]: "A = 0" "B ∈∘ Vset α"

    show "∃!T. T : A ↦⇘smc_Par α⇙ B"
    proof(intro ex1I[of _ ‹[0, 0, B]∘›])
      show zzB: "[0, 0, B]∘ : A ↦⇘smc_Par α⇙ B"
        by 
          ( 
            intro smc_Par_is_arrI arr_Par_vfsequenceI, 
            unfold arr_Rel_components
          ) 
          simp_all
      show "T = [0, 0, B]∘" if "T : A ↦⇘smc_Par α⇙ B" for T
      proof(rule arr_Par_eqI[of α], unfold arr_Rel_components)
        interpret arr_Par α T using that by (simp add: smc_Par_is_arrD(1))
        show "arr_Par α T" by (rule arr_Par_axioms)
        from zzB show "arr_Par α [0, 0, B]∘" by (auto elim: smc_Par_is_arrE)
        from arr_Par_axioms that show "T⦇ArrVal⦈ = 0"
          by (elim smc_Par_is_arrE arr_ParE)
            (
              auto 
                intro: ArrVal.vsv_vrange_vempty 
                simp: ArrVal.vdomain_vrange_is_vempty
            )
      qed (use that in ‹auto dest: smc_Par_is_arrD›)
    qed
  qed

  then show ?thesis
    unfolding obj_initial_def
    apply(intro iffI obj_terminalI, elim obj_terminalE, unfold smc_op_simps)
    subgoal by (metis smc_Par_components(1))
    subgoal by (simp add: smc_Par_components(1))
    subgoal by (metis smc_Par_components(1))
    done

qed

lemma (in 𝒵) smc_Par_obj_terminal_obj_initial:
  "obj_initial (smc_Par α) A ⟷ obj_terminal (smc_Par α) A"
  unfolding smc_Par_obj_initial smc_Par_obj_terminal by simp

lemma (in 𝒵) smc_Par_obj_null: "obj_null (smc_Par α) A ⟷ A = 0"
  unfolding obj_null_def smc_Par_obj_terminal smc_Par_obj_initial by simp



subsection‹Zero arrow›

lemma (in 𝒵) smc_Par_is_zero_arr: 
  assumes "A ∈∘ smc_Par α⦇Obj⦈" and "B ∈∘ smc_Par α⦇Obj⦈"
  shows "T : A ↦0⇘smc_Par α⇙ B ⟷ T = [0, A, B]∘"
proof(intro HOL.ext iffI)
  interpret Par: semicategory α ‹smc_Par α› by (rule semicategory_smc_Par)
  fix T A B assume "T : A ↦0⇘smc_Par α⇙ B"
  with smc_Par_is_arrD(1) obtain R S 
    where T_def: "T = R ∘A⇘smc_Par α⇙ S" 
      and S: "S : A ↦⇘smc_Par α⇙ 0" 
      and R: "R : 0 ↦⇘smc_Par α⇙ B"
    by (auto simp: arr_Par_def 𝒵.smc_Par_obj_initial obj_null_def) 
  interpret S: arr_Par α S
    rewrites [simp]: "S⦇ArrDom⦈ = A" and [simp]: "S⦇ArrCod⦈ = 0"
    using S smc_Par_is_arrD by auto
  interpret R: arr_Par α R
    rewrites [simp]: "R⦇ArrDom⦈ = 0" and [simp]: "R⦇ArrCod⦈ = B"
    using R smc_Par_is_arrD by auto
  have S_def: "S = [0, A, 0]∘"
    by 
      (
        rule arr_Rel_eqI[of α], 
        unfold arr_Rel_components,
        insert S.arr_Rel_ArrVal_vrange S.ArrVal.vbrelation_vintersection_vrange
      )
      (
        auto simp: 
        S.arr_Rel_axioms 
        S.arr_Rel_ArrDom_in_Vset 
        arr_Rel_vfsequenceI vbrelationI
      )
  show "T = [0, A, B]∘" 
     unfolding T_def smc_Par_Comp_app[OF R S] 
     by (rule arr_Rel_eqI[of α], unfold comp_Rel_components)
       (
         auto simp: 
          𝒵_axioms
          S_def
          R.arr_Rel_axioms 
          S.arr_Rel_axioms 
          arr_Rel_comp_Rel
          arr_Rel_components
          R.arr_Rel_ArrCod_in_Vset 
          S.arr_Rel_ArrDom_in_Vset 
          𝒵.arr_Rel_vfsequenceI 
          vbrelation_vempty
       )
next
  fix T assume prems: "T = [0, A, B]∘"
  let ?S = ‹[0, A, 0]∘› and ?R = ‹[0, 0, B]∘›
  have S: "arr_Par α ?S" and R: "arr_Par α ?R"  
    by (all‹intro arr_Par_vfsequenceI›)
      (simp_all add: assms[unfolded smc_Par_components])
  have SA0: "?S : A ↦⇘smc_Par α⇙ 0"
    by (intro smc_Par_is_arrI) (simp_all add: S arr_Rel_components)
  moreover have R0B: "?R : 0 ↦⇘smc_Par α⇙ B"
    by (intro smc_Par_is_arrI) (simp_all add: R arr_Rel_components)
  moreover have "T = ?R ∘A⇘smc_Par α⇙ ?S" 
    unfolding smc_Par_Comp_app[OF R0B SA0]
  proof
    (
      rule arr_Par_eqI[of α],
      unfold comp_Rel_components arr_Rel_components prems
    )
    show "arr_Par α [0, A, B]∘"
      unfolding prems 
      by (intro arr_Par_vfsequenceI) 
        (auto simp: assms[unfolded smc_Par_components])
  qed (use R S in ‹auto simp: smc_Par_cs_intros›)
  ultimately show "T : A ↦0⇘smc_Par α⇙ B" 
    by (simp add: is_zero_arrI smc_Par_obj_null)
qed

text‹\newpage›

end