Theory CZH_SMC_Subsemicategory

(* Copyright 2021 (C) Mihails Milehins *)

section‹Subsemicategory›
theory CZH_SMC_Subsemicategory
  imports 
    CZH_DG_Subdigraph
    CZH_SMC_Semifunctor
begin



subsection‹Background›

named_theorems smc_sub_cs_intros
named_theorems smc_sub_bw_cs_intros
named_theorems smc_sub_fw_cs_intros
named_theorems smc_sub_bw_cs_simps



subsection‹Simple subsemicategory›


subsubsection‹Definition and elementary properties›


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

locale subsemicategory = 
  sdg: semicategory α 𝔅 + dg: semicategory α ℭ for α 𝔅 ℭ + 
  assumes subsmc_subdigraph[slicing_intros]: "smc_dg 𝔅 ⊆⇩D⇩G⇘α⇙ smc_dg ℭ" 
    and subsmc_Comp[smc_sub_fw_cs_intros]: 
      "⟦ g : b ↦⇘𝔅⇙ c; f : a ↦⇘𝔅⇙ b ⟧ ⟹ g ∘⇩A⇘𝔅⇙ f = g ∘⇩A⇘ℭ⇙ f"

abbreviation is_subsemicategory ("(_/ ⊆⇩S⇩M⇩Cı _)" [51, 51] 50)
  where "𝔅 ⊆⇩S⇩M⇩C⇘α⇙ ℭ ≡ subsemicategory α 𝔅 ℭ"

lemmas [smc_sub_fw_cs_intros] = subsemicategory.subsmc_Comp


text‹Rules.›

lemma (in subsemicategory) subsemicategory_axioms'[smc_cs_intros]:
  assumes "α' = α" and "𝔅' = 𝔅"
  shows "𝔅' ⊆⇩S⇩M⇩C⇘α'⇙ ℭ"
  unfolding assms by (rule subsemicategory_axioms)

lemma (in subsemicategory) subsemicategory_axioms''[smc_cs_intros]:
  assumes "α' = α" and "ℭ' = ℭ"
  shows "𝔅 ⊆⇩S⇩M⇩C⇘α'⇙ ℭ'"
  unfolding assms by (rule subsemicategory_axioms)

mk_ide rf subsemicategory_def[unfolded subsemicategory_axioms_def]
  |intro subsemicategoryI|
  |dest subsemicategoryD[dest]|
  |elim subsemicategoryE[elim!]|

lemmas [smc_sub_cs_intros] = subsemicategoryD(1,2)

lemma subsemicategoryI':
  assumes "semicategory α 𝔅"
    and "semicategory α ℭ"
    and "⋀a. a ∈⇩∘ 𝔅⦇Obj⦈ ⟹ a ∈⇩∘ ℭ⦇Obj⦈"
    and "⋀a b f. f : a ↦⇘𝔅⇙ b ⟹ f : a ↦⇘ℭ⇙ b"
    and "⋀b c g a f. ⟦ g : b ↦⇘𝔅⇙ c; f : a ↦⇘𝔅⇙ b ⟧ ⟹
      g ∘⇩A⇘𝔅⇙ f = g ∘⇩A⇘ℭ⇙ f"
  shows "𝔅 ⊆⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔅: semicategory α 𝔅 by (rule assms(1))
  interpret ℭ: semicategory α ℭ by (rule assms(2))  
  show ?thesis
    by 
      (
        intro subsemicategoryI subdigraphI, 
        unfold slicing_simps; 
        (intro 𝔅.smc_digraph ℭ.smc_digraph assms)?
      )
qed


text‹Subsemicategory is a subdigraph.›

context subsemicategory
begin

interpretation subdg: subdigraph α ‹smc_dg 𝔅› ‹smc_dg ℭ›
  by (rule subsmc_subdigraph)

lemmas_with [unfolded slicing_simps]:
  subsmc_Obj_vsubset = subdg.subdg_Obj_vsubset
  and subsmc_is_arr_vsubset = subdg.subdg_is_arr_vsubset
  and subsmc_subdigraph_op_dg_op_dg = subdg.subdg_subdigraph_op_dg_op_dg
  and subsmc_objD = subdg.subdg_objD
  and subsmc_arrD = subdg.subdg_arrD
  and subsmc_dom_simp = subdg.subdg_dom_simp
  and subsmc_cod_simp = subdg.subdg_cod_simp
  and subsmc_is_arrD = subdg.subdg_is_arrD
  and subsmc_dghm_inc_op_dg_is_dghm = subdg.subdg_dghm_inc_op_dg_is_dghm
  and subsmc_op_dg_dghm_inc = subdg.subdg_op_dg_dghm_inc
  and subsmc_inc_is_ft_dghm_axioms = subdg.inc.is_ft_dghm_axioms

