Theory CZH_SMC_Semicategory

(* Copyright 2021 (C) Mihails Milehins *)

section‹Semicategory›
theory CZH_SMC_Semicategory
  imports 
    CZH_DG_Digraph
    CZH_SMC_Introduction
begin              



subsection‹Background›

lemmas [smc_cs_simps] = dg_shared_cs_simps
lemmas [smc_cs_intros] = dg_shared_cs_intros


subsubsection‹Slicing›


text‹
‹Slicing› is a term that is introduced in this work for the description
of the process of the conversion of more specialized mathematical objects to 
their generalizations. 

The terminology was adapted from the informal imperative
object oriented programming, where the term slicing often refers to the
process of copying an object of a subclass type to an object of a 
superclass type \<^cite>‹"noauthor_wikipedia_2001"›\footnote{
\url{https://en.wikipedia.org/wiki/Object_slicing}
}.
However, it is important to note that the term has other meanings in 
programming and computer science.
›

definition smc_dg :: "V ⇒ V"
  where "smc_dg ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]⇩∘"


text‹Components.›

lemma smc_dg_components[slicing_simps]:
  shows "smc_dg ℭ⦇Obj⦈ = ℭ⦇Obj⦈"
    and "smc_dg ℭ⦇Arr⦈ = ℭ⦇Arr⦈"
    and "smc_dg ℭ⦇Dom⦈ = ℭ⦇Dom⦈"
    and "smc_dg ℭ⦇Cod⦈ = ℭ⦇Cod⦈"
  unfolding smc_dg_def dg_field_simps by (auto simp: nat_omega_simps)


text‹Regular definitions.›

lemma smc_dg_is_arr[slicing_simps]: "f : a ↦⇘smc_dg ℭ⇙ b ⟷ f : a ↦⇘ℭ⇙ b"
  unfolding is_arr_def slicing_simps ..

lemmas [slicing_intros] = smc_dg_is_arr[THEN iffD2]


subsubsection‹Composition and composable arrows›


text‹
The definition of a set of ‹composable_arrs› is equivalent to the definition
of ‹composable pairs› presented on page 10 in \<^cite>‹"mac_lane_categories_2010"›
(see theorem ‹dg_composable_arrs'› below). 
Nonetheless, the definition is meant to be used sparingly. Normally,
the arrows are meant to be specified explicitly using the predicate 
\<^const>‹is_arr›.
›

definition Comp :: V
  where [dg_field_simps]: "Comp = 4⇩ℕ"

abbreviation Comp_app :: "V ⇒ V ⇒ V ⇒ V" (infixl ‹∘⇩Aı› 55)
  where "Comp_app ℭ a b ≡ ℭ⦇Comp⦈⦇a, b⦈⇩∙"

definition composable_arrs :: "V ⇒ V"
  where "composable_arrs ℭ = set 
    {[g, f]⇩∘ | g f. ∃a b c. g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b}"

lemma small_composable_arrs[simp]:
  "small {[g, f]⇩∘ | g f. ∃a b c. g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b}"
proof(intro down[of _ ‹ℭ⦇Arr⦈ ^⇩× 2⇩ℕ›] subsetI)
  fix x assume "x ∈ {[g, f]⇩∘ | g f. ∃a b c. g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b}"
  then obtain g f a b c 
    where x_def: "x = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c"  and "f : a ↦⇘ℭ⇙ b"
    by clarsimp
  with vfsequence_vcpower_two_vpair show "x ∈⇩∘ ℭ⦇Arr⦈ ^⇩× 2⇩ℕ"
    unfolding x_def by auto
qed


text‹Rules.›

lemma composable_arrsI[smc_cs_intros]:
  assumes "gf = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b"
  shows "gf ∈⇩∘ composable_arrs ℭ"
  using assms(2,3) small_composable_arrs 
  unfolding assms(1) composable_arrs_def 
  by auto

lemma composable_arrsE[elim!]:
  assumes "gf ∈⇩∘ composable_arrs ℭ"
  obtains g f a b c where "gf = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b"
  using assms small_composable_arrs unfolding composable_arrs_def by clarsimp

lemma small_composable_arrs'[simp]:
  "small {[g, f]⇩∘ | g f. g ∈⇩∘ ℭ⦇Arr⦈ ∧ f ∈⇩∘ ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈}"
proof(intro down[of _ ‹ℭ⦇Arr⦈ ^⇩× 2⇩ℕ›] subsetI)
  fix gf assume 
    "gf ∈{[g, f]⇩∘ | g f. g ∈⇩∘ ℭ⦇Arr⦈ ∧ f ∈⇩∘ ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈}"
  then obtain g f 
    where gf_def: "gf = [g, f]⇩∘" 
      and "g ∈⇩∘ ℭ⦇Arr⦈" 
      and "f ∈⇩∘ ℭ⦇Arr⦈" 
      and "ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈"
    by clarsimp
  with vfsequence_vcpower_two_vpair show "gf ∈⇩∘ ℭ⦇Arr⦈ ^⇩× 2⇩ℕ"
    unfolding gf_def by auto
qed

lemma dg_composable_arrs':
  "set {[g, f]⇩∘ | g f. g ∈⇩∘ ℭ⦇Arr⦈ ∧ f ∈⇩∘ ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈} = 
    composable_arrs ℭ"
proof-
  have "{[g, f]⇩∘ | g f. g ∈⇩∘ ℭ⦇Arr⦈ ∧ f ∈⇩∘ ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈} = 
    {[g, f]⇩∘ | g f. ∃a b c. g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b}"
  proof(intro subset_antisym subsetI, unfold mem_Collect_eq; elim exE conjE)
    fix gf g f 
    assume gf_def: "gf = [g, f]⇩∘" 
      and "g ∈⇩∘ ℭ⦇Arr⦈"
      and "f ∈⇩∘ ℭ⦇Arr⦈" 
      and gf: "ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈"
    then obtain a b b' c where g: "g : b' ↦⇘ℭ⇙ c" and f: "f : a ↦⇘ℭ⇙ b" 
      by (auto intro!: is_arrI)
    moreover have "b' = b"
      unfolding is_arrD(2,3)[OF g, symmetric] is_arrD(2,3)[OF f, symmetric]
      by (rule gf)
    ultimately have "∃a b c. g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b" by auto
    then show "∃g f. gf = [g, f]⇩∘ ∧ (∃a b c. g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
      unfolding gf_def by auto
  next
    fix gf g f a b c 
    assume gf_def: "gf = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b"
    then have "g ∈⇩∘ ℭ⦇Arr⦈" "f ∈⇩∘ ℭ⦇Arr⦈" "ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈" by auto
    then show 
      "∃g f. gf = [g, f]⇩∘ ∧ g ∈⇩∘ ℭ⦇Arr⦈ ∧ f ∈⇩∘ ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇g⦈ = ℭ⦇Cod⦈⦇f⦈"
      unfolding gf_def by auto
  qed
  then show ?thesis unfolding composable_arrs_def by auto
qed



subsection‹Definition and elementary properties›


text‹
The definition of a semicategory that is used in this work is
similar to the definition that was used in \<^cite>‹"mitchell_dominion_1972"›.
It is also a natural generalization of the definition of a category that is
presented in Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›. The generalization
is performed by omitting the identity and the axioms associated
with it. The amendments to the definitions that are associated with size 
have already been explained in the previous chapter.
›

locale semicategory = 𝒵 α + vfsequence ℭ + Comp: vsv ‹ℭ⦇Comp⦈› for α ℭ +
  assumes smc_length[smc_cs_simps]: "vcard ℭ = 5⇩ℕ"
    and smc_digraph[slicing_intros]: "digraph α (smc_dg ℭ)"
    and smc_Comp_vdomain: "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and smc_Comp_is_arr: 
      "⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and smc_Comp_assoc[smc_cs_simps]:
      "⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
        (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"

lemmas [smc_cs_simps] =
  semicategory.smc_length
  semicategory.smc_Comp_assoc

lemma (in semicategory) smc_Comp_is_arr'[smc_cs_intros]:
  assumes "g : b ↦⇘ℭ⇙ c"
    and "f : a ↦⇘ℭ⇙ b"
    and "ℭ' = ℭ"
  shows "g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ'⇙ c"
  using assms(1,2) unfolding assms(3) by (rule smc_Comp_is_arr)

lemmas [smc_cs_intros] = 
  semicategory.smc_Comp_is_arr'
  semicategory.smc_Comp_is_arr

lemmas [slicing_intros] = semicategory.smc_digraph


text‹Rules.›

lemma (in semicategory) semicategory_axioms'[smc_cs_intros]:
  assumes "α' = α"
  shows "semicategory α' ℭ"
  unfolding assms by (rule semicategory_axioms)

mk_ide rf semicategory_def[unfolded semicategory_axioms_def]
  |intro semicategoryI|
  |dest semicategoryD[dest]|
  |elim semicategoryE[elim]|

lemma semicategoryI':
  assumes "𝒵 α"
    and "vfsequence ℭ"
    and "vsv (ℭ⦇Comp⦈)"
    and "vcard ℭ = 5⇩ℕ"
    and "vsv (ℭ⦇Dom⦈)"
    and "vsv (ℭ⦇Cod⦈)"
    and "𝒟⇩∘ (ℭ⦇Dom⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Dom⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "𝒟⇩∘ (ℭ⦇Cod⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Cod⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "⋀gf. gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and "⋀b c g a f. ⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
        (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom ℭ a b) ∈⇩∘ Vset α"
  shows "semicategory α ℭ"
  by (intro semicategoryI digraphI, unfold slicing_simps)
    (simp_all add: assms  nat_omega_simps smc_dg_def)

lemma semicategoryD':
  assumes "semicategory α ℭ"
  shows "𝒵 α"
    and "vfsequence ℭ"
    and "vsv (ℭ⦇Comp⦈)"
    and "vcard ℭ = 5⇩ℕ"
    and "vsv (ℭ⦇Dom⦈)"
    and "vsv (ℭ⦇Cod⦈)"
    and "𝒟⇩∘ (ℭ⦇Dom⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Dom⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "𝒟⇩∘ (ℭ⦇Cod⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Cod⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "⋀gf. gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and "⋀b c g a f. ⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
        (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom ℭ a b) ∈⇩∘ Vset α"
  by 
    (
      simp_all add: 
        semicategoryD(2-8)[OF assms] 
        digraphD[OF semicategoryD(5)[OF assms], unfolded slicing_simps]
    )

lemma semicategoryE':
  assumes "semicategory α ℭ"
  obtains "𝒵 α"
    and "vfsequence ℭ"
    and "vsv (ℭ⦇Comp⦈)"
    and "vcard ℭ = 5⇩ℕ"
    and "vsv (ℭ⦇Dom⦈)"
    and "vsv (ℭ⦇Cod⦈)"
    and "𝒟⇩∘ (ℭ⦇Dom⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Dom⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "𝒟⇩∘ (ℭ⦇Cod⦈) = ℭ⦇Arr⦈"
    and "ℛ⇩∘ (ℭ⦇Cod⦈) ⊆⇩∘ ℭ⦇Obj⦈"
    and "⋀gf. gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈) ⟷
      (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b)"
    and "⋀b c g a f. ⟦ g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹ g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
    and "⋀c d h b g a f. ⟦ h : c ↦⇘ℭ⇙ d; g : b ↦⇘ℭ⇙ c; f : a ↦⇘ℭ⇙ b ⟧ ⟹
        (h ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f = h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f)"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom ℭ a b) ∈⇩∘ Vset α"
  using assms by (simp add: semicategoryD')


text‹
While using the sublocale infrastructure in conjunction with the rewrite 
morphisms is plausible for achieving automation of slicing, this approach
has certain limitations. For example, the rewrite morphisms cannot be added to a 
given interpretation that was achieved using the
command @{command sublocale}\footnote{
\url{
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-September/msg00074.html
}
}.
Thus, instead of using a partial solution based on the command 
@{command sublocale}, the rewriting is performed manually for 
selected theorems. However, it is hoped that better automation will be provided
in the future.
›

context semicategory
begin

interpretation dg: digraph α ‹smc_dg ℭ› by (rule smc_digraph)

sublocale Dom: vsv ‹ℭ⦇Dom⦈› by (rule dg.Dom.vsv_axioms[unfolded slicing_simps])
sublocale Cod: vsv ‹ℭ⦇Cod⦈› by (rule dg.Cod.vsv_axioms[unfolded slicing_simps])

lemmas_with [unfolded slicing_simps]:
  smc_Dom_vdomain[smc_cs_simps] = dg.dg_Dom_vdomain
  and smc_Dom_vrange = dg.dg_Dom_vrange
  and smc_Cod_vdomain[smc_cs_simps] = dg.dg_Cod_vdomain
  and smc_Cod_vrange = dg.dg_Cod_vrange
  and smc_Obj_vsubset_Vset = dg.dg_Obj_vsubset_Vset
  and smc_Hom_vifunion_in_Vset[smc_cs_intros] = dg.dg_Hom_vifunion_in_Vset
  and smc_Obj_if_Dom_vrange = dg.dg_Obj_if_Dom_vrange
  and smc_Obj_if_Cod_vrange = dg.dg_Obj_if_Cod_vrange
  and smc_is_arrD = dg.dg_is_arrD
  and smc_is_arrE[elim] = dg.dg_is_arrE
  and smc_in_ArrE[elim] = dg.dg_in_ArrE
  and smc_Hom_in_Vset[smc_cs_intros] = dg.dg_Hom_in_Vset
  and smc_Arr_vsubset_Vset = dg.dg_Arr_vsubset_Vset
  and smc_Dom_vsubset_Vset = dg.dg_Dom_vsubset_Vset
  and smc_Cod_vsubset_Vset = dg.dg_Cod_vsubset_Vset
  and smc_Obj_in_Vset = dg.dg_Obj_in_Vset
  and smc_in_Obj_in_Vset[smc_cs_intros] = dg.dg_in_Obj_in_Vset
  and smc_Arr_in_Vset = dg.dg_Arr_in_Vset
  and smc_in_Arr_in_Vset[smc_cs_intros] = dg.dg_in_Arr_in_Vset
  and smc_Dom_in_Vset = dg.dg_Dom_in_Vset
  and smc_Cod_in_Vset = dg.dg_Cod_in_Vset
  and smc_digraph_if_ge_Limit = dg.dg_digraph_if_ge_Limit
  and smc_Dom_app_in_Obj = dg.dg_Dom_app_in_Obj
  and smc_Cod_app_in_Obj = dg.dg_Cod_app_in_Obj
  and smc_Arr_vempty_if_Obj_vempty = dg.dg_Arr_vempty_if_Obj_vempty
  and smc_Dom_vempty_if_Arr_vempty = dg.dg_Dom_vempty_if_Arr_vempty
  and smc_Cod_vempty_if_Arr_vempty = dg.dg_Cod_vempty_if_Arr_vempty

end

lemmas [smc_cs_intros] =
  semicategory.smc_is_arrD(1-3)
  semicategory.smc_Hom_in_Vset


text‹Elementary properties.›

lemma smc_eqI:
  assumes "semicategory α 𝔄" 
    and "semicategory α 𝔅"
    and "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈"
    and "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈"
    and "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈"
    and "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
    and "𝔄⦇Comp⦈ = 𝔅⦇Comp⦈"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄: semicategory α 𝔄 by (rule assms(1))
  interpret 𝔅: semicategory α 𝔅 by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟⇩∘ 𝔄 = 5⇩ℕ" 
      by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
    show "𝒟⇩∘ 𝔄 = 𝒟⇩∘ 𝔅" 
      by (cs_concl cs_shallow cs_simp: dom smc_cs_simps V_cs_simps)
    show "a ∈⇩∘ 𝒟⇩∘ 𝔄 ⟹ 𝔄⦇a⦈ = 𝔅⦇a⦈" for a 
      by (unfold dom, elim_in_numeral, insert assms) (auto simp: dg_field_simps)
  qed auto
qed

lemma smc_dg_eqI:
  assumes "semicategory α 𝔄"
    and "semicategory α 𝔅"
    and "𝔄⦇Comp⦈ = 𝔅⦇Comp⦈"
    and "smc_dg 𝔄 = smc_dg 𝔅"
  shows "𝔄 = 𝔅"
proof(rule smc_eqI)
  from assms(4) have 
    "smc_dg 𝔄⦇Obj⦈ = smc_dg 𝔅⦇Obj⦈"
    "smc_dg 𝔄⦇Arr⦈ = smc_dg 𝔅⦇Arr⦈"
    "smc_dg 𝔄⦇Dom⦈ = smc_dg 𝔅⦇Dom⦈"
    "smc_dg 𝔄⦇Cod⦈ = smc_dg 𝔅⦇Cod⦈" 
    by auto
  then show
    "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
    unfolding slicing_simps by simp_all
qed (auto intro: assms)

lemma (in semicategory) smc_def: "ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈, ℭ⦇Comp⦈]⇩∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ ℭ = 5⇩ℕ" 
    by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
  have dom_rhs: "𝒟⇩∘ [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈, ℭ⦇Comp⦈]⇩∘ = 5⇩ℕ"
    by (simp add: nat_omega_simps)
  then show "𝒟⇩∘ ℭ = 𝒟⇩∘ [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈, ℭ⦇Comp⦈]⇩∘"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ ℭ ⟹ ℭ⦇a⦈ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈, ℭ⦇Comp⦈]⇩∘⦇a⦈" 
    for a
    unfolding dom_lhs
    by elim_in_numeral (simp_all add: dg_field_simps nat_omega_simps)
qed auto

lemma (in semicategory) smc_Comp_vdomainI[smc_cs_intros]: 
  assumes "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" and "gf = [g, f]⇩∘"
  shows "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈)"
  using assms by (intro smc_Comp_vdomain[THEN iffD2]) auto

lemmas [smc_cs_intros] = semicategory.smc_Comp_vdomainI

lemma (in semicategory) smc_Comp_vdomainE[elim!]: 
  assumes "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈)" 
  obtains g f a b c where "gf = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b"
proof-
  from smc_Comp_vdomain[THEN iffD1, OF assms(1)] obtain g f b c a
    where "gf = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b"
    by clarsimp
  with that show ?thesis by simp
qed

lemma (in semicategory) smc_Comp_vdomain_is_composable_arrs: 
  "𝒟⇩∘ (ℭ⦇Comp⦈) = composable_arrs ℭ"
  by (intro vsubset_antisym vsubsetI) (auto intro!: smc_cs_intros)+

lemma (in semicategory) smc_Comp_vrange: "ℛ⇩∘ (ℭ⦇Comp⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof(rule Comp.vsv_vrange_vsubset)
  fix gf assume "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈)"
  from smc_Comp_vdomain[THEN iffD1, OF this] obtain g f b c a
    where gf_def: "gf = [g, f]⇩∘" 
      and g: "g : b ↦⇘ℭ⇙ c" 
      and f: "f : a ↦⇘ℭ⇙ b"  
    by clarsimp
  from semicategory_axioms g f show "ℭ⦇Comp⦈⦇gf⦈ ∈⇩∘ ℭ⦇Arr⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: gf_def smc_cs_simps cs_intro: smc_cs_intros
      )
qed

sublocale semicategory ⊆ Comp: pbinop ‹ℭ⦇Arr⦈› ‹ℭ⦇Comp⦈›
proof unfold_locales
  show "𝒟⇩∘ (ℭ⦇Comp⦈) ⊆⇩∘ ℭ⦇Arr⦈ ^⇩× 2⇩ℕ"
  proof(intro vsubsetI; unfold smc_Comp_vdomain)
    fix gf assume "∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘ℭ⇙ c ∧ f : a ↦⇘ℭ⇙ b"
    then obtain a b c g f 
      where x_def: "gf = [g, f]⇩∘" and "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b"
      by auto
    then have "g ∈⇩∘ ℭ⦇Arr⦈" "f ∈⇩∘ ℭ⦇Arr⦈" by auto
    then show "gf ∈⇩∘ ℭ⦇Arr⦈ ^⇩× 2⇩ℕ" 
      unfolding x_def by (auto simp: nat_omega_simps)
  qed
  show "ℛ⇩∘ (ℭ⦇Comp⦈) ⊆⇩∘ ℭ⦇Arr⦈" by (rule smc_Comp_vrange)
qed auto


text‹Size.›

lemma (in semicategory) smc_Comp_vsubset_Vset: "ℭ⦇Comp⦈ ⊆⇩∘ Vset α"
proof(intro vsubsetI)
  fix gfh assume "gfh ∈⇩∘ ℭ⦇Comp⦈"
  then obtain gf h 
    where gfh_def: "gfh = ⟨gf, h⟩" 
      and gf: "gf ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈)" 
      and h: "h ∈⇩∘ ℛ⇩∘ (ℭ⦇Comp⦈)"
    by (blast elim: Comp.vbrelation_vinE)
  from gf obtain g f a b c
    where gf_def: "gf = [g, f]⇩∘" and g: "g : b ↦⇘ℭ⇙ c" and f: "f : a ↦⇘ℭ⇙ b"  
    by clarsimp
  from h smc_Comp_vrange have "h ∈⇩∘ ℭ⦇Arr⦈" by auto
  with g f show "gfh ∈⇩∘ Vset α"
    unfolding gfh_def gf_def 
    by (cs_concl cs_shallow cs_intro: smc_cs_intros V_cs_intros)
qed

lemma (in semicategory) smc_semicategory_in_Vset_4: "ℭ ∈⇩∘ Vset (α + 4⇩ℕ)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], smc_cs_intros] =
    smc_Obj_vsubset_Vset
    smc_Arr_vsubset_Vset
    smc_Dom_vsubset_Vset
    smc_Cod_vsubset_Vset
    smc_Comp_vsubset_Vset
  show ?thesis
    by (subst smc_def, succ_of_numeral)
      (
        cs_concl  
          cs_simp: plus_V_succ_right V_cs_simps 
          cs_intro: smc_cs_intros V_cs_intros
      )
qed

lemma (in semicategory) smc_Comp_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "ℭ⦇Comp⦈ ∈⇩∘ Vset β"
  using smc_Comp_vsubset_Vset by (meson Vset_in_mono assms(2) vsubset_in_VsetI)

lemma (in semicategory) smc_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "ℭ ∈⇩∘ Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [smc_cs_intros] = 
    smc_Obj_in_Vset 
    smc_Arr_in_Vset
    smc_Dom_in_Vset
    smc_Cod_in_Vset
    smc_Comp_in_Vset
  from assms(2) show ?thesis 
    by (subst smc_def) (cs_concl cs_shallow cs_intro: smc_cs_intros V_cs_intros)
qed

lemma (in semicategory) smc_semicategory_if_ge_Limit:
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "semicategory β ℭ"
  by (rule semicategoryI)
    (
      auto 
        intro: smc_cs_intros 
        simp: smc_cs_simps assms vfsequence_axioms smc_digraph_if_ge_Limit 
    )

lemma small_semicategory[simp]: "small {ℭ. semicategory α ℭ}"
proof(cases ‹𝒵 α›)
  case True
  from semicategory.smc_in_Vset[of α] show ?thesis
    by (intro down[of _ ‹Vset (α + ω)›]) 
      (auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{ℭ. semicategory α ℭ} = {}" by auto
  then show ?thesis by simp
qed

lemma (in 𝒵) semicategories_in_Vset: 
  assumes "𝒵 β" and "α ∈⇩∘ β"
  shows "set {ℭ. semicategory α ℭ} ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "set {ℭ. semicategory α ℭ} ⊆⇩∘ Vset (α + 4⇩ℕ)"
  proof(intro vsubsetI)
    fix ℭ assume prems: "ℭ ∈⇩∘ set {ℭ. semicategory α ℭ}"
    interpret semicategory α ℭ using prems by simp
    show "ℭ ∈⇩∘ Vset (α + 4⇩ℕ)"
      unfolding VPow_iff by (rule smc_semicategory_in_Vset_4)
  qed
  from assms(2) show "Vset (α + 4⇩ℕ) ∈⇩∘ Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma semicategory_if_semicategory:
  assumes "semicategory β ℭ"
    and "𝒵 α"
    and "ℭ⦇Obj⦈ ⊆⇩∘ Vset α"
    and "⋀A B. ⟦ A ⊆⇩∘ ℭ⦇Obj⦈; B ⊆⇩∘ ℭ⦇Obj⦈; A ∈⇩∘ Vset α; B ∈⇩∘ Vset α ⟧ ⟹
      (⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom ℭ a b) ∈⇩∘ Vset α"
  shows "semicategory α ℭ"
proof-
  interpret semicategory β ℭ by (rule assms(1))
  interpret α: 𝒵 α by (rule assms(2))
  show ?thesis
  proof(intro semicategoryI)
    show "vfsequence ℭ" by (simp add: vfsequence_axioms)
    show "digraph α (smc_dg ℭ)"
      by (rule digraph_if_digraph, unfold slicing_simps)
        (auto intro!: assms(1,3,4) slicing_intros)
  qed (auto intro: smc_cs_intros simp: smc_cs_simps)
qed


text‹Further properties.›

lemma (in semicategory) smc_Comp_vempty_if_Arr_vempty:
  assumes "ℭ⦇Arr⦈ = 0"
  shows "ℭ⦇Comp⦈ = 0"
  using assms smc_Comp_vrange by (auto intro: Comp.vsv_vrange_vempty)



subsection‹Opposite semicategory›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.›

definition op_smc :: "V ⇒ V"
  where "op_smc ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Cod⦈, ℭ⦇Dom⦈, fflip (ℭ⦇Comp⦈)]⇩∘"


text‹Components.›

lemma op_smc_components:
  shows [smc_op_simps]: "op_smc ℭ⦇Obj⦈ = ℭ⦇Obj⦈"
    and [smc_op_simps]: "op_smc ℭ⦇Arr⦈ = ℭ⦇Arr⦈"
    and [smc_op_simps]: "op_smc ℭ⦇Dom⦈ = ℭ⦇Cod⦈"
    and [smc_op_simps]: "op_smc ℭ⦇Cod⦈ = ℭ⦇Dom⦈"
    and "op_smc ℭ⦇Comp⦈ = fflip (ℭ⦇Comp⦈)"
  unfolding op_smc_def dg_field_simps by (auto simp: nat_omega_simps)

lemma op_smc_component_intros[smc_op_intros]:
  shows "a ∈⇩∘ ℭ⦇Obj⦈ ⟹ a ∈⇩∘ op_smc ℭ⦇Obj⦈"
    and "f ∈⇩∘ ℭ⦇Arr⦈ ⟹ f ∈⇩∘ op_smc ℭ⦇Arr⦈"
  unfolding smc_op_simps by simp_all


text‹Slicing.›

lemma op_dg_smc_dg[slicing_commute]: "op_dg (smc_dg ℭ) = smc_dg (op_smc ℭ)"
  unfolding smc_dg_def op_smc_def op_dg_def dg_field_simps
  by (simp add: nat_omega_simps)


text‹Regular definitions.›

lemma op_smc_Comp_vdomain[smc_op_simps]: 
  "𝒟⇩∘ (op_smc ℭ⦇Comp⦈) = (𝒟⇩∘ (ℭ⦇Comp⦈))¯⇩∙"
  unfolding op_smc_components by simp

lemma op_smc_is_arr[smc_op_simps]: "f : b ↦⇘op_smc ℭ⇙ a ⟷ f : a ↦⇘ℭ⇙ b"
  unfolding smc_op_simps is_arr_def by auto

lemmas [smc_op_intros] = op_smc_is_arr[THEN iffD2]

lemma (in semicategory) op_smc_Comp_vrange[smc_op_simps]: 
  "ℛ⇩∘ (op_smc ℭ⦇Comp⦈) = ℛ⇩∘ (ℭ⦇Comp⦈)"
  using Comp.vrange_fflip unfolding op_smc_components by simp

lemmas [smc_op_simps] = semicategory.op_smc_Comp_vrange

lemma (in semicategory) op_smc_Comp[smc_op_simps]: 
  assumes "f : b ↦⇘ℭ⇙ c" and "g : a ↦⇘ℭ⇙ b"
  shows "g ∘⇩A⇘op_smc ℭ⇙ f = f ∘⇩A⇘ℭ⇙ g"
  using assms 
  unfolding op_smc_components 
  by (auto intro!: fflip_app smc_cs_intros)

lemmas [smc_op_simps] = semicategory.op_smc_Comp

lemma op_smc_Hom[smc_op_simps]: "Hom (op_smc ℭ) a b = Hom ℭ b a"
  unfolding smc_op_simps by simp


subsubsection‹Further properties›

lemma (in semicategory) semicategory_op[smc_op_intros]: 
  "semicategory α (op_smc ℭ)"
proof(intro semicategoryI)
  from semicategory_axioms smc_digraph show "digraph α (smc_dg (op_smc ℭ))"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: slicing_commute[symmetric] cs_intro: dg_op_intros
      )
  show "vfsequence (op_smc ℭ)" unfolding op_smc_def by simp
  show "vcard (op_smc ℭ) = 5⇩ℕ"
    unfolding op_smc_def by (simp add: nat_omega_simps)
  show "(gf ∈⇩∘ 𝒟⇩∘ (op_smc ℭ⦇Comp⦈)) ⟷
    (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘op_smc ℭ⇙ c ∧ f : a ↦⇘op_smc ℭ⇙ b)"
    for gf
  proof(rule iffI; unfold smc_op_simps)
    assume prems: "gf ∈⇩∘ (𝒟⇩∘ (ℭ⦇Comp⦈))¯⇩∙"
    then obtain g' f' where gf_def: "gf = [g', f']⇩∘" by clarsimp
    with prems have "[f', g']⇩∘ ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈)" by (auto intro: smc_cs_intros)
    with smc_Comp_vdomain show 
      "∃g f b c a. gf = [g, f]⇩∘ ∧ g : c ↦⇘ℭ⇙ b ∧ f : b ↦⇘ℭ⇙ a"
      unfolding gf_def by auto
  next
    assume "∃g f b c a. gf = [g, f]⇩∘ ∧ g : c ↦⇘ℭ⇙ b ∧ f : b ↦⇘ℭ⇙ a"
    then obtain g f b c a 
      where gf_def: "gf = [g, f]⇩∘" and g: "g : c ↦⇘ℭ⇙ b" and f: "f : b ↦⇘ℭ⇙ a"
      by clarsimp
    then have "g ∈⇩∘ ℭ⦇Arr⦈" and "f ∈⇩∘ ℭ⦇Arr⦈" by force+
    from g f have "[f, g]⇩∘ ∈⇩∘ 𝒟⇩∘ (ℭ⦇Comp⦈)"
      unfolding gf_def by (intro smc_Comp_vdomainI) auto
    then show "gf ∈⇩∘ (𝒟⇩∘ (ℭ⦇Comp⦈))¯⇩∙" 
      unfolding gf_def by (auto intro: smc_cs_intros)
  qed
  from semicategory_axioms show 
    "⟦ g : b ↦⇘op_smc ℭ⇙ c; f : a ↦⇘op_smc ℭ⇙ b ⟧ ⟹ 
      g ∘⇩A⇘op_smc ℭ⇙ f : a ↦⇘op_smc ℭ⇙ c"
    for g b c f a
    unfolding smc_op_simps 
    by (cs_concl cs_shallow cs_simp: smc_op_simps cs_intro: smc_cs_intros)
  fix h c d g b f a
  assume "h : c ↦⇘op_smc ℭ⇙ d" "g : b ↦⇘op_smc ℭ⇙ c" "f : a ↦⇘op_smc ℭ⇙ b"
  with semicategory_axioms show
    "(h ∘⇩A⇘op_smc ℭ⇙ g) ∘⇩A⇘op_smc ℭ⇙ f = h ∘⇩A⇘op_smc ℭ⇙ (g ∘⇩A⇘op_smc ℭ⇙ f)"
    unfolding smc_op_simps
    by (cs_concl cs_simp: smc_op_simps smc_cs_simps cs_intro: smc_cs_intros)
qed (auto simp: fflip_vsv op_smc_components(5))

lemmas semicategory_op[smc_op_intros] = semicategory.semicategory_op

lemma (in semicategory) smc_op_smc_op_smc[smc_op_simps]: "op_smc (op_smc ℭ) = ℭ"
  by (rule smc_eqI, unfold smc_op_simps op_smc_components)
    (
      auto simp: 
        Comp.pbinop_fflip_fflip 
        semicategory_axioms
        semicategory.semicategory_op semicategory_op
        intro: smc_cs_intros
    )

lemmas smc_op_smc_op_smc[smc_op_simps] = semicategory.smc_op_smc_op_smc

lemma eq_op_smc_iff[smc_op_simps]: 
  assumes "semicategory α 𝔄" and "semicategory α 𝔅"
  shows "op_smc 𝔄 = op_smc 𝔅 ⟷ 𝔄 = 𝔅"
proof
  interpret 𝔄: semicategory α 𝔄 by (rule assms(1))
  interpret 𝔅: semicategory α 𝔅 by (rule assms(2))
  assume prems: "op_smc 𝔄 = op_smc 𝔅" show "𝔄 = 𝔅"
  proof(rule smc_eqI)
    show 
      "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" 
      "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈"
      "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" 
      "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
      "𝔄⦇Comp⦈ = 𝔅⦇Comp⦈"
      by (metis prems 𝔄.smc_op_smc_op_smc 𝔅.smc_op_smc_op_smc)+
  qed (auto intro: assms)
qed auto



subsection‹Arrow with a domain and a codomain›

lemma (in semicategory) smc_assoc_helper:
  assumes "f : a ↦⇘ℭ⇙ b"
    and "g : b ↦⇘ℭ⇙ c"
    and "h : c ↦⇘ℭ⇙ d"
    and "h ∘⇩A⇘ℭ⇙ g = q"
  shows "h ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f) = q ∘⇩A⇘ℭ⇙ f"
  using semicategory_axioms assms(1-4)
  by (cs_concl cs_simp: assms(4) semicategory.smc_Comp_assoc[symmetric])

lemma (in semicategory) smc_pattern_rectangle_right:
  assumes "aa' : a ↦⇘ℭ⇙ a'" 
    and "a'a'' : a' ↦⇘ℭ⇙ a''"
    and "a''b'' : a'' ↦⇘ℭ⇙ b''"
    and "ab : a ↦⇘ℭ⇙ b"
    and "bb' : b ↦⇘ℭ⇙ b'"
    and "b'b'' : b' ↦⇘ℭ⇙ b''"
    and "a'b' : a' ↦⇘ℭ⇙ b'"
    and "a'b' ∘⇩A⇘ℭ⇙ aa' = bb' ∘⇩A⇘ℭ⇙ ab"
    and "b'b'' ∘⇩A⇘ℭ⇙ a'b' = a''b'' ∘⇩A⇘ℭ⇙ a'a''"
  shows "a''b'' ∘⇩A⇘ℭ⇙ (a'a'' ∘⇩A⇘ℭ⇙ aa') = (b'b'' ∘⇩A⇘ℭ⇙ bb') ∘⇩A⇘ℭ⇙ ab"
proof-
  from semicategory_axioms assms(3,2,1) have 
    "a''b'' ∘⇩A⇘ℭ⇙ (a'a'' ∘⇩A⇘ℭ⇙ aa') = (a''b'' ∘⇩A⇘ℭ⇙ a'a'') ∘⇩A⇘ℭ⇙ aa'"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  also have "… = (b'b'' ∘⇩A⇘ℭ⇙ a'b') ∘⇩A⇘ℭ⇙ aa'" unfolding assms(9) ..
  also from semicategory_axioms assms(1,6,7) have 
    "… = b'b'' ∘⇩A⇘ℭ⇙ (a'b' ∘⇩A⇘ℭ⇙ aa')"
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  also have "… = b'b'' ∘⇩A⇘ℭ⇙ (bb' ∘⇩A⇘ℭ⇙ ab)" unfolding assms(8) ..
  also from semicategory_axioms assms(6,5,4) have 
    "… = (b'b'' ∘⇩A⇘ℭ⇙ bb') ∘⇩A⇘ℭ⇙ ab" 
    by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
  finally show ?thesis by simp
qed

lemmas (in semicategory) smc_pattern_rectangle_left = 
  smc_pattern_rectangle_right[symmetric]



subsection‹Monic arrow and epic arrow›


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

definition is_monic_arr :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_monic_arr ℭ b c m ⟷
    m : b ↦⇘ℭ⇙ c ∧
    (
      ∀f g a.
        f : a ↦⇘ℭ⇙ b ⟶ g : a ↦⇘ℭ⇙ b ⟶ m ∘⇩A⇘ℭ⇙ f = m ∘⇩A⇘ℭ⇙ g ⟶ f = g
    )"

syntax "_is_monic_arr" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹_ : _ ↦⇩m⇩o⇩nı _› [51, 51, 51] 51)
syntax_consts "_is_monic_arr" ⇌ is_monic_arr
translations "m : b ↦⇩m⇩o⇩n⇘ℭ⇙ c" ⇌ "CONST is_monic_arr ℭ b c m"

definition is_epic_arr :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_epic_arr ℭ a b e ≡ e : b ↦⇩m⇩o⇩n⇘op_smc ℭ⇙ a"

syntax "_is_epic_arr" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹_ : _ ↦⇩e⇩p⇩iı _› [51, 51, 51] 51)
syntax_consts "_is_epic_arr" ⇌ is_epic_arr
translations "e : a ↦⇩e⇩p⇩i⇘ℭ⇙ b" ⇌ "CONST is_epic_arr ℭ a b e"


text‹Rules.›

mk_ide rf is_monic_arr_def
  |intro is_monic_arrI|
  |dest is_monic_arrD[dest]|
  |elim is_monic_arrE[elim!]|

lemmas [smc_arrow_cs_intros] = is_monic_arrD(1)

lemma (in semicategory) is_epic_arrI:
  assumes "e : a ↦⇘ℭ⇙ b"
    and "⋀f g c. ⟦ f : b ↦⇘ℭ⇙ c; g : b ↦⇘ℭ⇙ c; f ∘⇩A⇘ℭ⇙ e = g ∘⇩A⇘ℭ⇙ e ⟧ ⟹
      f = g"
  shows "e : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  unfolding is_epic_arr_def
proof(intro is_monic_arrI, unfold smc_op_simps)
  fix f g a 
  assume prems:
    "f : b ↦⇘ℭ⇙ a" "g : b ↦⇘ℭ⇙ a" "e ∘⇩A⇘op_smc ℭ⇙ f = e ∘⇩A⇘op_smc ℭ⇙ g"
  show "f = g"
  proof-
    from prems(3,1,2) assms(1) semicategory_axioms have "g ∘⇩A⇘ℭ⇙ e = f ∘⇩A⇘ℭ⇙ e"
      by 
        (
          cs_prems cs_shallow
            cs_simp: smc_cs_simps smc_op_simps
            cs_intro: smc_cs_intros smc_op_intros
        )
      simp
    from assms(2)[OF prems(2,1) this] show ?thesis ..
  qed
qed (rule assms(1))

lemma is_epic_arr_is_arr[smc_arrow_cs_intros, dest]:
  assumes "e : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  shows "e : a ↦⇘ℭ⇙ b"
  using assms unfolding is_epic_arr_def is_monic_arr_def smc_op_simps by simp

lemma (in semicategory) is_epic_arrD[dest]:
  assumes "e : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  shows "e : a ↦⇘ℭ⇙ b"
    and "⋀f g c. ⟦ f : b ↦⇘ℭ⇙ c; g : b ↦⇘ℭ⇙ c; f ∘⇩A⇘ℭ⇙ e = g ∘⇩A⇘ℭ⇙ e ⟧ ⟹
      f = g"
proof-
  note is_monic_arrD = 
    assms(1)[unfolded is_epic_arr_def is_monic_arr_def smc_op_simps] 
  from is_monic_arrD[THEN conjunct1] show e: "e : a ↦⇘ℭ⇙ b" by simp
  fix f g c 
  assume prems: "f : b ↦⇘ℭ⇙ c" "g : b ↦⇘ℭ⇙ c" "f ∘⇩A⇘ℭ⇙ e = g ∘⇩A⇘ℭ⇙ e"
  with semicategory_axioms e have "e ∘⇩A⇘op_smc ℭ⇙ f = e ∘⇩A⇘op_smc ℭ⇙ g"
    by (cs_concl cs_shallow cs_simp: smc_op_simps cs_intro: smc_cs_intros)
  then show "f = g" 
    by (rule is_monic_arrD[THEN conjunct2, rule_format, OF prems(1,2)])
qed

lemma (in semicategory) is_epic_arrE[elim!]:
  assumes "e : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  obtains "e : a ↦⇘ℭ⇙ b"
    and "⋀f g c. ⟦ f : b ↦⇘ℭ⇙ c; g : b ↦⇘ℭ⇙ c; f ∘⇩A⇘ℭ⇙ e = g ∘⇩A⇘ℭ⇙ e ⟧ ⟹ 
      f = g"
  using assms by auto


text‹Elementary properties.›

lemma (in semicategory) op_smc_is_epic_arr[smc_op_simps]: 
  "f : b ↦⇩e⇩p⇩i⇘op_smc ℭ⇙ a ⟷ f : a ↦⇩m⇩o⇩n⇘ℭ⇙ b"
  unfolding is_monic_arr_def is_epic_arr_def smc_op_simps ..

lemma (in semicategory) op_smc_is_monic_arr[smc_op_simps]: 
  "f : b ↦⇩m⇩o⇩n⇘op_smc ℭ⇙ a ⟷ f : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  unfolding is_monic_arr_def is_epic_arr_def smc_op_simps ..

lemma (in semicategory) smc_Comp_is_monic_arr[smc_arrow_cs_intros]:
  assumes "g : b ↦⇩m⇩o⇩n⇘ℭ⇙ c" and "f : a ↦⇩m⇩o⇩n⇘ℭ⇙ b"
  shows "g ∘⇩A⇘ℭ⇙ f : a ↦⇩m⇩o⇩n⇘ℭ⇙ c"
proof(intro is_monic_arrI)
  from assms show "g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c" by (auto intro: smc_cs_intros)
  fix f' g' a'
  assume f': "f' : a' ↦⇘ℭ⇙ a"
    and g': "g' : a' ↦⇘ℭ⇙ a"
    and "g ∘⇩A⇘ℭ⇙ f ∘⇩A⇘ℭ⇙ f' = g ∘⇩A⇘ℭ⇙ f ∘⇩A⇘ℭ⇙ g'"
  with assms have "g ∘⇩A⇘ℭ⇙ (f ∘⇩A⇘ℭ⇙ f') = g ∘⇩A⇘ℭ⇙ (f ∘⇩A⇘ℭ⇙ g')"
    by (force simp: smc_Comp_assoc)
  moreover from assms have "f ∘⇩A⇘ℭ⇙ f' : a' ↦⇘ℭ⇙ b" "f ∘⇩A⇘ℭ⇙ g' : a' ↦⇘ℭ⇙ b" 
    by (auto intro: f' g' smc_cs_intros)
  ultimately have "f ∘⇩A⇘ℭ⇙ f' = f ∘⇩A⇘ℭ⇙ g'" using assms(1) by clarsimp
  with assms f' g' show "f' = g'" by clarsimp
qed

lemmas [smc_arrow_cs_intros] = semicategory.smc_Comp_is_monic_arr

lemma (in semicategory) smc_Comp_is_epic_arr[smc_arrow_cs_intros]: 
  assumes "g : b ↦⇩e⇩p⇩i⇘ℭ⇙ c" and "f : a ↦⇩e⇩p⇩i⇘ℭ⇙ b"
  shows "g ∘⇩A⇘ℭ⇙ f : a ↦⇩e⇩p⇩i⇘ℭ⇙ c"
proof-
  from assms op_smc_is_arr have "g : b ↦⇘ℭ⇙ c" "f : a ↦⇘ℭ⇙ b" 
    unfolding is_epic_arr_def by auto
  with semicategory_axioms have "f ∘⇩A⇘op_smc ℭ⇙ g = g ∘⇩A⇘ℭ⇙ f"
    by (cs_concl cs_shallow cs_simp: smc_op_simps)
  with 
    semicategory.smc_Comp_is_monic_arr[
      OF semicategory_op,
      OF assms(2,1)[unfolded is_epic_arr_def],
      folded is_epic_arr_def
      ]
  show ?thesis    
    by auto
qed

lemmas [smc_arrow_cs_intros] = semicategory.smc_Comp_is_epic_arr

lemma (in semicategory) smc_Comp_is_monic_arr_is_monic_arr:
  assumes "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" and "g ∘⇩A⇘ℭ⇙ f : a ↦⇩m⇩o⇩n⇘ℭ⇙ c"
  shows "f : a ↦⇩m⇩o⇩n⇘ℭ⇙ b"
proof(intro is_monic_arrI)
  fix f' g' a'
  assume f': "f' : a' ↦⇘ℭ⇙ a" 
    and g': "g' : a' ↦⇘ℭ⇙ a" 
    and f'gg'g: "f ∘⇩A⇘ℭ⇙ f' = f ∘⇩A⇘ℭ⇙ g'"
  from assms(1,2) f' g' have "(g ∘⇩A⇘ℭ⇙ f) ∘⇩A⇘ℭ⇙ f' = (g ∘⇩A⇘ℭ⇙ f) ∘⇩A⇘ℭ⇙ g'"
    by (auto simp: smc_Comp_assoc f'gg'g)
  with assms(3) f' g' show "f' = g'" by clarsimp
qed (simp add: assms(2))

lemma (in semicategory) smc_Comp_is_epic_arr_is_epic_arr:
  assumes "g : a ↦⇘ℭ⇙ b" and "f : b ↦⇘ℭ⇙ c" and "f ∘⇩A⇘ℭ⇙ g : a ↦⇩e⇩p⇩i⇘ℭ⇙ c"
  shows "f : b ↦⇩e⇩p⇩i⇘ℭ⇙ c"
proof-
  from assms have "g : b ↦⇘op_smc ℭ⇙ a" "f : c ↦⇘op_smc ℭ⇙ b" 
    unfolding smc_op_simps by simp_all 
  moreover from semicategory_axioms assms have "g ∘⇩A⇘op_smc ℭ⇙ f : a ↦⇩e⇩p⇩i⇘ℭ⇙ c"
    by (cs_concl cs_shallow cs_simp: smc_op_simps)
  ultimately show ?thesis 
    using 
      semicategory.smc_Comp_is_monic_arr_is_monic_arr[
        OF semicategory_op, folded is_epic_arr_def
        ]
    by auto
qed



subsection‹Idempotent arrow›


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

definition is_idem_arr :: "V ⇒ V ⇒ V ⇒ bool"
  where "is_idem_arr ℭ b f ⟷ f : b ↦⇘ℭ⇙ b ∧ f ∘⇩A⇘ℭ⇙ f = f"

syntax "_is_idem_arr" :: "V ⇒ V ⇒ V ⇒ bool" (‹_ : ↦⇩i⇩d⇩eı _› [51, 51] 51)
syntax_consts "_is_idem_arr" ⇌ is_idem_arr
translations "f : ↦⇩i⇩d⇩e⇘ℭ⇙ b" ⇌ "CONST is_idem_arr ℭ b f"


text‹Rules.›

mk_ide rf is_idem_arr_def
  |intro is_idem_arrI|
  |dest is_idem_arrD[dest]|
  |elim is_idem_arrE[elim!]|

lemmas [smc_cs_simps] = is_idem_arrD(2)


text‹Elementary properties.›

lemma (in semicategory) op_smc_is_idem_arr[smc_op_simps]: 
  "f : ↦⇩i⇩d⇩e⇘op_smc ℭ⇙ b ⟷ f : ↦⇩i⇩d⇩e⇘ℭ⇙ b"
  using op_smc_Comp unfolding is_idem_arr_def smc_op_simps by auto



subsection‹Terminal object and initial object›


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

definition obj_terminal :: "V ⇒ V ⇒ bool"
  where "obj_terminal ℭ t ⟷ 
    t ∈⇩∘ ℭ⦇Obj⦈ ∧ (∀a. a ∈⇩∘ ℭ⦇Obj⦈ ⟶ (∃!f. f : a ↦⇘ℭ⇙ t))"

definition obj_initial :: "V ⇒ V ⇒ bool"
  where "obj_initial ℭ ≡ obj_terminal (op_smc ℭ)"


text‹Rules.›

mk_ide rf obj_terminal_def
  |intro obj_terminalI|
  |dest obj_terminalD[dest]|
  |elim obj_terminalE[elim]|

lemma obj_initialI:
  assumes "a ∈⇩∘ ℭ⦇Obj⦈" and "⋀b. b ∈⇩∘ ℭ⦇Obj⦈ ⟹ ∃!f. f : a ↦⇘ℭ⇙ b" 
  shows "obj_initial ℭ a"
  unfolding obj_initial_def
  by (simp add: obj_terminalI[of _ ‹op_smc ℭ›, unfolded smc_op_simps, OF assms])

lemma obj_initialD[dest]:
  assumes "obj_initial ℭ a" 
  shows "a ∈⇩∘ ℭ⦇Obj⦈" and "⋀b. b ∈⇩∘ ℭ⦇Obj⦈ ⟹ ∃!f. f : a ↦⇘ℭ⇙ b"   
  by 
    (
      simp_all add: 
        obj_terminalD[OF assms[unfolded obj_initial_def], unfolded smc_op_simps]
    )

lemma obj_initialE[elim]:
  assumes "obj_initial ℭ a" 
  obtains "a ∈⇩∘ ℭ⦇Obj⦈" and "⋀b. b ∈⇩∘ ℭ⦇Obj⦈ ⟹ ∃!f. f : a ↦⇘ℭ⇙ b"   
  using assms by (auto simp: obj_initialD)


text‹Elementary properties.›

lemma op_smc_obj_initial[smc_op_simps]: 
  "obj_initial (op_smc ℭ) = obj_terminal ℭ"
  unfolding obj_initial_def obj_terminal_def smc_op_simps ..

lemma op_smc_obj_terminal[smc_op_simps]: 
  "obj_terminal (op_smc ℭ) = obj_initial ℭ"
  unfolding obj_initial_def obj_terminal_def smc_op_simps ..



subsection‹Null object›


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

definition obj_null :: "V ⇒ V ⇒ bool"
  where "obj_null ℭ a ⟷ obj_initial ℭ a ∧ obj_terminal ℭ a"


text‹Rules.›

mk_ide rf obj_null_def
  |intro obj_nullI|
  |dest obj_nullD[dest]|
  |elim obj_nullE[elim]|


text‹Elementary properties.›

lemma op_smc_obj_null[smc_op_simps]: "obj_null (op_smc ℭ) a = obj_null ℭ a"
  unfolding obj_null_def smc_op_simps by auto



subsection‹Zero arrow›

definition is_zero_arr :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_zero_arr ℭ a b h ⟷
    (∃z g f. obj_null ℭ z ∧ h = g ∘⇩A⇘ℭ⇙ f ∧ f : a ↦⇘ℭ⇙ z ∧ g : z ↦⇘ℭ⇙ b)"

syntax "_is_zero_arr" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹_ : _ ↦⇩0ı _› [51, 51, 51] 51)
syntax_consts "_is_zero_arr" ⇌ is_zero_arr
translations "h : a ↦⇩0⇘ℭ⇙ b" ⇌ "CONST is_zero_arr ℭ a b h"


text‹Rules.›

lemma is_zero_arrI:
  assumes "obj_null ℭ z" 
    and "h = g ∘⇩A⇘ℭ⇙ f" 
    and "f : a ↦⇘ℭ⇙ z" 
    and "g : z ↦⇘ℭ⇙ b"
  shows "h : a ↦⇩0⇘ℭ⇙ b"
  using assms unfolding is_zero_arr_def by auto

lemma is_zero_arrD[dest]:
  assumes "h : a ↦⇩0⇘ℭ⇙ b"
  shows "∃z g f. obj_null ℭ z ∧ h = g ∘⇩A⇘ℭ⇙ f ∧ f : a ↦⇘ℭ⇙ z ∧ g : z ↦⇘ℭ⇙ b"
  using assms unfolding is_zero_arr_def by simp

lemma is_zero_arrE[elim]:
  assumes "h : a ↦⇩0⇘ℭ⇙ b"
  obtains z g f 
    where "obj_null ℭ z"
      and "h = g ∘⇩A⇘ℭ⇙ f" 
      and "f : a ↦⇘ℭ⇙ z" 
      and "g : z ↦⇘ℭ⇙ b"
  using assms by auto


text‹Elementary properties.›

lemma (in semicategory) op_smc_is_zero_arr[smc_op_simps]: 
  "f : b ↦⇩0⇘op_smc ℭ⇙ a ⟷ f : a ↦⇩0⇘ℭ⇙ b"
  using op_smc_Comp unfolding is_zero_arr_def smc_op_simps by metis

lemma (in semicategory) smc_is_zero_arr_Comp_right:
  assumes "h : b ↦⇩0⇘ℭ⇙ c" and "h' : a ↦⇘ℭ⇙ b"
  shows "h ∘⇩A⇘ℭ⇙ h' : a ↦⇩0⇘ℭ⇙ c"
proof-
  from assms(1) obtain z g f  
    where "obj_null ℭ z" 
      and "h = g ∘⇩A⇘ℭ⇙ f" 
      and "f : b ↦⇘ℭ⇙ z" 
      and "g : z ↦⇘ℭ⇙ c"
    by auto 
  with assms show ?thesis 
    by (auto simp: smc_cs_simps intro: is_zero_arrI smc_cs_intros) 
qed

lemmas [smc_arrow_cs_intros] = semicategory.smc_is_zero_arr_Comp_right

lemma (in semicategory) smc_is_zero_arr_Comp_left:
  assumes "h' : b ↦⇘ℭ⇙ c" and "h : a ↦⇩0⇘ℭ⇙ b" 
  shows "h' ∘⇩A⇘ℭ⇙ h : a ↦⇩0⇘ℭ⇙ c"
proof-
  from assms(2) obtain z g f 
    where "obj_null ℭ z" 
      and "h = g ∘⇩A⇘ℭ⇙ f" 
      and "f : a ↦⇘ℭ⇙ z" 
      and "g : z ↦⇘ℭ⇙ b"
    by auto
  with assms(1) show ?thesis
    by (intro is_zero_arrI[of _ _ _ ‹h' ∘⇩A⇘ℭ⇙ g›]) 
      (auto simp: smc_Comp_assoc intro: is_zero_arrI smc_cs_intros)
qed

lemmas [smc_arrow_cs_intros] = semicategory.smc_is_zero_arr_Comp_left

text‹\newpage›

end