Theory CZH_SMC_Rel

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Rel› as a semicategory›
theory CZH_SMC_Rel
  imports 
    CZH_DG_Rel
    CZH_SMC_Semifunctor
    CZH_SMC_Small_Semicategory
begin



subsection‹Background›


text‹
The methodology chosen for the exposition 
of ‹Rel› as a semicategory is analogous to the 
one used in the previous chapter for the exposition of ‹Rel› as a digraph. 
The general references for this section are Chapter I-7 
in cite‹"mac_lane_categories_2010"› and nLab 
cite‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/Rel}
}.
›

named_theorems smc_Rel_cs_simps
named_theorems smc_Rel_cs_intros

lemmas (in arr_Rel) [smc_Rel_cs_simps] = 
  dg_Rel_shared_cs_simps

lemmas (in arr_Rel) [smc_cs_intros, smc_Rel_cs_intros] = 
  arr_Rel_axioms'

lemmas [smc_Rel_cs_simps] = 
  dg_Rel_shared_cs_simps
  arr_Rel.arr_Rel_length
  arr_Rel_comp_Rel_id_Rel_left
  arr_Rel_comp_Rel_id_Rel_right
  arr_Rel.arr_Rel_converse_Rel_converse_Rel
  arr_Rel_converse_Rel_eq_iff
  arr_Rel_converse_Rel_comp_Rel
  arr_Rel_comp_Rel_converse_Rel_left_if_v11
  arr_Rel_comp_Rel_converse_Rel_right_if_v11

lemmas [smc_Rel_cs_intros] =
  dg_Rel_shared_cs_intros
  arr_Rel_comp_Rel
  arr_Rel.arr_Rel_converse_Rel



subsection‹‹Rel› as a semicategory›


subsubsection‹Definition and elementary properties›

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


text‹Components.›

lemma smc_Rel_components:
  shows "smc_Rel α⦇Obj⦈ = Vset α"
    and "smc_Rel α⦇Arr⦈ = set {T. arr_Rel α T}"
    and "smc_Rel α⦇Dom⦈ = (λT∈∘set {T. arr_Rel α T}. T⦇ArrDom⦈)"
    and "smc_Rel α⦇Cod⦈ = (λT∈∘set {T. arr_Rel α T}. T⦇ArrCod⦈)"
    and "smc_Rel α⦇Comp⦈ = (λST∈∘composable_arrs (dg_Rel α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)"
  unfolding smc_Rel_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smc_dg_smc_Rel: "smc_dg (smc_Rel α) = dg_Rel α"
proof(rule vsv_eqI)
  show "vsv (smc_dg (smc_Rel α))" unfolding smc_dg_def by auto
  show "vsv (dg_Rel α)" unfolding dg_Rel_def by auto
  have dom_lhs: "𝒟∘ (smc_dg (smc_Rel α)) = 4ℕ" 
    unfolding smc_dg_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ (dg_Rel α) = 4ℕ"
    unfolding dg_Rel_def by (simp add: nat_omega_simps)
  show "𝒟∘ (smc_dg (smc_Rel α)) = 𝒟∘ (dg_Rel α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ (smc_dg (smc_Rel α)) ⟹ smc_dg (smc_Rel α)⦇a⦈ = dg_Rel α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold smc_dg_def dg_field_simps smc_Rel_def dg_Rel_def
      )
      (auto simp: nat_omega_simps)
qed

lemmas_with [folded smc_dg_smc_Rel, unfolded slicing_simps]: 
  smc_Rel_Obj_iff = dg_Rel_Obj_iff
  and smc_Rel_Arr_iff[smc_Rel_cs_simps] = dg_Rel_Arr_iff
  and smc_Rel_Dom_vsv[smc_Rel_cs_intros] = dg_Rel_Dom_vsv
  and smc_Rel_Dom_vdomain[smc_Rel_cs_simps] = dg_Rel_Dom_vdomain
  and smc_Rel_Dom_app[smc_Rel_cs_simps] = dg_Rel_Dom_app
  and smc_Rel_Dom_vrange = dg_Rel_Dom_vrange
  and smc_Rel_Cod_vsv[smc_Rel_cs_intros] = dg_Rel_Cod_vsv
  and smc_Rel_Cod_vdomain[smc_Rel_cs_simps] = dg_Rel_Cod_vdomain
  and smc_Rel_Cod_app[smc_Rel_cs_simps] = dg_Rel_Cod_app
  and smc_Rel_Cod_vrange = dg_Rel_Cod_vrange
  and smc_Rel_is_arrI[smc_Rel_cs_intros] = dg_Rel_is_arrI
  and smc_Rel_is_arrD = dg_Rel_is_arrD
  and smc_Rel_is_arrE = dg_Rel_is_arrE
  and smc_Rel_is_arr_ArrValE = dg_Rel_is_arr_ArrValE

lemmas [smc_cs_simps] = smc_Rel_is_arrD(2,3)

lemmas_with (in 𝒵) [folded smc_dg_smc_Rel, unfolded slicing_simps]: 
  smc_Rel_Hom_vifunion_in_Vset = dg_Rel_Hom_vifunion_in_Vset
  and smc_Rel_incl_Rel_is_arr = dg_Rel_incl_Rel_is_arr
  and smc_Rel_incl_Rel_is_arr'[smc_Rel_cs_intros] = dg_Rel_incl_Rel_is_arr'

lemmas [smc_Rel_cs_intros] = 𝒵.smc_Rel_incl_Rel_is_arr'


subsubsection‹Composable arrows›

lemma smc_Rel_composable_arrs_dg_Rel: 
  "composable_arrs (dg_Rel α) = composable_arrs (smc_Rel α)"
  unfolding composable_arrs_def smc_dg_smc_Rel[symmetric] slicing_simps by simp

lemma smc_Rel_Comp: 
  "smc_Rel α⦇Comp⦈ = (λST∈∘composable_arrs (smc_Rel α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈)"
  unfolding smc_Rel_components smc_Rel_composable_arrs_dg_Rel ..


subsubsection‹Composition›

lemma smc_Rel_Comp_app[smc_Rel_cs_simps]:
  assumes "S : b ↦⇘smc_Rel α⇙ c" and "T : a ↦⇘smc_Rel α⇙ b"
  shows "S ∘A⇘smc_Rel α⇙ T = S ∘Rel T"
proof-
  from assms have "[S, T]∘ ∈∘ composable_arrs (smc_Rel α)" 
    by (auto intro: smc_cs_intros)
  then show "S ∘A⇘smc_Rel α⇙ T = S ∘Rel T"
    unfolding smc_Rel_Comp by (simp add: nat_omega_simps)
qed 

lemma smc_Rel_Comp_vdomain: "𝒟∘ (smc_Rel α⦇Comp⦈) = composable_arrs (smc_Rel α)" 
  unfolding smc_Rel_Comp by simp