end

lemmas subsmc_subdigraph_op_dg_op_dg[intro] = 
  subsemicategory.subsmc_subdigraph_op_dg_op_dg

lemmas [smc_sub_fw_cs_intros] = 
  subsemicategory.subsmc_Obj_vsubset
  subsemicategory.subsmc_is_arr_vsubset
  subsemicategory.subsmc_objD
  subsemicategory.subsmc_arrD
  subsemicategory.subsmc_is_arrD

lemmas [smc_sub_bw_cs_simps] =
  subsemicategory.subsmc_dom_simp
  subsemicategory.subsmc_cod_simp


text‹The opposite subsemicategory.›

lemma (in subsemicategory) subsmc_subsemicategory_op_smc: 
  "op_smc 𝔅 ⊆⇩S⇩M⇩C⇘α⇙ op_smc ℭ"
proof(rule subsemicategoryI)
  fix g b c f a assume prems: "g : b ↦⇘op_smc 𝔅⇙ c" "f : a ↦⇘op_smc 𝔅⇙ b"
  then have "g : c ↦⇘𝔅⇙ b" and "f : b ↦⇘𝔅⇙ a" 
    by (simp_all add: smc_op_simps)
  with subsemicategory_axioms have g: "g : c ↦⇘ℭ⇙ b" and f: "f : b ↦⇘ℭ⇙ a" 
    by (cs_concl cs_shallow cs_intro: smc_sub_fw_cs_intros)+
  from dg.op_smc_Comp[OF this(2,1)] have "g ∘⇩A⇘op_smc ℭ⇙ f = f ∘⇩A⇘ℭ⇙ g".
  with prems show "g ∘⇩A⇘op_smc 𝔅⇙ f = g ∘⇩A⇘op_smc ℭ⇙ f"
    by (simp add: smc_op_simps subsmc_Comp)
qed 
  (
    auto 
      simp:
        smc_op_simps slicing_commute[symmetric] subsmc_subdigraph_op_dg_op_dg
      intro: smc_op_intros
  )

lemmas subsmc_subsemicategory_op_smc[intro, smc_op_intros] = 
  subsemicategory.subsmc_subsemicategory_op_smc


text‹Further rules.›

lemma (in subsemicategory) subsmc_Comp_simp:
  assumes "g : b ↦⇘𝔅⇙ c" and "f : a ↦⇘𝔅⇙ b"
  shows "g ∘⇩A⇘𝔅⇙ f = g ∘⇩A⇘ℭ⇙ f"
  using assms subsmc_Comp by auto

lemmas [smc_sub_bw_cs_simps] = subsemicategory.subsmc_Comp_simp

lemma (in subsemicategory) subsmc_is_idem_arrD: 
  assumes "f : ↦⇩i⇩d⇩e⇘𝔅⇙ b" 
  shows "f : ↦⇩i⇩d⇩e⇘ℭ⇙ b"
  using assms subsemicategory_axioms
  by (intro is_idem_arrI; elim is_idem_arrE)
    (
      cs_concl cs_shallow 
        cs_simp: smc_sub_bw_cs_simps[symmetric] cs_intro: smc_sub_fw_cs_intros
    )

lemmas [smc_sub_fw_cs_intros] = subsemicategory.subsmc_is_idem_arrD


subsubsection‹Subsemicategory relation is a partial order›

lemma subsmc_refl: 
  assumes "semicategory α 𝔄" 
  shows "𝔄 ⊆⇩S⇩M⇩C⇘α⇙ 𝔄"
proof-
  interpret semicategory α 𝔄 by (rule assms)
  show ?thesis 
    by (auto intro: smc_cs_intros slicing_intros subdg_refl subsemicategoryI)
qed

lemma subsmc_trans[trans]: 
  assumes "𝔄 ⊆⇩S⇩M⇩C⇘α⇙ 𝔅" and "𝔅 ⊆⇩S⇩M⇩C⇘α⇙ ℭ"
  shows "𝔄 ⊆⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
  interpret 𝔄𝔅: subsemicategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅ℭ: subsemicategory α 𝔅 ℭ by (rule assms(2))
  show ?thesis 
  proof(rule subsemicategoryI)
    from 𝔄𝔅.subsmc_subdigraph 𝔅ℭ.subsmc_subdigraph 
    show "smc_dg 𝔄 ⊆⇩D⇩G⇘α⇙ smc_dg ℭ" by (meson subdg_trans)
    show "g ∘⇩A⇘𝔄⇙ f = g ∘⇩A⇘ℭ⇙ f" 
      if "g : b ↦⇘𝔄⇙ c" and "f : a ↦⇘𝔄⇙ b" for g b c f a
      by 
        (
          metis 
            that
            𝔄𝔅.subsmc_is_arr_vsubset 
            𝔄𝔅.subsmc_Comp_simp 
            𝔅ℭ.subsmc_Comp_simp
        )
  qed (auto intro: smc_cs_intros)
qed

lemma subsmc_antisym:
  assumes "𝔄 ⊆⇩S⇩M⇩C⇘α⇙ 𝔅" and "𝔅 ⊆⇩S⇩M⇩C⇘α⇙ 𝔄"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄𝔅: subsemicategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅𝔄: subsemicategory α 𝔅 𝔄 by (rule assms(2))
  show ?thesis
  proof(rule smc_eqI)
    from subdg_antisym[OF 𝔄𝔅.subsmc_subdigraph 𝔅𝔄.subsmc_subdigraph] have 
      "smc_dg 𝔄⦇Obj⦈ = smc_dg 𝔅⦇Obj⦈" "smc_dg 𝔄⦇Arr⦈ = smc_dg 𝔅⦇Arr⦈"
      by simp_all
    then show "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" and Arr: "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" 
      unfolding slicing_simps by simp_all
    show "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" 
      by (rule vsv_eqI) (auto simp: smc_cs_simps 𝔄𝔅.subsmc_dom_simp Arr)
    show "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
      by (rule vsv_eqI) (auto simp: smc_cs_simps 𝔅𝔄.subsmc_cod_simp Arr)
    show "𝔄⦇Comp⦈ = 𝔅⦇Comp⦈"
    proof(rule vsv_eqI)
      show "𝒟⇩∘ (𝔄⦇Comp⦈) = 𝒟⇩∘ (𝔅⦇Comp⦈)"
      proof(intro vsubset_antisym vsubsetI)
        fix gf assume "gf ∈⇩∘ 𝒟⇩∘ (𝔄⦇Comp⦈)"
        then obtain g f b c a 
          where gf_def: "gf = [g, f]⇩∘" 
            and g: "g : b ↦⇘𝔄⇙ c" 
            and f: "f : a ↦⇘𝔄⇙ b"
          by (auto simp: 𝔄𝔅.sdg.smc_Comp_vdomain)
        from g f show "gf ∈⇩∘ 𝒟⇩∘ (𝔅⦇Comp⦈)"
          unfolding gf_def by (meson 𝔄𝔅.dg.smc_Comp_vdomainI 𝔄𝔅.subsmc_is_arrD)
      next
        fix gf assume "gf ∈⇩∘ 𝒟⇩∘ (𝔅⦇Comp⦈)"
        then obtain g f b c a 
          where gf_def: "gf = [g, f]⇩∘" 
            and g: "g : b ↦⇘𝔅⇙ c" 
            and f: "f : a ↦⇘𝔅⇙ b"
          by (auto simp: 𝔄𝔅.dg.smc_Comp_vdomain)
        from g f show "gf ∈⇩∘ 𝒟⇩∘ (𝔄⦇Comp⦈)"
          unfolding gf_def by (meson 𝔄𝔅.sdg.smc_Comp_vdomainI 𝔅𝔄.subsmc_is_arrD)
      qed
      show "a ∈⇩∘ 𝒟⇩∘ (𝔄⦇Comp⦈) ⟹ 𝔄⦇Comp⦈⦇a⦈ = 𝔅⦇Comp⦈⦇a⦈" for a
        by (metis 𝔄𝔅.sdg.smc_Comp_vdomain 𝔄𝔅.subsmc_Comp_simp)
    qed auto
  qed (auto intro: smc_cs_intros)
qed



subsection‹Inclusion semifunctor›


subsubsection‹Definition and elementary properties›


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

abbreviation (input) smcf_inc :: "V ⇒ V ⇒ V"
  where "smcf_inc ≡ dghm_inc"


text‹Slicing.›

lemma dghm_smcf_inc[slicing_commute]: 
  "dghm_inc (smc_dg 𝔅) (smc_dg ℭ) = smcf_dghm (smcf_inc 𝔅 ℭ)"
  unfolding 
    smcf_dghm_def dghm_inc_def smc_dg_def dg_field_simps dghm_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Elementary properties.›

lemmas [smc_cs_simps] = 
  dghm_inc_ObjMap_app 
  dghm_inc_ArrMap_app


subsubsection‹Canonical inclusion semifunctor associated with a subsemicategory›