lemma (in 𝒵) smc_Rel_Comp_vrange: "ℛ∘ (smc_Rel α⦇Comp⦈) ⊆∘ set {T. arr_Rel α T}"
proof(rule vsubsetI)
  interpret digraph α ‹smc_dg (smc_Rel α)›
    unfolding smc_dg_smc_Rel by (simp add: digraph_dg_Rel)
  fix R assume "R ∈∘ ℛ∘ (smc_Rel α⦇Comp⦈)"
  then obtain ST 
    where R_def: "R = smc_Rel α⦇Comp⦈⦇ST⦈"
      and "ST ∈∘ 𝒟∘ (smc_Rel α⦇Comp⦈)"
    unfolding smc_Rel_components by (auto intro: smc_cs_intros)
  then obtain S T a b c 
    where "ST = [S, T]∘" 
      and S: "S : b ↦⇘smc_Rel α⇙ c" 
      and T: "T : a ↦⇘smc_Rel α⇙ b"
    by (auto simp: smc_Rel_Comp_vdomain)
  with R_def have R_def': "R = S ∘A⇘smc_Rel α⇙ T" by simp
  note S_D = dg_is_arrD(1)[unfolded slicing_simps, OF S]
  note T_D = dg_is_arrD(1)[unfolded slicing_simps, OF T]
  from S_D T_D have "arr_Rel α S" "arr_Rel α T" 
    by (simp_all add: smc_Rel_components)
  from this show "R ∈∘ set {T. arr_Rel α T}" 
    unfolding R_def' smc_Rel_Comp_app[OF S T] by (auto simp: arr_Rel_comp_Rel)
qed


subsubsection‹‹Rel› is a semicategory›

lemma (in 𝒵) semicategory_smc_Rel: "semicategory α (smc_Rel α)"
proof(rule semicategoryI, unfold smc_dg_smc_Rel)
  show "vfsequence (smc_Rel α)" unfolding smc_Rel_def by simp
  show "vcard (smc_Rel α) = 5ℕ" 
    unfolding smc_Rel_def by (simp add: nat_omega_simps)
  show "gf ∈∘ 𝒟∘ (smc_Rel α⦇Comp⦈) ⟷ 
    (∃g f b c a. gf = [g, f]∘ ∧ g : b ↦⇘smc_Rel α⇙ c ∧ f : a ↦⇘smc_Rel α⇙ b)"
    for gf
    unfolding smc_Rel_Comp_vdomain by (auto intro: composable_arrsI)
  show "g ∘A⇘smc_Rel α⇙ f : a ↦⇘smc_Rel α⇙ c"
    if "g : b ↦⇘smc_Rel α⇙ c" and "f : a ↦⇘smc_Rel α⇙ b" for g b c f a
  proof-
    from that have "arr_Rel α g" and "arr_Rel α f" 
      by (auto simp: smc_Rel_is_arrD(1))
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_Rel_cs_simps cs_intro: smc_Rel_cs_intros
        )
  qed
  show "h ∘A⇘smc_Rel α⇙ g ∘A⇘smc_Rel α⇙ f = h ∘A⇘smc_Rel α⇙ (g ∘A⇘smc_Rel α⇙ f)"
    if "h : c ↦⇘smc_Rel α⇙ d" 
      and "g : b ↦⇘smc_Rel α⇙ c"
      and "f : a ↦⇘smc_Rel α⇙ b"
    for h c d g b f a
  proof-
    from that have "arr_Rel α h" and "arr_Rel α g" and "arr_Rel α f" 
      by (auto simp: smc_Rel_is_arrD(1))
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: smc_cs_simps smc_Rel_cs_simps 
            cs_intro: smc_Rel_cs_intros
        )
  qed
qed (auto simp: digraph_dg_Rel smc_Rel_components)



subsection‹Canonical dagger for ‹Rel››


subsubsection‹Definition and elementary properties›

definition smcf_dag_Rel :: "V ⇒ V" (‹†SMC.Rel›)
  where "†SMC.Rel α =
    [
      vid_on (smc_Rel α⦇Obj⦈),
      VLambda (smc_Rel α⦇Arr⦈) converse_Rel,
      op_smc (smc_Rel α), 
      smc_Rel α
    ]∘"


text‹Components.›

lemma smcf_dag_Rel_components:
  shows "†SMC.Rel α⦇ObjMap⦈ = vid_on (smc_Rel α⦇Obj⦈)"
    and "†SMC.Rel α⦇ArrMap⦈ = VLambda (smc_Rel α⦇Arr⦈) converse_Rel"
    and "†SMC.Rel α⦇HomDom⦈ = op_smc (smc_Rel α)"
    and "†SMC.Rel α⦇HomCod⦈ = smc_Rel α"
  unfolding smcf_dag_Rel_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smcf_dghm_smcf_dag_Rel: "smcf_dghm (†SMC.Rel α) = †DG.Rel α"
proof(rule vsv_eqI)
  show "vsv (smcf_dghm (†SMC.Rel α))" unfolding smcf_dghm_def by auto
  show "vsv (†DG.Rel α)" unfolding dghm_dag_Rel_def by auto
  have dom_lhs: "𝒟∘ (smcf_dghm (†SMC.Rel α)) = 4ℕ" 
    unfolding smcf_dghm_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ (†DG.Rel α) = 4ℕ"
    unfolding dghm_dag_Rel_def by (simp add: nat_omega_simps)
  show "𝒟∘ (smcf_dghm (†SMC.Rel α)) = 𝒟∘ (†DG.Rel α)"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ (smcf_dghm (†SMC.Rel α)) ⟹
    smcf_dghm (†SMC.Rel α)⦇a⦈ = †DG.Rel α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        unfold dghm_field_simps[symmetric],
        unfold 
          smc_dg_smc_Rel
          slicing_commute[symmetric]
          smcf_dghm_components 
          dghm_dag_Rel_components
          smcf_dag_Rel_components
          dg_Rel_components
          smc_Rel_components
      )
      simp_all
qed

lemmas_with [
    folded smc_dg_smc_Rel smcf_dghm_smcf_dag_Rel, unfolded slicing_simps
    ]: 
  smcf_dag_Rel_ObjMap_vsv[smc_Rel_cs_intros] = dghm_dag_Rel_ObjMap_vsv
  and smcf_dag_Rel_ObjMap_vdomain[smc_Rel_cs_simps] = 
    dghm_dag_Rel_ObjMap_vdomain
  and smcf_dag_Rel_ObjMap_app[smc_Rel_cs_simps] = dghm_dag_Rel_ObjMap_app
  and smcf_dag_Rel_ObjMap_vrange[smc_Rel_cs_simps] = dghm_dag_Rel_ObjMap_vrange
  and smcf_dag_Rel_ArrMap_vsv[smc_Rel_cs_intros] = dghm_dag_Rel_ArrMap_vsv
  and smcf_dag_Rel_ArrMap_vdomain[smc_Rel_cs_simps] = 
    dghm_dag_Rel_ArrMap_vdomain
  and smcf_dag_Rel_ArrMap_app[smc_Rel_cs_simps] = dghm_dag_Rel_ArrMap_app
  and smcf_dag_Rel_ArrMap_app_vdomain[smc_cs_simps] = 
    dghm_dag_Rel_ArrMap_app_vdomain
  and smcf_dag_Rel_ArrMap_app_vrange[smc_cs_simps] = 
    dghm_dag_Rel_ArrMap_app_vrange
  and smcf_dag_Rel_ArrMap_vrange[smc_Rel_cs_simps] = dghm_dag_Rel_ArrMap_vrange
  and smcf_dag_Rel_ArrMap_app_iff[smc_cs_simps] = dghm_dag_Rel_ArrMap_app_iff
  and smcf_dag_Rel_app_is_arr = dghm_dag_Rel_ArrMap_app_is_arr


subsubsection‹Canonical dagger is a contravariant isomorphism of ‹Rel››

lemma (in 𝒵) smcf_dag_Rel_is_iso_semifunctor: 
  "†SMC.Rel α : op_smc (smc_Rel α) ↦↦SMC.iso⇘α⇙ smc_Rel α"
proof(rule is_iso_semifunctorI)
  interpret dag: is_iso_dghm α ‹op_dg (dg_Rel α)› ‹dg_Rel α› ‹†DG.Rel α›
    by (rule dghm_dag_Rel_is_iso_dghm)
  interpret Rel: semicategory α ‹smc_Rel α› 
    by (rule semicategory_smc_Rel)
  show "†SMC.Rel α : op_smc (smc_Rel α) ↦↦SMC⇘α⇙ smc_Rel α"
  proof
    (
      rule is_semifunctorI,
      unfold 
        smc_dg_smc_Rel 
        smcf_dghm_smcf_dag_Rel 
        smc_op_simps 
        slicing_commute[symmetric] 
        smcf_dag_Rel_components(3,4)
    )
    show "vfsequence (†SMC.Rel α)"
      unfolding smcf_dag_Rel_def by (simp add: nat_omega_simps)
    show "vcard (†SMC.Rel α) = 4ℕ"
      unfolding smcf_dag_Rel_def by (simp add: nat_omega_simps)
    show "†SMC.Rel α⦇ArrMap⦈⦇f ∘A⇘smc_Rel α⇙ g⦈ =
      †SMC.Rel α⦇ArrMap⦈⦇g⦈ ∘A⇘smc_Rel α⇙ †SMC.Rel α⦇ArrMap⦈⦇f⦈"
      if "g : c ↦⇘smc_Rel α⇙ b" and "f : b ↦⇘smc_Rel α⇙ a"
      for g b c f a
    proof-
      from that have "arr_Rel α g" and "arr_Rel α f" 
        by (auto simp: smc_Rel_is_arrD(1))
      with that show ?thesis
        by 
          (
            cs_concl cs_shallow
              cs_simp: smc_cs_simps smc_Rel_cs_simps 
              cs_intro: smc_Rel_cs_intros
          )
    qed
  qed (auto simp: dg_cs_intros smc_op_intros semicategory_smc_Rel) 

  show "smcf_dghm (†SMC.Rel α) :
    smc_dg (op_smc (smc_Rel α)) ↦↦DG.iso⇘α⇙ smc_dg (smc_Rel α)"
    by 
      (
        simp add: 
          smc_dg_smc_Rel 
          smcf_dghm_smcf_dag_Rel 
          smc_op_simps 
          slicing_simps 
          slicing_commute[symmetric] 
          dghm_dag_Rel_is_iso_dghm
      )

qed


subsubsection‹Further properties of the canonical dagger›

lemma (in 𝒵) smcf_cn_comp_smcf_dag_Rel_smcf_dag_Rel: 
  "†SMC.Rel α SMCF∘ †SMC.Rel α = smcf_id (smc_Rel α)"
proof(rule smcf_dghm_eqI)
  interpret semicategory α ‹smc_Rel α› by (simp add: semicategory_smc_Rel)
  from smcf_dag_Rel_is_iso_semifunctor have dag:
    "†SMC.Rel α : op_smc (smc_Rel α) ↦↦SMC⇘α⇙ smc_Rel α"
    by (simp add: is_iso_semifunctor.axioms(1))
  from smcf_cn_comp_is_semifunctor[OF semicategory_axioms dag dag] show 
    "†SMC.Rel α SMCF∘ †SMC.Rel α : smc_Rel α ↦↦SMC⇘α⇙ smc_Rel α" .
  show "smcf_id (smc_Rel α) : smc_Rel α ↦↦SMC⇘α⇙ smc_Rel α"
    by (auto simp: smc_smcf_id_is_semifunctor)
  show "smcf_dghm (†SMC.Rel α SMCF∘ †SMC.Rel α) = smcf_dghm (smcf_id (smc_Rel α))"
    unfolding 
      slicing_simps slicing_commute[symmetric] 
      smc_dg_smc_Rel 
      smcf_dghm_smcf_dag_Rel
    by (simp add: dghm_cn_comp_dghm_dag_Rel_dghm_dag_Rel)
qed simp_all

lemma smcf_dag_Rel_ArrMap_smc_Rel_Comp:
  assumes "S : b ↦⇘smc_Rel α⇙ c" and "T : a ↦⇘smc_Rel α⇙ b"
  shows "†SMC.Rel α⦇ArrMap⦈⦇S ∘A⇘smc_Rel α⇙ T⦈ =
    †SMC.Rel α⦇ArrMap⦈⦇T⦈ ∘A⇘smc_Rel α⇙ †SMC.Rel α⦇ArrMap⦈⦇S⦈"
proof-
  from assms have "arr_Rel α S" and "arr_Rel α T" 
    by (auto simp: smc_Rel_is_arrD(1))
  with assms show ?thesis
    by 
      (
        cs_concl cs_shallow
          cs_simp: smc_cs_simps smc_Rel_cs_simps cs_intro: smc_Rel_cs_intros
      )
qed



subsection‹Monic arrow and epic arrow›


text‹
The conditions for an arrow of ‹Rel› to be either monic or epic are 
outlined in nLab cite‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/Rel}
}.
›

context
begin

private lemma smc_Rel_is_monic_arr_vsubset: 
  assumes "T : A ↦⇘smc_Rel α⇙ B" 
    and "R : A' ↦⇘smc_Rel α⇙ A" 
    and "S : A' ↦⇘smc_Rel α⇙ A" 
    and "T ∘A⇘smc_Rel α⇙ R = T ∘A⇘smc_Rel α⇙ S"
    and "⋀y z X. 
      ⟦ y ⊆∘ A; z ⊆∘ A; T⦇ArrVal⦈ `∘ y = X; T⦇ArrVal⦈ `∘ z = X ⟧ ⟹ y = z"
  shows "R⦇ArrVal⦈ ⊆∘ S⦇ArrVal⦈"