sublocale subsemicategory ⊆ inc: is_ft_semifunctor α 𝔅 ℭ ‹smcf_inc 𝔅 ℭ›
proof(rule is_ft_semifunctorI)
  show "smcf_inc 𝔅 ℭ : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
  proof(rule is_semifunctorI)
    show "vfsequence (dghm_inc 𝔅 ℭ)" unfolding dghm_inc_def by auto
    show "vcard (dghm_inc 𝔅 ℭ) = 4⇩ℕ"
      unfolding dghm_inc_def by (simp add: nat_omega_simps)
    fix g b c f a assume prems: "g : b ↦⇘𝔅⇙ c" "f : a ↦⇘𝔅⇙ b"
    then have "g ∘⇩A⇘𝔅⇙ f : a ↦⇘𝔅⇙ c" by (simp add: smc_cs_intros)
    with subsemicategory_axioms prems have [simp]: 
      "vid_on (𝔅⦇Arr⦈)⦇g ∘⇩A⇘𝔅⇙ f⦈ = g ∘⇩A⇘ℭ⇙ f" 
      by (auto simp: smc_sub_bw_cs_simps)
    from prems show "dghm_inc 𝔅 ℭ⦇ArrMap⦈⦇g ∘⇩A⇘𝔅⇙ f⦈ = 
      dghm_inc 𝔅 ℭ⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ dghm_inc 𝔅 ℭ⦇ArrMap⦈⦇f⦈"
      by 
        (
          cs_concl 
            cs_simp: smc_cs_simps cs_intro: smc_cs_intros smc_sub_fw_cs_intros
        )
  qed 
    (
      insert subsmc_inc_is_ft_dghm_axioms, 
      auto simp: slicing_commute[symmetric] dghm_inc_components smc_cs_intros
    )
qed (auto simp: slicing_commute[symmetric] subsmc_inc_is_ft_dghm_axioms)

lemmas (in subsemicategory) subsmc_smcf_inc_is_ft_semifunctor = 
  inc.is_ft_semifunctor_axioms


subsubsection‹Inclusion semifunctor for the opposite semicategories›

lemma (in subsemicategory) 
  subsemicategory_smcf_inc_op_smc_is_semifunctor[smc_sub_cs_intros]:
  "smcf_inc (op_smc 𝔅) (op_smc ℭ) : op_smc 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_smc ℭ"
  by 
    (
      intro 
        subsemicategory.subsmc_smcf_inc_is_ft_semifunctor
        subsmc_subsemicategory_op_smc
    )

lemmas [smc_sub_cs_intros] = 
  subsemicategory.subsemicategory_smcf_inc_op_smc_is_semifunctor

lemma (in subsemicategory) subdg_op_smc_smcf_inc[smc_op_simps]: 
  "op_smcf (smcf_inc 𝔅 ℭ) = smcf_inc (op_smc 𝔅) (op_smc ℭ)"
  by 
    (
      rule smcf_eqI[of α ‹op_smc 𝔅› ‹op_smc ℭ›], 
      unfold smc_op_simps dghm_inc_components
    )
    (
      auto simp: 
        is_ft_semifunctorD
        subsemicategory_smcf_inc_op_smc_is_semifunctor
        inc.is_semifunctor_op
    )

lemmas [smc_op_simps] = subsemicategory.subdg_op_smc_smcf_inc



subsection‹Full subsemicategory›


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

locale fl_subsemicategory = subsemicategory +
  assumes fl_subsemicategory_fl_subdigraph: "smc_dg 𝔅 ⊆⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ smc_dg ℭ"

abbreviation is_fl_subsemicategory ("(_/ ⊆⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩lı _)" [51, 51] 50)
  where "𝔅 ⊆⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ ≡ fl_subsemicategory α 𝔅 ℭ"


text‹Rules.›

lemma (in fl_subsemicategory) fl_subsemicategory_axioms'[smc_cs_intros]:
  assumes "α' = α" and "𝔅' = 𝔅"
  shows "𝔅' ⊆⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α'⇙ ℭ"
  unfolding assms by (rule fl_subsemicategory_axioms)

lemma (in fl_subsemicategory) fl_subsemicategory_axioms''[smc_cs_intros]:
  assumes "α' = α" and "ℭ' = ℭ"
  shows "𝔅 ⊆⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α'⇙ ℭ'"
  unfolding assms by (rule fl_subsemicategory_axioms)

mk_ide rf fl_subsemicategory_def[unfolded fl_subsemicategory_axioms_def]
  |intro fl_subsemicategoryI|
  |dest fl_subsemicategoryD[dest]|
  |elim fl_subsemicategoryE[elim!]|