proof-
  interpret R: arr_Rel α R 
    rewrites "R⦇ArrDom⦈ = A'" and "R⦇ArrCod⦈ = A"
    by (intro smc_Rel_is_arrD[OF assms(2)])+
  interpret S: arr_Rel α S
    rewrites "S⦇ArrDom⦈ = A'" and "S⦇ArrCod⦈ = A"
    by (intro smc_Rel_is_arrD[OF assms(3)])+
  interpret Rel: semicategory α ‹smc_Rel α› by (rule R.semicategory_smc_Rel)
  from assms(4) have "(T ∘A⇘smc_Rel α⇙ R)⦇ArrVal⦈ = (T ∘A⇘smc_Rel α⇙ S)⦇ArrVal⦈"
    by simp
  then have eq: "T⦇ArrVal⦈ ∘∘ R⦇ArrVal⦈ = T⦇ArrVal⦈ ∘∘ S⦇ArrVal⦈"
    unfolding 
      smc_Rel_Comp_app[OF assms(1,2)]
      smc_Rel_Comp_app[OF assms(1,3)]
      comp_Rel_components
    by simp
  show "R⦇ArrVal⦈ ⊆∘ S⦇ArrVal⦈"
  proof(rule vsubsetI)    
    fix ab assume ab[intro]: "ab ∈∘ R⦇ArrVal⦈"
    with R.ArrVal.vbrelation obtain a b where ab_def: "ab = ⟨a, b⟩" by auto 
    with ab R.arr_Rel_ArrVal_vrange have "a ∈∘ 𝒟∘ (R⦇ArrVal⦈)" and "b ∈∘ A" 
      by auto
    define B' and C' where "B' = R⦇ArrVal⦈ `∘ set {a}" and "C' = T⦇ArrVal⦈ `∘ B'"
    have ne_C': "C' ≠ 0"
    proof(rule ccontr, unfold not_not)
      assume prems: "C' = 0"
      from ab have "b ∈∘ B'" unfolding ab_def B'_def by simp
      with C'_def[unfolded prems] have b0: "T⦇ArrVal⦈ `∘ set {b} = 0" by auto
      from assms(5)[OF _ _ b0, of 0] ‹b ∈∘ A› show False by auto
    qed
    have cac''[intro, simp]: 
      "c ∈∘ C' ⟹ ⟨a, c⟩ ∈∘ T⦇ArrVal⦈ ∘∘ S⦇ArrVal⦈" for c
      unfolding eq[symmetric] C'_def B'_def 
      by (metis vcomp_vimage vimage_vsingleton_iff)
    define A'' where "A'' = (T⦇ArrVal⦈ ∘∘ S⦇ArrVal⦈) -`∘ C'"
    define B'' where "B'' = S⦇ArrVal⦈ `∘ set {a}"
    define C'' where "C'' = T⦇ArrVal⦈ `∘ B''"
    have a'': "a ∈∘ A''"
    proof-
      from ne_C' obtain c' where [intro]: "c' ∈∘ C'" 
        by (auto intro!: vsubset_antisym)
      then have "⟨a, c'⟩ ∈∘ T⦇ArrVal⦈ ∘∘ S⦇ArrVal⦈" by simp
      then show ?thesis unfolding A''_def by auto
    qed
    have "C' ⊆∘ C''"
      unfolding C''_def B''_def A''_def C'_def B'_def
      by (rule vsubsetI) (metis eq vcomp_vimage)
    have "C' = C''"
    proof(rule ccontr)
      assume "C' ≠ C''"
      with ‹C' ⊆∘ C''› obtain c' where c': "c' ∈∘ C'' -∘ C'" 
        by (auto intro!: vsubset_antisym)
      then obtain b'' where "b'' ∈∘ B''" and "⟨b'', c'⟩ ∈∘ T⦇ArrVal⦈"
        unfolding C''_def by auto
      then have "⟨a, c'⟩ ∈∘ T⦇ArrVal⦈ ∘∘ R⦇ArrVal⦈" unfolding eq B''_def by auto
      with c' show False unfolding B'_def C'_def by auto
    qed
    then have "T⦇ArrVal⦈ `∘ B'' = T⦇ArrVal⦈ `∘ B'" by (simp add: C''_def C'_def)
    moreover have "B' ⊆∘ A" and "B'' ⊆∘ A"
      using R.arr_Rel_ArrVal_vrange S.arr_Rel_ArrVal_vrange         
      unfolding B'_def B''_def 
      by auto
    ultimately have "B'' = B'" by (simp add: assms(5))
    with ab have "b ∈∘ B''" unfolding B'_def ab_def by simp
    then show "ab ∈∘ S⦇ArrVal⦈" unfolding ab_def B''_def by simp
  qed
qed

lemma smc_Rel_is_monic_arrI:
  assumes "T : A ↦⇘smc_Rel α⇙ B"  
    and "⋀y z X. ⟦ y ⊆∘ A; z ⊆∘ A; T⦇ArrVal⦈ `∘ y = X; T⦇ArrVal⦈ `∘ z = X ⟧ ⟹ 
      y = z"
  shows "T : A ↦mon⇘smc_Rel α⇙ B"
proof(rule is_monic_arrI)

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

  interpret Rel: semicategory α ‹smc_Rel α› by (simp add: T.semicategory_smc_Rel)

  fix R S A' assume prems: 
    "R : A' ↦⇘smc_Rel α⇙ A" 
    "S : A' ↦⇘smc_Rel α⇙ A"
    "T ∘A⇘smc_Rel α⇙ R = T ∘A⇘smc_Rel α⇙ S"

  interpret R: arr_Rel α R 
    rewrites [simp]: "R⦇ArrDom⦈ = A'" and [simp]: "R⦇ArrCod⦈ = A"
    by (intro smc_Rel_is_arrD[OF prems(1)])+
  interpret S: arr_Rel α S
    rewrites [simp]: "S⦇ArrDom⦈ = A'" and [simp]: "S⦇ArrCod⦈ = A"
    by (intro smc_Rel_is_arrD[OF prems(2)])+

  from assms prems have 
    "R⦇ArrVal⦈ ⊆∘ S⦇ArrVal⦈" "S⦇ArrVal⦈ ⊆∘ R⦇ArrVal⦈" 
    by (auto simp: smc_Rel_is_monic_arr_vsubset)
  then show "R = S"
    using R.arr_Rel_axioms S.arr_Rel_axioms 
    by (intro arr_Rel_eqI[of α R S]) auto

qed (rule assms(1))

end

lemma smc_Rel_is_monic_arrD[dest]:
  assumes "T : A ↦mon⇘smc_Rel α⇙ B"
    and "y ⊆∘ A"
    and "z ⊆∘ A" 
    and "T⦇ArrVal⦈ `∘ y = X" 
    and "T⦇ArrVal⦈ `∘ z = X" 
  shows "y = z"
proof-

  from assms have T: "T : A ↦⇘smc_Rel α⇙ B" by (simp add: is_monic_arr_def)

  interpret T: arr_Rel α T
    rewrites "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    by (intro smc_Rel_is_arrD[OF T])+

  interpret Rel: semicategory α ‹smc_Rel α› 
    by (simp add: T.semicategory_smc_Rel)
 
  define R where "R = [set {0} ×∘ y, set {0}, A]∘"
  define S where "S = [set {0} ×∘ z, set {0}, A]∘"
  
  have R: "R : set {0} ↦⇘smc_Rel α⇙ A" 
  proof(intro smc_Rel_is_arrI)
    show "arr_Rel α R"
      unfolding R_def
    proof(intro T.arr_Rel_vfsequenceI)
      from assms(2) show "ℛ∘ (set {0} ×∘ y) ⊆∘ A" by auto
    qed (auto simp: T.arr_Rel_ArrDom_in_Vset)
  qed (simp_all add: R_def arr_Rel_components)

  from assms(3) have S: "S : set {0} ↦⇘smc_Rel α⇙ A"
  proof(intro smc_Rel_is_arrI)
    show "arr_Rel α S"
      unfolding S_def
    proof(intro T.arr_Rel_vfsequenceI)
      from assms(3) show "ℛ∘ (set {0} ×∘ z) ⊆∘ A" by auto
    qed (auto simp: T.arr_Rel_ArrDom_in_Vset)
  qed (simp_all add: S_def arr_Rel_components)

  from assms(4) have "T ∘A⇘smc_Rel α⇙ R = [set {0} ×∘ X, set {0}, B]∘"
    unfolding smc_Rel_Comp_app[OF T R]
    unfolding comp_Rel_components R_def comp_Rel_def arr_Rel_components
    by (simp add: vcomp_vimage_vtimes_right)
  moreover from assms have "T ∘A⇘smc_Rel α⇙ S = [set {0} ×∘ X, set {0}, B]∘"
    unfolding smc_Rel_Comp_app[OF T S]
    unfolding comp_Rel_components S_def comp_Rel_def arr_Rel_components
    by (simp add: vcomp_vimage_vtimes_right)
  ultimately have "T ∘A⇘smc_Rel α⇙ R = T ∘A⇘smc_Rel α⇙ S" by simp
  from R S assms(1) this have "R = S" by (elim is_monic_arrE)
  then show "y = z" unfolding R_def S_def by auto

qed

lemma smc_Rel_is_monic_arr:
  "T : A ↦mon⇘smc_Rel α⇙ B ⟷
    T : A ↦⇘smc_Rel α⇙ B ∧
    (
      ∀y z X.
        y ⊆∘ A ⟶
        z ⊆∘ A ⟶
        (T⦇ArrVal⦈) `∘ y = X ⟶
        (T⦇ArrVal⦈) `∘ z = X ⟶
        y = z
    )"
  by (rule iffI allI impI) 
    (auto simp: smc_Rel_is_monic_arrD smc_Rel_is_monic_arrI)

lemma smc_Rel_is_monic_arr_is_epic_arr: 
  assumes "T : A ↦⇘smc_Rel α⇙ B" 
    and "(†SMC.Rel α)⦇ArrMap⦈⦇T⦈ : B ↦mon⇘smc_Rel α⇙ A"
  shows "T : A ↦epi⇘smc_Rel α⇙ B"
proof-

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

  interpret is_iso_semifunctor α ‹op_smc (smc_Rel α)› ‹smc_Rel α› ‹†SMC.Rel α›
    rewrites "op_smc ℭ'⦇Obj⦈ = ℭ'⦇Obj⦈" 
      and "op_smc ℭ'⦇Arr⦈ = ℭ'⦇Arr⦈"
      and "f : b ↦⇘op_smc ℭ'⇙ a ⟷ f : a ↦⇘ℭ'⇙ b" 
      for ℭ' f a b
    unfolding smc_op_simps by (auto simp: T.smcf_dag_Rel_is_iso_semifunctor)
  
  show ?thesis
  proof(intro HomCod.is_epic_arrI)

    show T: "T : A ↦⇘smc_Rel α⇙ B" by (rule assms(1))
  
    fix f g a assume prems: 
      "f : B ↦⇘smc_Rel α⇙ a" 
      "g : B ↦⇘smc_Rel α⇙ a" 
      "f ∘A⇘smc_Rel α⇙ T = g ∘A⇘smc_Rel α⇙ T" 
  
    from prems(1) have "†SMC.Rel α⦇ArrMap⦈⦇f⦈ :
      †SMC.Rel α⦇ObjMap⦈⦇a⦈ ↦⇘smc_Rel α⇙ †SMC.Rel α⦇ObjMap⦈⦇B⦈"
      by (auto intro: smc_cs_intros)
    with prems(1) HomCod.smc_is_arrD(3) T have dag_f: 
      "†SMC.Rel α⦇ArrMap⦈⦇f⦈ : a ↦⇘smc_Rel α⇙ B" 
      unfolding smcf_dag_Rel_components(1) by auto
    from prems(2) have "†SMC.Rel α⦇ArrMap⦈⦇g⦈ : 
      †SMC.Rel α⦇ObjMap⦈⦇a⦈ ↦⇘smc_Rel α⇙ †SMC.Rel α⦇ObjMap⦈⦇B⦈"
      by (auto intro: smc_cs_intros)
    with prems(2) have dag_g: "†SMC.Rel α⦇ArrMap⦈⦇g⦈ : a ↦⇘smc_Rel α⇙ B"
      unfolding smcf_dag_Rel_components(1) 
      by (metis HomCod.smc_is_arrD(3) T vid_on_eq_atI)
    from prems T have 
      "†SMC.Rel α⦇ArrMap⦈⦇T⦈ ∘A⇘smc_Rel α⇙ †SMC.Rel α⦇ArrMap⦈⦇f⦈ = 
        †SMC.Rel α⦇ArrMap⦈⦇T⦈ ∘A⇘smc_Rel α⇙ †SMC.Rel α⦇ArrMap⦈⦇g⦈"
      by (simp add: smcf_dag_Rel_ArrMap_smc_Rel_Comp[symmetric])
    from is_monic_arrD(2)[OF assms(2) dag_f dag_g this] show "f = g"
      by (meson prems HomDom.smc_is_arrD(1) ArrMap.v11_eq_iff)
  
  qed
qed

lemma smc_Rel_is_epic_arr_is_monic_arr:
  assumes "T : A ↦epi⇘smc_Rel α⇙ B" 
  shows "†SMC.Rel α⦇ArrMap⦈⦇T⦈ : B ↦mon⇘smc_Rel α⇙ A"
proof(rule is_monic_arrI)

  from assms(1) have T: "T : A ↦⇘smc_Rel α⇙ B" 
    by (simp add: is_epic_arr_def is_monic_arr_def smc_op_simps)

  interpret T: arr_Rel α T
    rewrites "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    by (intro smc_Rel_is_arrD[OF T])+

  interpret is_iso_semifunctor α ‹op_smc (smc_Rel α)› ‹smc_Rel α› ‹†SMC.Rel α› 
    rewrites "f : b ↦⇘op_smc ℭ'⇙ a ⟷ f : a ↦⇘ℭ'⇙ b" for ℭ' f a b
    unfolding smc_op_simps by (auto simp: T.smcf_dag_Rel_is_iso_semifunctor)

  have dag: "†SMC.Rel α : op_smc (smc_Rel α) ↦↦SMC⇘α⇙ smc_Rel α" 
    by (auto intro: smc_cs_intros)

  from HomCod.is_epic_arrD(1)[OF assms] have T: "T : A ↦⇘smc_Rel α⇙ B".

  from T have "†SMC.Rel α⦇ArrMap⦈⦇T⦈ : 
    †SMC.Rel α⦇ObjMap⦈⦇B⦈ ↦⇘smc_Rel α⇙ †SMC.Rel α⦇ObjMap⦈⦇A⦈"
    by (auto intro: smc_cs_intros)
  with T show dag_T: "†SMC.Rel α⦇ArrMap⦈⦇T⦈ : B ↦⇘smc_Rel α⇙ A"
    unfolding smcf_dag_Rel_components(1)
    by (metis HomCod.smc_is_arrD(2) HomCod.smc_is_arrD(3) vid_on_eq_atI)

  fix f g a assume prems:
    "f : a ↦⇘smc_Rel α⇙ B" 
    "g : a ↦⇘smc_Rel α⇙ B" 
    "†SMC.Rel α⦇ArrMap⦈⦇T⦈ ∘A⇘smc_Rel α⇙ f = †SMC.Rel α⦇ArrMap⦈⦇T⦈ ∘A⇘smc_Rel α⇙ g" 
  then have a: "a ∈∘ smc_Rel α⦇Obj⦈" by auto
  from prems(1) have "†SMC.Rel α⦇ArrMap⦈⦇f⦈ :
    †SMC.Rel α⦇ObjMap⦈⦇B⦈ ↦⇘smc_Rel α⇙ †SMC.Rel α⦇ObjMap⦈⦇a⦈"
    by (auto intro: smc_cs_intros)
  with prems(1) have dag_f: "†SMC.Rel α⦇ArrMap⦈⦇f⦈ : B ↦⇘smc_Rel α⇙ a"
    by (cs_concl cs_intro: smc_cs_intros cs_simp: smc_Rel_cs_simps)
  from prems(2) have "†SMC.Rel α⦇ArrMap⦈⦇g⦈ : 
    †SMC.Rel α⦇ObjMap⦈⦇B⦈ ↦⇘smc_Rel α⇙ †SMC.Rel α⦇ObjMap⦈⦇a⦈"
    by (cs_concl cs_shallow cs_intro: smc_cs_intros cs_simp:)
  with prems(2) have dag_g: "†SMC.Rel α⦇ArrMap⦈⦇g⦈ : B ↦⇘smc_Rel α⇙ a" 
    by (cs_concl cs_intro: smc_cs_intros cs_simp: smc_Rel_cs_simps)
  from T dag have 
    "†SMC.Rel α⦇ArrMap⦈⦇†SMC.Rel α⦇ArrMap⦈⦇T⦈⦈ =
      (†SMC.Rel α SMCF∘ †SMC.Rel α)⦇ArrMap⦈⦇T⦈"
    by
      (
        cs_concl 
          cs_intro: smc_cs_intros 
          cs_simp: smc_Rel_cs_simps smc_cn_cs_simps smc_cs_simps
      )
  also from T have "… = T" 
    unfolding dghm_id_components T.smcf_cn_comp_smcf_dag_Rel_smcf_dag_Rel 
    by auto
  finally have dag_dag_T: "†SMC.Rel α⦇ArrMap⦈⦇†SMC.Rel α⦇ArrMap⦈⦇T⦈⦈ = T" by simp
  have 
    "†SMC.Rel α⦇ArrMap⦈⦇f⦈ ∘A⇘smc_Rel α⇙ T = †SMC.Rel α⦇ArrMap⦈⦇g⦈ ∘A⇘smc_Rel α⇙ T"
    by (metis dag_T dag_dag_T prems smcf_dag_Rel_ArrMap_smc_Rel_Comp)
  from HomCod.is_epic_arrD(2)[OF assms dag_f dag_g this] prems ArrMap.v11_eq_iff
  show "f = g"
    by blast

qed

lemma smc_Rel_is_epic_arrI:
  assumes "T : A ↦⇘smc_Rel α⇙ B"  
    and "⋀y z X. ⟦ y ⊆∘ B; z ⊆∘ B; T⦇ArrVal⦈ -`∘ y = X; T⦇ArrVal⦈ -`∘ z = X ⟧ ⟹
      y = z"
  shows "T : A ↦epi⇘smc_Rel α⇙ B"
proof-

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

  interpret is_iso_semifunctor α ‹op_smc (smc_Rel α)› ‹smc_Rel α› ‹†SMC.Rel α› 
    rewrites "f : b ↦⇘op_smc ℭ'⇙ a ⟷ f : a ↦⇘ℭ'⇙ b" for ℭ' f a b 
    unfolding smc_op_simps by (auto simp: T.smcf_dag_Rel_is_iso_semifunctor)

  have "†SMC.Rel α⦇ArrMap⦈⦇T⦈ : B ↦mon⇘smc_Rel α⇙ A"
  proof(rule smc_Rel_is_monic_arrI)
    from assms(1) have "†SMC.Rel α⦇ArrMap⦈⦇T⦈ :
      †SMC.Rel α⦇ObjMap⦈⦇B⦈ ↦⇘smc_Rel α⇙ †SMC.Rel α⦇ObjMap⦈⦇A⦈"
      by (cs_concl cs_shallow cs_intro: smc_cs_intros)
    with assms(1) show "†SMC.Rel α⦇ArrMap⦈⦇T⦈ : B ↦⇘smc_Rel α⇙ A"
      by (cs_concl cs_intro: smc_cs_intros cs_simp: smc_Rel_cs_simps)
    fix y z X
    assume
      "y ⊆∘ B"
      "z ⊆∘ B" 
      "†SMC.Rel α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈ `∘ y = X" 
      "†SMC.Rel α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈ `∘ z = X" 
    then show "y = z"
      unfolding 
        converse_Rel_components 
        smcf_dag_Rel_ArrMap_app[OF T.arr_Rel_axioms] 
        app_invimage_def[symmetric]
      by (rule assms(2))
  qed
  from smc_Rel_is_monic_arr_is_epic_arr[OF assms(1) this] show ?thesis by simp
qed

lemma smc_Rel_is_epic_arrD[dest]:
  assumes "T : A ↦epi⇘smc_Rel α⇙ B"
    and "y ⊆∘ B"
    and "z ⊆∘ B" 
    and "T⦇ArrVal⦈ -`∘ y = X" 
    and "T⦇ArrVal⦈ -`∘ z = X" 
  shows "y = z"
proof-

  from assms(1) have T: "T : A ↦⇘smc_Rel α⇙ B" 
    by (simp add: is_epic_arr_def is_monic_arr_def smc_op_simps)

  interpret T: arr_Rel α T
    rewrites "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    by (intro smc_Rel_is_arrD[OF T])+

  interpret is_iso_semifunctor α ‹op_smc (smc_Rel α)› ‹smc_Rel α› ‹†SMC.Rel α› 
    rewrites "f : b ↦⇘op_smc ℭ'⇙ a ⟷ f : a ↦⇘ℭ'⇙ b" 
    for ℭ' f a b 
    unfolding smc_op_simps by (auto simp: T.smcf_dag_Rel_is_iso_semifunctor)
  have dag_T: "†SMC.Rel α⦇ArrMap⦈⦇T⦈ : B ↦mon⇘smc_Rel α⇙ A"
    by (rule smc_Rel_is_epic_arr_is_monic_arr[OF assms(1)])
  from HomCod.is_epic_arrD(1)[OF assms(1)] have T: "T : A ↦⇘smc_Rel α⇙ B".
  then have T: "arr_Rel α T" by (auto simp: smc_Rel_is_arrD(1))
  from 
    assms(4,5) 
    smc_Rel_is_monic_arrD
      [
        OF dag_T assms(2,3), 
        unfolded 
          smc_dg_smc_Rel 
          smcf_dghm_smcf_dag_Rel 
          converse_Rel_components 
          smcf_dag_Rel_ArrMap_app[OF T]
      ]
  show ?thesis
    by (auto simp: app_invimage_def)
qed

lemma smc_Rel_is_epic_arr:
  "T : A ↦epi⇘smc_Rel α⇙ B ⟷
    T : A ↦⇘smc_Rel α⇙ B ∧ 
      (
        ∀y z X.
          y ⊆∘ B ⟶
          z ⊆∘ B ⟶
          T⦇ArrVal⦈ -`∘ y = X ⟶
          T⦇ArrVal⦈ -`∘ z = X ⟶
          y = z
      )"
proof(intro iffI allI impI conjI)
  show "T : A ↦epi⇘smc_Rel α⇙ B ⟹ T : A ↦⇘smc_Rel α⇙ B"
    by (simp add: is_epic_arr_def is_monic_arr_def op_smc_is_arr)
qed (auto simp: smc_Rel_is_epic_arrI)



subsection‹Terminal object, initial object and null object›


text‹
An object in the semicategory ‹Rel› is terminal/initial/null if and only if 
it is the empty set (see
nLab cite‹"noauthor_nlab_nodate"›)\footnote{
\url{https://ncatlab.org/nlab/show/database+of+categories}
}. 
›

lemma (in 𝒵) smc_Rel_obj_terminal: "obj_terminal (smc_Rel α) A ⟷ A = 0"
proof-

  interpret semicategory α ‹smc_Rel α› by (rule semicategory_smc_Rel)

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

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

    then obtain T where "T : 0 ↦⇘smc_Rel α⇙ B" by (meson vempty_is_zet)
    then have [simp]: "B ∈∘ Vset α" by (fastforce simp: smc_Rel_components(1))
    
    show "B = 0"
    proof(rule ccontr)
      assume "B ≠ 0"
      with trad_foundation obtain b where "b ∈∘ B" by auto
      let ?b0B = ‹[set {⟨0, b⟩}, set {0}, B]∘›
      let ?z0B = ‹[0, set {0}, B]∘›
      have "?b0B : set {0} ↦⇘smc_Rel α⇙ B"
      proof(intro smc_Rel_is_arrI)
        show b0B: "arr_Rel α ?b0B"
          by (intro arr_Rel_vfsequenceI)
            (force simp: ‹b ∈∘ B› vsubset_vsingleton_leftI)+
      qed (simp_all add: arr_Rel_components)
      moreover have "?z0B : set {0} ↦⇘smc_Rel α⇙ B"
      proof(intro smc_Rel_is_arrI)
        show b0B: "arr_Rel α ?z0B"
          by (intro arr_Rel_vfsequenceI)
            (force simp: ‹b ∈∘ B› vsubset_vsingleton_leftI)+
      qed (simp_all add: arr_Rel_components)
      moreover have "[set {⟨0, b⟩}, set {0}, B]∘ ≠ [0, set {0}, B]∘" by simp
      ultimately show False  
        by (metis prems smc_is_arrE smc_Rel_components(1))
    qed

  next

    fix A assume prems[simp]: "B = 0" "A ∈∘ Vset α" 
    let ?zAz = ‹[0, A, 0]∘›
    have zAz: "arr_Rel α ?zAz"
      by 
        (
          simp add: 
            𝒵.arr_Rel_vfsequenceI 
            𝒵_axioms 
            smc_Rel_components(2) 
            vbrelation_vempty
        )

    show "∃!T. T : A ↦⇘smc_Rel α⇙ B"
    proof(rule ex1I[of _ ‹?zAz›])
      show "?zAz : A ↦⇘smc_Rel α⇙ B"
        by (intro smc_Rel_is_arrI)
          (
            simp_all add: 
              zAz 
              smc_Rel_Dom_app[OF zAz] 
              smc_Rel_Cod_app[OF zAz] 
              arr_Rel_components
          )      
      fix T assume "T : A ↦⇘smc_Rel α⇙ B"
      then have T: "T : A ↦⇘smc_Rel α⇙ 0" by simp
      then interpret T: arr_Rel α T by (fastforce simp: smc_Rel_components(2))
      show "T = [0, A, 0]∘"
      proof
        (
          subst T.arr_Rel_def, 
          rule arr_Rel_eqI[of α], 
          unfold arr_Rel_components
        )
        show "arr_Rel α [T⦇ArrVal⦈, T⦇ArrDom⦈, T⦇ArrCod⦈]∘"
          by (fold T.arr_Rel_def) (simp add: T.arr_Rel_axioms)
        from zAz show "arr_Rel α ?zAz" 
          by (simp add: arr_Rel_vfsequenceI vbrelationI)
        from T have "T ∈∘ smc_Rel α⦇Arr⦈" by (auto intro: smc_cs_intros)
        with is_arrD(2,3)[OF T] show "T⦇ArrDom⦈ = A" "T⦇ArrCod⦈ = 0"
          using T smc_Rel_is_arrD(2,3) by auto
        with T.arr_Rel_ArrVal_vrange T.ArrVal.vbrelation_vintersection_vrange 
        show "T⦇ArrVal⦈ = 0"
          by auto
      qed

    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_Rel_components(1))
    done

qed

(*TODO: generalize: duality/dagger*)
lemma (in 𝒵) smc_Rel_obj_initial: "obj_initial (smc_Rel α) A ⟷ A = 0"
proof-

  interpret semicategory α ‹smc_Rel α› by (rule semicategory_smc_Rel)

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

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

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

    show "A = 0"
    proof(rule ccontr)
      assume "A ≠ 0"
      with trad_foundation obtain a where "a ∈∘ A" by auto
      have "[set {⟨a, 0⟩}, A, set {0}]∘ : A ↦⇘smc_Rel α⇙ set {0}"
      proof(intro smc_Rel_is_arrI)
        show "arr_Rel α [set {⟨a, 0⟩}, A, set {0}]∘"
          by (intro arr_Rel_vfsequenceI)
            (auto simp: ‹a ∈∘ A› vsubset_vsingleton_leftI)
      qed (simp_all add: arr_Rel_components)
      moreover have "[0, A, set {0}]∘ : A ↦⇘smc_Rel α⇙ set {0}"
      proof(intro smc_Rel_is_arrI)
        show "arr_Rel α [0, A, set {0}]∘"
          by (intro arr_Rel_vfsequenceI)
            (auto simp: ‹a ∈∘ A› vsubset_vsingleton_leftI)
      qed (simp_all add: arr_Rel_components)
      moreover have "[set {⟨a, 0⟩}, A, set {0}]∘ ≠ [0, A, set {0}]∘" by simp
      ultimately show False
        by (metis prems smc_is_arrE smc_Rel_components(1))
    qed
  next

    fix B assume [simp]: "A = 0" "B ∈∘ Vset α" 
    show "∃!T. T : A ↦⇘smc_Rel α⇙ B"
    proof(rule ex1I[of _ ‹[0, 0, B]∘›])
      show "[0, 0, B]∘ : A ↦⇘smc_Rel α⇙ B"
        by (rule is_arrI)
          (
            simp_all add:
              smc_Rel_cs_simps
              smc_Rel_components(2) 
              vbrelation_vempty
              arr_Rel_vfsequenceI 
          )
      fix T assume "T : A ↦⇘smc_Rel α⇙ B"
      then have T: "T : 0 ↦⇘smc_Rel α⇙ B" by simp
      interpret T: arr_Rel α T 
        using T by (fastforce simp: smc_Rel_components(2))
      show "T = [0, 0, B]∘"
      proof
        (
          subst T.arr_Rel_def, 
          rule arr_Rel_eqI[of α], 
          unfold arr_Rel_components
        )
        show "arr_Rel α [T⦇ArrVal⦈, T⦇ArrDom⦈, T⦇ArrCod⦈]∘"
          by (fold T.arr_Rel_def) (simp add: T.arr_Rel_axioms)
        show "arr_Rel α [0, 0, B]∘" 
          by (simp add: arr_Rel_vfsequenceI vbrelationI)
        from T have "T ∈∘ smc_Rel α⦇Arr⦈" by (auto intro: smc_cs_intros)
        with T is_arrD(2,3)[OF T] show "T⦇ArrDom⦈ = 0" "T⦇ArrCod⦈ = B"
          by (auto simp: smc_Rel_is_arrD(2,3))
        with 
          T.arr_Rel_ArrVal_vrange 
          T.arr_Rel_ArrVal_vdomain 
          T.ArrVal.vbrelation_vintersection_vdomain
        show "T⦇ArrVal⦈ = 0"
          by auto
      qed
    qed
  qed

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

qed

lemma (in 𝒵) smc_Rel_obj_terminal_obj_initial:
  "obj_initial (smc_Rel α) A ⟷ obj_terminal (smc_Rel α) A"
  unfolding smc_Rel_obj_initial smc_Rel_obj_terminal by simp

lemma (in 𝒵) smc_Rel_obj_null: "obj_null (smc_Rel α) A ⟷ A = 0"
  unfolding obj_null_def smc_Rel_obj_terminal smc_Rel_obj_initial by simp



subsection‹Zero arrow›


text‹
A zero arrow for ‹Rel› is any admissible ‹V›-arrow, such that its value 
is the empty set. A reference for this result is not given, but the 
result is not expected to be original.
›

lemma (in 𝒵) smc_Rel_is_zero_arr: 
  assumes "A ∈∘ smc_Rel α⦇Obj⦈" and "B ∈∘ smc_Rel α⦇Obj⦈"
  shows "T : A ↦0⇘smc_Rel α⇙ B ⟷ T = [0, A, B]∘"
proof(rule HOL.ext iffI)

  interpret Rel: semicategory α ‹smc_Rel α› by (rule semicategory_smc_Rel)
  
  fix T A B assume "T : A ↦0⇘smc_Rel α⇙ B"
  then obtain R S
    where T_def: "T = R ∘A⇘smc_Rel α⇙ S" 
      and S: "S : A ↦⇘smc_Rel α⇙ 0" 
      and R: "R : 0 ↦⇘smc_Rel α⇙ B"
    by (elim is_zero_arrE) (simp add: obj_null_def smc_Rel_obj_terminal)

  interpret S: arr_Rel α S
    rewrites [simp]: "S⦇ArrDom⦈ = A" and [simp]: "S⦇ArrCod⦈ = 0"
    by (intro smc_Rel_is_arrD[OF S])+
  interpret R: arr_Rel α R
    rewrites [simp]: "R⦇ArrDom⦈ = 0" and [simp]: "R⦇ArrCod⦈ = B"
    by (intro smc_Rel_is_arrD[OF R])+

  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_Rel_Comp_app[OF R S] 
     by (rule arr_Rel_eqI[of α], unfold comp_Rel_components)
       (
         auto simp: 
          S_def 
          𝒵_axioms
          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

  assume prems: "T = [0, A, B]∘"
  let ?S = ‹[0, A, 0]∘› and ?R = ‹[0, 0, B]∘›
  have S: "arr_Rel α ?S" and R: "arr_Rel α ?R" 
    by (all‹intro arr_Rel_vfsequenceI›) 
      (auto simp: assms[unfolded smc_Rel_components])
  have SA0: "?S : A ↦⇘smc_Rel α⇙ 0"
    by (intro smc_Rel_is_arrI) (simp_all add: S arr_Rel_components)
  moreover have R0B: "?R : 0 ↦⇘smc_Rel α⇙ B"
    by (intro smc_Rel_is_arrI) (simp_all add: R arr_Rel_components)
  moreover have "T = ?R ∘A⇘smc_Rel α⇙ ?S" 
    unfolding smc_Rel_Comp_app[OF R0B SA0]
  proof(rule arr_Rel_eqI, unfold comp_Rel_components arr_Rel_components prems)
    show "arr_Rel α [0, A, B]∘"
      unfolding prems 
      by (intro arr_Rel_vfsequenceI) 
        (auto simp: assms[unfolded smc_Rel_components(1)])
  qed (use R S in ‹auto simp: smc_Rel_cs_intros›)
  ultimately show "T : A ↦0⇘smc_Rel α⇙ B" 
    by (simp add: is_zero_arrI smc_Rel_obj_null)

qed

text‹\newpage›

end