lemmas [smc_sub_cs_intros] = fl_subsemicategoryD(1)


text‹Full subsemicategory.›

sublocale fl_subsemicategory ⊆ inc: is_fl_semifunctor α 𝔅 ℭ ‹smcf_inc 𝔅 ℭ›
  using fl_subsemicategory_fl_subdigraph inc.is_semifunctor_axioms
  by (intro is_fl_semifunctorI) (auto simp: slicing_commute[symmetric])



subsection‹Wide subsemicategory›


subsubsection‹Definition and elementary properties›


text‹
See \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/wide+subcategory}
}).
›

locale wide_subsemicategory = subsemicategory +
  assumes wide_subsmc_wide_subdigraph: "smc_dg 𝔅 ⊆⇩D⇩G⇩.⇩w⇩i⇩d⇩e⇘α⇙ smc_dg ℭ"

abbreviation is_wide_subsemicategory ("(_/ ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩eı _)" [51, 51] 50)
  where "𝔅 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ ℭ ≡ wide_subsemicategory α 𝔅 ℭ"


text‹Rules.›

lemma (in wide_subsemicategory) wide_subsemicategory_axioms'[smc_cs_intros]:
  assumes "α' = α" and "𝔅' = 𝔅"
  shows "𝔅' ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α'⇙ ℭ"
  unfolding assms by (rule wide_subsemicategory_axioms)

lemma (in wide_subsemicategory) wide_subsemicategory_axioms''[smc_cs_intros]:
  assumes "α' = α" and "ℭ' = ℭ"
  shows "𝔅 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α'⇙ ℭ'"
  unfolding assms by (rule wide_subsemicategory_axioms)

mk_ide rf wide_subsemicategory_def[unfolded wide_subsemicategory_axioms_def]
  |intro wide_subsemicategoryI|
  |dest wide_subsemicategoryD[dest]|
  |elim wide_subsemicategoryE[elim!]|

lemmas [smc_sub_cs_intros] = wide_subsemicategoryD(1)


text‹Wide subsemicategory is wide subdigraph.›

context wide_subsemicategory
begin

interpretation wide_subdg: wide_subdigraph α ‹smc_dg 𝔅› ‹smc_dg ℭ›
  by (rule wide_subsmc_wide_subdigraph)

lemmas_with [unfolded slicing_simps]:
  wide_subsmc_Obj[dg_sub_bw_cs_intros] = wide_subdg.wide_subdg_Obj
  and wide_subsmc_obj_eq[dg_sub_bw_cs_simps] = wide_subdg.wide_subdg_obj_eq

end

lemmas [dg_sub_bw_cs_intros] = wide_subsemicategory.wide_subsmc_Obj
lemmas [dg_sub_bw_cs_simps] = wide_subsemicategory.wide_subsmc_obj_eq


subsubsection‹The wide subsemicategory relation is a partial order›

lemma wide_subsmc_refl: 
  assumes "semicategory α 𝔄" 
  shows "𝔄 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔄"
proof-
  interpret semicategory α 𝔄 by (rule assms)
  show ?thesis 
    by 
      (
        auto intro: 
          assms
          slicing_intros 
          wide_subdg_refl 
          wide_subsemicategoryI 
          subsmc_refl 
      )
qed

lemma wide_subsmc_trans[trans]:
  assumes "𝔄 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔅" and "𝔅 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ ℭ"
  shows "𝔄 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ ℭ"
proof-
  interpret 𝔄𝔅: wide_subsemicategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅ℭ: wide_subsemicategory α 𝔅 ℭ by (rule assms(2))
  show ?thesis
    by 
      (
        intro 
          wide_subsemicategoryI 
          subsmc_trans[
            OF 𝔄𝔅.subsemicategory_axioms 𝔅ℭ.subsemicategory_axioms
            ], 
        rule wide_subdg_trans, 
        rule 𝔄𝔅.wide_subsmc_wide_subdigraph, 
        rule 𝔅ℭ.wide_subsmc_wide_subdigraph
     )
qed

lemma wide_subsmc_antisym:
  assumes "𝔄 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔅" and "𝔅 ⊆⇩S⇩M⇩C⇩.⇩w⇩i⇩d⇩e⇘α⇙ 𝔄"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄𝔅: wide_subsemicategory α 𝔄 𝔅 by (rule assms(1))
  interpret 𝔅𝔄: wide_subsemicategory α 𝔅 𝔄 by (rule assms(2))
  show ?thesis 
    by 
      (
        rule subsmc_antisym[
          OF 𝔄𝔅.subsemicategory_axioms 𝔅𝔄.subsemicategory_axioms
          ]
      )
qed

text‹\newpage›

end