Theory CZH_ECAT_SS

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹→∙←› and ‹←∙→›: cospan and span›
theory CZH_ECAT_SS
  imports CZH_ECAT_Small_Functor
begin



subsection‹Background›


text‹
General information about ‹→∙←› and ‹←∙→› (also known as 
cospans and spans, respectively) can be found in in Chapters III-3 and III-4 
in \<^cite>‹"mac_lane_categories_2010"›, as well as 
nLab \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/cospan}
}\footnote{\url{https://ncatlab.org/nlab/show/span}}.
›

named_theorems cat_ss_cs_simps
named_theorems cat_ss_cs_intros

named_theorems cat_ss_elem_simps

definition 𝔬⇩S⇩S where [cat_ss_elem_simps]: "𝔬⇩S⇩S = 0"
definition 𝔞⇩S⇩S where [cat_ss_elem_simps]: "𝔞⇩S⇩S = 1⇩ℕ"
definition 𝔟⇩S⇩S where [cat_ss_elem_simps]: "𝔟⇩S⇩S = 2⇩ℕ"
definition 𝔤⇩S⇩S where [cat_ss_elem_simps]: "𝔤⇩S⇩S = 3⇩ℕ"
definition 𝔣⇩S⇩S where [cat_ss_elem_simps]: "𝔣⇩S⇩S = 4⇩ℕ"

lemma cat_ss_ineq:
  shows cat_ss_𝔞𝔟[cat_ss_cs_intros]: "𝔞⇩S⇩S ≠ 𝔟⇩S⇩S"
    and cat_ss_𝔞𝔬[cat_ss_cs_intros]: "𝔞⇩S⇩S ≠ 𝔬⇩S⇩S"
    and cat_ss_𝔟𝔬[cat_ss_cs_intros]: "𝔟⇩S⇩S ≠ 𝔬⇩S⇩S"
    and cat_ss_𝔤𝔣[cat_ss_cs_intros]: "𝔤⇩S⇩S ≠ 𝔣⇩S⇩S"
    and cat_ss_𝔤𝔞[cat_ss_cs_intros]: "𝔤⇩S⇩S ≠ 𝔞⇩S⇩S"
    and cat_ss_𝔤𝔟[cat_ss_cs_intros]: "𝔤⇩S⇩S ≠ 𝔟⇩S⇩S"
    and cat_ss_𝔤𝔬[cat_ss_cs_intros]: "𝔤⇩S⇩S ≠ 𝔬⇩S⇩S"
    and cat_ss_𝔣𝔞[cat_ss_cs_intros]: "𝔣⇩S⇩S ≠ 𝔞⇩S⇩S"
    and cat_ss_𝔣𝔟[cat_ss_cs_intros]: "𝔣⇩S⇩S ≠ 𝔟⇩S⇩S"
    and cat_ss_𝔣𝔬[cat_ss_cs_intros]: "𝔣⇩S⇩S ≠ 𝔬⇩S⇩S"
  unfolding cat_ss_elem_simps by simp_all

lemma (in 𝒵) 
  shows cat_ss_𝔞[cat_ss_cs_intros]: "𝔞⇩S⇩S ∈⇩∘ Vset α"
    and cat_ss_𝔟[cat_ss_cs_intros]: "𝔟⇩S⇩S ∈⇩∘ Vset α"
    and cat_ss_𝔬[cat_ss_cs_intros]: "𝔬⇩S⇩S ∈⇩∘ Vset α"
    and cat_ss_𝔤[cat_ss_cs_intros]: "𝔤⇩S⇩S ∈⇩∘ Vset α"
    and cat_ss_𝔣[cat_ss_cs_intros]: "𝔣⇩S⇩S ∈⇩∘ Vset α"
  unfolding cat_ss_elem_simps by simp_all



subsection‹Composable arrows in ‹→∙←› and ‹←∙→››

abbreviation cat_scospan_composable :: V
  where "cat_scospan_composable ≡ 
    (set {𝔬⇩S⇩S} ×⇩∙ set {𝔬⇩S⇩S, 𝔤⇩S⇩S, 𝔣⇩S⇩S}) ∪⇩∘ 
    (set {𝔤⇩S⇩S, 𝔞⇩S⇩S} ×⇩∙ set {𝔞⇩S⇩S}) ∪⇩∘ 
    (set {𝔣⇩S⇩S, 𝔟⇩S⇩S} ×⇩∙ set {𝔟⇩S⇩S})"

abbreviation cat_sspan_composable :: V
  where "cat_sspan_composable ≡ (cat_scospan_composable)¯⇩∙"


text‹Rules.›

lemma cat_scospan_composable_𝔬𝔬[cat_ss_cs_intros]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composable_𝔬𝔤[cat_ss_cs_intros]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔤⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composable_𝔬𝔣[cat_ss_cs_intros]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔣⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composable_𝔤𝔞[cat_ss_cs_intros]:
  assumes "g = 𝔤⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composable_𝔣𝔟[cat_ss_cs_intros]:
  assumes "g = 𝔣⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composable_𝔞𝔞[cat_ss_cs_intros]:
  assumes "g = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composable_𝔟𝔟[cat_ss_cs_intros]:
  assumes "g = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  using assms by auto

lemma cat_scospan_composableE:
  assumes "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable"
  obtains "g = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S" 
        | "g = 𝔬⇩S⇩S" and "f = 𝔤⇩S⇩S"
        | "g = 𝔬⇩S⇩S" and "f = 𝔣⇩S⇩S"
        | "g = 𝔤⇩S⇩S" and "f = 𝔞⇩S⇩S"
        | "g = 𝔣⇩S⇩S" and "f = 𝔟⇩S⇩S"
        | "g = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
        | "g = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  using assms that by auto

lemma cat_sspan_composable_𝔬𝔬[cat_ss_cs_intros]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composable_𝔤𝔬[cat_ss_cs_intros]:
  assumes "g = 𝔤⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composable_𝔣𝔬[cat_ss_cs_intros]:
  assumes "g = 𝔣⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composable_𝔞𝔤[cat_ss_cs_intros]:
  assumes "g = 𝔞⇩S⇩S" and "f = 𝔤⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composable_𝔟𝔣[cat_ss_cs_intros]:
  assumes "g = 𝔟⇩S⇩S" and "f = 𝔣⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composable_𝔞𝔞[cat_ss_cs_intros]:
  assumes "g = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composable_𝔟𝔟[cat_ss_cs_intros]:
  assumes "g = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  using assms by auto

lemma cat_sspan_composableE:
  assumes "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable"
  obtains "g = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S" 
        | "g = 𝔤⇩S⇩S" and "f = 𝔬⇩S⇩S"
        | "g = 𝔣⇩S⇩S" and "f = 𝔬⇩S⇩S"
        | "g = 𝔞⇩S⇩S" and "f = 𝔤⇩S⇩S"
        | "g = 𝔟⇩S⇩S" and "f = 𝔣⇩S⇩S"
        | "g = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
        | "g = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  using assms that by auto



subsection‹Categories ‹→∙←› and ‹←∙→››


subsubsection‹Definition and elementary properties›


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

definition the_cat_scospan :: V (‹→∙←⇩C›)
  where "→∙←⇩C =
    [
      set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S},
      set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S},
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | x = 𝔤⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔣⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      ),
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      ),
      (
        λgf∈⇩∘cat_scospan_composable. 
         if gf = [𝔬⇩S⇩S, 𝔤⇩S⇩S]⇩∘ ⇒ 𝔤⇩S⇩S
          | gf = [𝔬⇩S⇩S, 𝔣⇩S⇩S]⇩∘ ⇒ 𝔣⇩S⇩S
          | otherwise ⇒ gf⦇0⦈
      ),
      vid_on (set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S})
    ]⇩∘"

definition the_cat_sspan :: V (‹←∙→⇩C›)
  where "←∙→⇩C =
    [
      set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S},
      set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S},
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      ),
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | x = 𝔤⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔣⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      ),
      (
        λgf∈⇩∘cat_sspan_composable. 
         if gf = [𝔞⇩S⇩S, 𝔤⇩S⇩S]⇩∘ ⇒ 𝔤⇩S⇩S
          | gf = [𝔟⇩S⇩S, 𝔣⇩S⇩S]⇩∘ ⇒ 𝔣⇩S⇩S
          | otherwise ⇒ gf⦇0⦈
      ),
      vid_on (set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S})
    ]⇩∘"


text‹Components.›

lemma the_cat_scospan_components: 
  shows "→∙←⇩C⦇Obj⦈ = set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S}"
    and "→∙←⇩C⦇Arr⦈ = set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}"
    and "→∙←⇩C⦇Dom⦈ = 
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | x = 𝔤⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔣⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      )"
    and "→∙←⇩C⦇Cod⦈ = 
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      )"
    and "→∙←⇩C⦇Comp⦈ =
      (
        λgf∈⇩∘cat_scospan_composable. 
         if gf = [𝔬⇩S⇩S, 𝔤⇩S⇩S]⇩∘ ⇒ 𝔤⇩S⇩S
          | gf = [𝔬⇩S⇩S, 𝔣⇩S⇩S]⇩∘ ⇒ 𝔣⇩S⇩S
          | otherwise ⇒ gf⦇0⦈
      )"
    and "→∙←⇩C⦇CId⦈ = vid_on (set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S})"
  unfolding the_cat_scospan_def dg_field_simps by (simp_all add: nat_omega_simps)

lemma the_cat_sspan_components: 
  shows "←∙→⇩C⦇Obj⦈ = set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S}"
    and "←∙→⇩C⦇Arr⦈ = set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}"
    and "←∙→⇩C⦇Dom⦈ =
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      )"
    and "←∙→⇩C⦇Cod⦈ =
      (
        λx∈⇩∘set {𝔞⇩S⇩S, 𝔤⇩S⇩S, 𝔬⇩S⇩S, 𝔣⇩S⇩S, 𝔟⇩S⇩S}. 
         if x = 𝔞⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔟⇩S⇩S ⇒ 𝔟⇩S⇩S
          | x = 𝔤⇩S⇩S ⇒ 𝔞⇩S⇩S
          | x = 𝔣⇩S⇩S ⇒ 𝔟⇩S⇩S
          | otherwise ⇒ 𝔬⇩S⇩S
      )"
    and "←∙→⇩C⦇Comp⦈ =
      (
        λgf∈⇩∘cat_sspan_composable. 
         if gf = [𝔞⇩S⇩S, 𝔤⇩S⇩S]⇩∘ ⇒ 𝔤⇩S⇩S
          | gf = [𝔟⇩S⇩S, 𝔣⇩S⇩S]⇩∘ ⇒ 𝔣⇩S⇩S
          | otherwise ⇒ gf⦇0⦈
      )"
    and "←∙→⇩C⦇CId⦈ = vid_on (set {𝔞⇩S⇩S, 𝔟⇩S⇩S, 𝔬⇩S⇩S})"
  unfolding the_cat_sspan_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Elementary properties.›

lemma the_cat_scospan_components_vsv[cat_ss_cs_intros]: "vsv (→∙←⇩C)"
  unfolding the_cat_scospan_def by auto

lemma the_cat_sspan_components_vsv[cat_ss_cs_intros]: "vsv (←∙→⇩C)"
  unfolding the_cat_sspan_def by auto


subsubsection‹Objects›

lemma the_cat_scospan_Obj_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Obj_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Obj_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_ObjE:
  assumes "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
  obtains ‹a = 𝔬⇩S⇩S› | ‹a = 𝔞⇩S⇩S› | ‹a = 𝔟⇩S⇩S›
  using assms unfolding the_cat_scospan_components by auto

lemma the_cat_sspan_Obj_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Obj⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Obj_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Obj⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Obj_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Obj⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_ObjE:
  assumes "a ∈⇩∘ ←∙→⇩C⦇Obj⦈"
  obtains ‹a = 𝔬⇩S⇩S› | ‹a = 𝔞⇩S⇩S› | ‹a = 𝔟⇩S⇩S›
  using assms unfolding the_cat_sspan_components by auto


subsubsection‹Arrows›

lemma the_cat_scospan_Arr_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Arr⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Arr⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Arr⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔤I[cat_ss_cs_intros]:
  assumes "a = 𝔤⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Arr⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔣I[cat_ss_cs_intros]:
  assumes "a = 𝔣⇩S⇩S"
  shows "a ∈⇩∘ →∙←⇩C⦇Arr⦈"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_ArrE:
  assumes "f ∈⇩∘ →∙←⇩C⦇Arr⦈"
  obtains ‹f = 𝔞⇩S⇩S› | ‹f = 𝔟⇩S⇩S› | ‹f = 𝔬⇩S⇩S› | ‹f = 𝔤⇩S⇩S› | ‹f = 𝔣⇩S⇩S› 
  using assms unfolding the_cat_scospan_components by auto

lemma the_cat_sspan_Arr_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔤I[cat_ss_cs_intros]:
  assumes "a = 𝔤⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔣I[cat_ss_cs_intros]:
  assumes "a = 𝔣⇩S⇩S"
  shows "a ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_ArrE:
  assumes "f ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  obtains ‹f = 𝔞⇩S⇩S› | ‹f = 𝔟⇩S⇩S› | ‹f = 𝔬⇩S⇩S› | ‹f = 𝔤⇩S⇩S› | ‹f = 𝔣⇩S⇩S› 
  using assms unfolding the_cat_sspan_components by auto


subsubsection‹Domain›

mk_VLambda the_cat_scospan_components(3)
  |vsv the_cat_scospan_Dom_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_scospan_Dom_vdomain[cat_ss_cs_simps]|

lemma the_cat_scospan_Dom_app_𝔞[cat_ss_cs_simps]:
  assumes "f = 𝔞⇩S⇩S"
  shows "→∙←⇩C⦇Dom⦈⦇f⦈ = 𝔞⇩S⇩S"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Dom_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟⇩S⇩S"
  shows "→∙←⇩C⦇Dom⦈⦇f⦈ = 𝔟⇩S⇩S"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Dom_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬⇩S⇩S"
  shows "→∙←⇩C⦇Dom⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Dom_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤⇩S⇩S"
  shows "→∙←⇩C⦇Dom⦈⦇f⦈ = 𝔞⇩S⇩S"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Dom_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣⇩S⇩S"
  shows "→∙←⇩C⦇Dom⦈⦇f⦈ = 𝔟⇩S⇩S"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

mk_VLambda the_cat_sspan_components(3)
  |vsv the_cat_sspan_Dom_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_sspan_Dom_vdomain[cat_ss_cs_simps]|

lemma the_cat_sspan_Dom_app_𝔞[cat_ss_cs_simps]:
  assumes "f = 𝔞⇩S⇩S"
  shows "←∙→⇩C⦇Dom⦈⦇f⦈ = 𝔞⇩S⇩S"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Dom_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟⇩S⇩S"
  shows "←∙→⇩C⦇Dom⦈⦇f⦈ = 𝔟⇩S⇩S"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Dom_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬⇩S⇩S"
  shows "←∙→⇩C⦇Dom⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Dom_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤⇩S⇩S"
  shows "←∙→⇩C⦇Dom⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Dom_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣⇩S⇩S"
  shows "←∙→⇩C⦇Dom⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto


subsubsection‹Codomain›

mk_VLambda the_cat_scospan_components(4)
  |vsv the_cat_scospan_Cod_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_scospan_Cod_vdomain[cat_ss_cs_simps]|

lemma the_cat_scospan_Cod_app_𝔞[cat_ss_cs_simps]:
  assumes "f = 𝔞⇩S⇩S"
  shows "→∙←⇩C⦇Cod⦈⦇f⦈ = 𝔞⇩S⇩S"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Cod_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟⇩S⇩S"
  shows "→∙←⇩C⦇Cod⦈⦇f⦈ = 𝔟⇩S⇩S"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Cod_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬⇩S⇩S"
  shows "→∙←⇩C⦇Cod⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Cod_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤⇩S⇩S"
  shows "→∙←⇩C⦇Cod⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Cod_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣⇩S⇩S"
  shows "→∙←⇩C⦇Cod⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

mk_VLambda the_cat_sspan_components(4)
  |vsv the_cat_sspan_Cod_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_sspan_Cod_vdomain[cat_ss_cs_simps]|

lemma the_cat_sspan_Cod_app_𝔞[cat_ss_cs_simps]:
  assumes "f = 𝔞⇩S⇩S"
  shows "←∙→⇩C⦇Cod⦈⦇f⦈ = 𝔞⇩S⇩S"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Cod_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟⇩S⇩S"
  shows "←∙→⇩C⦇Cod⦈⦇f⦈ = 𝔟⇩S⇩S"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Cod_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬⇩S⇩S"
  shows "←∙→⇩C⦇Cod⦈⦇f⦈ = 𝔬⇩S⇩S"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Cod_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤⇩S⇩S"
  shows "←∙→⇩C⦇Cod⦈⦇f⦈ = 𝔞⇩S⇩S"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Cod_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣⇩S⇩S"
  shows "←∙→⇩C⦇Cod⦈⦇f⦈ = 𝔟⇩S⇩S"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto


subsubsection‹Composition›

mk_VLambda the_cat_scospan_components(5)
  |vsv the_cat_scospan_Comp_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_scospan_Comp_vdomain[cat_ss_cs_simps]|

lemma the_cat_scospan_Comp_app_𝔞𝔞[cat_ss_cs_simps]:
  assumes "g = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = g" "g ∘⇩A⇘→∙←⇩C⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  with assms show "g ∘⇩A⇘→∙←⇩C⇙ f = g" "g ∘⇩A⇘→∙←⇩C⇙ f = f"
    unfolding the_cat_scospan_components(5) by (auto simp: nat_omega_simps)
qed

lemma the_cat_scospan_Comp_app_𝔟𝔟[cat_ss_cs_simps]:
  assumes "g = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = g" "g ∘⇩A⇘→∙←⇩C⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  with assms show "g ∘⇩A⇘→∙←⇩C⇙ f = g" "g ∘⇩A⇘→∙←⇩C⇙ f = f"
    unfolding the_cat_scospan_components(5) by (auto simp: nat_omega_simps)
qed

lemma the_cat_scospan_Comp_app_𝔬𝔬[cat_ss_cs_simps]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = g" "g ∘⇩A⇘→∙←⇩C⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  with assms show "g ∘⇩A⇘→∙←⇩C⇙ f = g" "g ∘⇩A⇘→∙←⇩C⇙ f = f"
    unfolding the_cat_scospan_components(5) by (auto simp: nat_omega_simps)
qed

lemma the_cat_scospan_Comp_app_𝔬𝔤[cat_ss_cs_simps]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔤⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = f" 
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  then show "g ∘⇩A⇘→∙←⇩C⇙ f = f" 
    unfolding the_cat_scospan_components(5) assms by (auto simp: nat_omega_simps)
qed

lemma the_cat_scospan_Comp_app_𝔬𝔣[cat_ss_cs_simps]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔣⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = f" 
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  then show "g ∘⇩A⇘→∙←⇩C⇙ f = f" 
    unfolding the_cat_scospan_components(5) assms by (auto simp: nat_omega_simps)
qed

lemma the_cat_scospan_Comp_app_𝔤𝔞[cat_ss_cs_simps]:
  assumes "g = 𝔤⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = g"  
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  then show "g ∘⇩A⇘→∙←⇩C⇙ f = g" 
    unfolding the_cat_scospan_components(5) assms 
    using cat_ss_ineq
    by (auto simp: nat_omega_simps)
qed

lemma the_cat_scospan_Comp_app_𝔣𝔟[cat_ss_cs_simps]:
  assumes "g = 𝔣⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "g ∘⇩A⇘→∙←⇩C⇙ f = g"  
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_scospan_composable" by auto
  then show "g ∘⇩A⇘→∙←⇩C⇙ f = g" 
    unfolding the_cat_scospan_components(5) assms 
    using cat_ss_ineq
    by (auto simp: nat_omega_simps)
qed

mk_VLambda the_cat_sspan_components(5)
  |vsv the_cat_sspan_Comp_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_sspan_Comp_vdomain[cat_ss_cs_simps]|

lemma the_cat_sspan_Comp_app_𝔞𝔞[cat_ss_cs_simps]:
  assumes "g = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = g" "g ∘⇩A⇘←∙→⇩C⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  with assms show "g ∘⇩A⇘←∙→⇩C⇙ f = g" "g ∘⇩A⇘←∙→⇩C⇙ f = f"
    unfolding the_cat_sspan_components(5) by (auto simp: nat_omega_simps)
qed

lemma the_cat_sspan_Comp_app_𝔟𝔟[cat_ss_cs_simps]:
  assumes "g = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = g" "g ∘⇩A⇘←∙→⇩C⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  with assms show "g ∘⇩A⇘←∙→⇩C⇙ f = g" "g ∘⇩A⇘←∙→⇩C⇙ f = f"
    unfolding the_cat_sspan_components(5) by (auto simp: nat_omega_simps)
qed

lemma the_cat_sspan_Comp_app_𝔬𝔬[cat_ss_cs_simps]:
  assumes "g = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = g" "g ∘⇩A⇘←∙→⇩C⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  with assms show "g ∘⇩A⇘←∙→⇩C⇙ f = g" "g ∘⇩A⇘←∙→⇩C⇙ f = f"
    unfolding the_cat_sspan_components(5) by (auto simp: nat_omega_simps)
qed

lemma the_cat_sspan_Comp_app_𝔞𝔤[cat_ss_cs_simps]:
  assumes "g = 𝔞⇩S⇩S" and "f = 𝔤⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = f" 
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  then show "g ∘⇩A⇘←∙→⇩C⇙ f = f" 
    unfolding the_cat_sspan_components(5) assms by (auto simp: nat_omega_simps)
qed

lemma the_cat_sspan_Comp_app_𝔟𝔣[cat_ss_cs_simps]:
  assumes "g = 𝔟⇩S⇩S" and "f = 𝔣⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = f" 
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  then show "g ∘⇩A⇘←∙→⇩C⇙ f = f" 
    unfolding the_cat_sspan_components(5) assms by (auto simp: nat_omega_simps)
qed

lemma the_cat_sspan_Comp_app_𝔤𝔬[cat_ss_cs_simps]:
  assumes "g = 𝔤⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = g"  
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  then show "g ∘⇩A⇘←∙→⇩C⇙ f = g" 
    unfolding the_cat_sspan_components(5) assms 
    using cat_ss_ineq
    by (auto simp: nat_omega_simps)
qed

lemma the_cat_sspan_Comp_app_𝔣𝔬[cat_ss_cs_simps]:
  assumes "g = 𝔣⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "g ∘⇩A⇘←∙→⇩C⇙ f = g"  
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_sspan_composable" by auto
  then show "g ∘⇩A⇘←∙→⇩C⇙ f = g" 
    unfolding the_cat_sspan_components(5) assms 
    using cat_ss_ineq
    by (auto simp: nat_omega_simps)
qed


subsubsection‹Identity›

mk_VLambda the_cat_scospan_components(6)[folded VLambda_vid_on]
  |vsv the_cat_scospan_CId_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_scospan_CId_vdomain[cat_ss_cs_simps]|
  |app the_cat_scospan_CId_app[cat_ss_cs_simps]|

mk_VLambda the_cat_sspan_components(6)[folded VLambda_vid_on]
  |vsv the_cat_sspan_CId_vsv[cat_ss_cs_intros]|
  |vdomain the_cat_sspan_CId_vdomain[cat_ss_cs_simps]|
  |app the_cat_sspan_CId_app[cat_ss_cs_simps]|


subsubsection‹Arrow with a domain and a codomain›

lemma the_cat_scospan_is_arr_𝔞𝔞𝔞[cat_ss_cs_intros]:
  assumes "a' = 𝔞⇩S⇩S" and "b' = 𝔞⇩S⇩S" and "f = 𝔞⇩S⇩S"
  shows "f : a' ↦⇘→∙←⇩C⇙ b'"
proof(intro is_arrI, unfold assms)
  show "→∙←⇩C⦇Dom⦈⦇𝔞⇩S⇩S⦈ = 𝔞⇩S⇩S" "→∙←⇩C⦇Cod⦈⦇𝔞⇩S⇩S⦈ = 𝔞⇩S⇩S"
    by (cs_concl cs_simp: cat_ss_cs_simps)+
qed (auto simp: the_cat_scospan_components)

lemma the_cat_scospan_is_arr_𝔟𝔟𝔟[cat_ss_cs_intros]:
  assumes "a' = 𝔟⇩S⇩S" and "b' = 𝔟⇩S⇩S" and "f = 𝔟⇩S⇩S"
  shows "f : a' ↦⇘→∙←⇩C⇙ b'"
proof(intro is_arrI, unfold assms)
  show "→∙←⇩C⦇Dom⦈⦇𝔟⇩S⇩S⦈ = 𝔟⇩S⇩S" "→∙←⇩C⦇Cod⦈⦇𝔟⇩S⇩S⦈ = 𝔟⇩S⇩S"
    by (cs_concl cs_simp: cat_ss_cs_simps)+
qed (auto simp: the_cat_scospan_components)

lemma the_cat_scospan_is_arr_𝔬𝔬𝔬[cat_ss_cs_intros]:
  assumes "a' = 𝔬⇩S⇩S" and "b' = 𝔬⇩S⇩S" and "f = 𝔬⇩S⇩S"
  shows "f : a' ↦⇘→∙←⇩C⇙ b'"
proof(intro is_arrI, unfold assms)
  show "→∙←⇩C⦇Dom⦈⦇𝔬⇩S⇩S⦈ = 𝔬⇩S⇩S" "→∙←⇩C⦇Cod⦈⦇𝔬⇩S⇩S⦈ = 𝔬⇩S⇩S"
    by (cs_concl cs_simp: cat_ss_cs_simps)+
qed (auto simp: the_cat_scospan_components)

lemma the_cat_scospan_is_arr_𝔞𝔬𝔤[cat_ss_cs_intros]:
  assumes "a' = 𝔞⇩S⇩S" and "b' = 𝔬⇩S⇩S" and "f = 𝔤⇩S⇩S"
  shows "f : a' ↦⇘→∙←⇩C⇙ b'"
proof(intro is_arrI, unfold assms)
  show "→∙←⇩C⦇Dom⦈⦇𝔤⇩S⇩S⦈ = 𝔞⇩S⇩S" "→∙←⇩C⦇Cod⦈⦇𝔤⇩S⇩S⦈ = 𝔬⇩S⇩S"
    by (cs_concl cs_simp: cat_ss_cs_simps)+
qed (auto simp: the_cat_scospan_components)

lemma the_cat_scospan_is_arr_𝔟𝔬𝔣[cat_ss_cs_intros]:
  assumes "a' = 𝔟⇩S⇩S" and "b' = 𝔬⇩S⇩S" and "f = 𝔣⇩S⇩S"
  shows "f : a' ↦⇘→∙←⇩C⇙ b'"
proof(intro is_arrI, unfold assms)
  show "→∙←⇩C⦇Dom⦈⦇𝔣⇩S⇩S⦈ = 𝔟⇩S⇩S" "→∙←⇩C⦇Cod⦈⦇𝔣⇩S⇩S⦈ = 𝔬⇩S⇩S"
    by (cs_concl cs_shallow cs_simp: cat_ss_cs_simps)+
qed (auto simp: the_cat_scospan_components)

lemma the_cat_scospan_is_arrE:
  assumes "f' : a' ↦⇘→∙←⇩C⇙ b'"
  obtains "a' = 𝔞⇩S⇩S" and "b' = 𝔞⇩S⇩S" and "f' = 𝔞⇩S⇩S"
        | "a' = 𝔟⇩S⇩S" and "b' = 𝔟⇩S⇩S" and "f' = 𝔟⇩S⇩S"
        | "a' = 𝔬⇩S⇩S" and "b' = 𝔬⇩S⇩S" and "f' = 𝔬⇩S⇩S"
        | "a' = 𝔞⇩S⇩S" and "b' = 𝔬⇩S⇩S" and "f' = 𝔤⇩S⇩S"
        | "a' = 𝔟⇩S⇩S" and "b' = 𝔬⇩S⇩S" and "f' = 𝔣⇩S⇩S"
proof-
  note f = is_arrD[OF assms]
  from f(1) consider (𝔞⇩S⇩S) ‹f' = 𝔞⇩S⇩S› 
                   | (𝔟⇩S⇩S) ‹f' = 𝔟⇩S⇩S› 
                   | (𝔬⇩S⇩S) ‹f' = 𝔬⇩S⇩S› 
                   | (𝔤⇩S⇩S) ‹f' = 𝔤⇩S⇩S› 
                   | (𝔣⇩S⇩S) ‹f' = 𝔣⇩S⇩S› 
    by (elim the_cat_scospan_ArrE)
  then show ?thesis
  proof cases
    case 𝔞⇩S⇩S
    moreover from f(2,3)[unfolded 𝔞⇩S⇩S, symmetric] have "a' = 𝔞⇩S⇩S" "b' = 𝔞⇩S⇩S"
      by (simp_all add: cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔟⇩S⇩S
    moreover from f(2,3)[unfolded 𝔟⇩S⇩S, symmetric] have "a' = 𝔟⇩S⇩S" "b' = 𝔟⇩S⇩S"
      by (simp_all add: cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔬⇩S⇩S
    moreover from f(2,3)[unfolded 𝔬⇩S⇩S, symmetric] have "a' = 𝔬⇩S⇩S" "b' = 𝔬⇩S⇩S"
      by (simp_all add: cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔤⇩S⇩S
    moreover have "a' = 𝔞⇩S⇩S" "b' = 𝔬⇩S⇩S"
      by (simp_all add: f(2,3)[unfolded 𝔤⇩S⇩S, symmetric] cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔣⇩S⇩S
    moreover have "a' = 𝔟⇩S⇩S" "b' = 𝔬⇩S⇩S"
      by (simp_all add: f(2,3)[unfolded 𝔣⇩S⇩S, symmetric] cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  qed
qed


subsubsection‹‹→∙←› is a finite category›

lemma (in 𝒵) finite_category_the_cat_scospan[cat_ss_cs_intros]:
  "finite_category α (→∙←⇩C)"
proof(intro finite_categoryI'' tiny_categoryI'')
  show "vfsequence (→∙←⇩C)" unfolding the_cat_scospan_def by simp
  show "vcard (→∙←⇩C) = 6⇩ℕ"
    unfolding the_cat_scospan_def by (simp_all add: nat_omega_simps)
  show "ℛ⇩∘ (→∙←⇩C⦇Dom⦈) ⊆⇩∘ →∙←⇩C⦇Obj⦈" by (auto simp: the_cat_scospan_components)
  show "ℛ⇩∘ (→∙←⇩C⦇Cod⦈) ⊆⇩∘ →∙←⇩C⦇Obj⦈" by (auto simp: the_cat_scospan_components)
  show "(gf ∈⇩∘ 𝒟⇩∘ (→∙←⇩C⦇Comp⦈)) =
    (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘→∙←⇩C⇙ c ∧ f : a ↦⇘→∙←⇩C⇙ b)"
    for gf
    unfolding the_cat_scospan_Comp_vdomain
  proof
    assume prems: "gf ∈⇩∘ cat_scospan_composable"
    then obtain g f where gf_def: "gf = [g, f]⇩∘" by auto
    from prems show 
      "∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘→∙←⇩C⇙ c ∧ f : a ↦⇘→∙←⇩C⇙ b"
      unfolding gf_def
      by (*slow*)
        (
          cases rule: cat_scospan_composableE; 
          (intro exI conjI)?; 
          cs_concl_step?;
          (simp only:)?,
          all‹intro is_arrI, unfold the_cat_scospan_components(2)›
        )
        (cs_concl cs_simp: cat_ss_cs_simps V_cs_simps cs_intro: V_cs_intros)+
  next
    assume prems: 
      "∃g f b' c' a'. gf = [g, f]⇩∘ ∧ g : b' ↦⇘→∙←⇩C⇙ c' ∧ f : a' ↦⇘→∙←⇩C⇙ b'"
    then obtain g f b c a
      where gf_def: "gf = [g, f]⇩∘"
        and g: "g : b ↦⇘→∙←⇩C⇙ c"
        and f: "f : a ↦⇘→∙←⇩C⇙ b"
      by clarsimp
    from g f show "gf ∈⇩∘ cat_scospan_composable"
      unfolding gf_def 
      by (elim the_cat_scospan_is_arrE) (auto simp: cat_ss_cs_intros)
  qed
  show "𝒟⇩∘ (→∙←⇩C⦇CId⦈) = →∙←⇩C⦇Obj⦈"
    by (simp add: cat_ss_cs_simps the_cat_scospan_components)
  show "g ∘⇩A⇘→∙←⇩C⇙ f : a ↦⇘→∙←⇩C⇙ c"
    if "g : b ↦⇘→∙←⇩C⇙ c" and "f : a ↦⇘→∙←⇩C⇙ b" for b c g a f
    using that
    by (elim the_cat_scospan_is_arrE; simp only:)
      (
        all‹
          solves‹simp add: cat_ss_ineq cat_ss_ineq[symmetric]› |
          cs_concl cs_simp: cat_ss_cs_simps cs_intro: cat_ss_cs_intros
        ›
      )
  show "h ∘⇩A⇘→∙←⇩C⇙ g ∘⇩A⇘→∙←⇩C⇙ f = h ∘⇩A⇘→∙←⇩C⇙ (g ∘⇩A⇘→∙←⇩C⇙ f)"
    if "h : c ↦⇘→∙←⇩C⇙ d" and "g : b ↦⇘→∙←⇩C⇙ c" and "f : a ↦⇘→∙←⇩C⇙ b"
    for c d h b g a f
    using that 
    by (elim the_cat_scospan_is_arrE; simp only:) (*slow*)
      (
        all‹
          solves‹simp only: cat_ss_ineq cat_ss_ineq[symmetric]› | 
          cs_concl cs_simp: cat_ss_cs_simps cs_intro: cat_ss_cs_intros
          ›
      )
  show "→∙←⇩C⦇CId⦈⦇a⦈ : a ↦⇘→∙←⇩C⇙ a" if "a ∈⇩∘ →∙←⇩C⦇Obj⦈" for a
    using that
    by (elim the_cat_scospan_ObjE) 
      (
        all‹
          cs_concl 
            cs_simp: V_cs_simps cat_ss_cs_simps
            cs_intro: V_cs_intros cat_ss_cs_intros
        ›
      )
  show "→∙←⇩C⦇CId⦈⦇b⦈ ∘⇩A⇘→∙←⇩C⇙ f = f" if "f : a ↦⇘→∙←⇩C⇙ b" for a b f
    using that 
    by (elim the_cat_scospan_is_arrE) (*slow*)
      (
        cs_concl 
          cs_simp: V_cs_simps cat_ss_cs_simps 
          cs_intro: V_cs_intros cat_ss_cs_intros
      )+
  show "f ∘⇩A⇘→∙←⇩C⇙ →∙←⇩C⦇CId⦈⦇b⦈ = f" if "f : b ↦⇘→∙←⇩C⇙ c" for b c f
    using that 
    by (elim the_cat_scospan_is_arrE)
      (
        cs_concl 
          cs_simp: V_cs_simps cat_ss_cs_simps 
          cs_intro: V_cs_intros cat_ss_cs_intros
      )+
qed 
  (
    cs_concl 
      cs_simp: V_cs_simps cat_ss_cs_simps the_cat_scospan_components(1,2) 
      cs_intro: cat_cs_intros cat_ss_cs_intros V_cs_intros 
  )+

lemmas [cat_ss_cs_intros] = 𝒵.finite_category_the_cat_scospan


subsubsection‹Duality for ‹→∙←› and ‹←∙→››

lemma the_cat_scospan_op[cat_op_simps]: "op_cat (→∙←⇩C) = ←∙→⇩C"
proof-
  have dom_lhs: "𝒟⇩∘ (op_cat (→∙←⇩C)) = 6⇩ℕ" 
    unfolding op_cat_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (←∙→⇩C) = 6⇩ℕ" 
    unfolding the_cat_sspan_def by (simp add: nat_omega_simps)
  show ?thesis
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "a ∈⇩∘ 6⇩ℕ ⟹ op_cat (→∙←⇩C)⦇a⦈ = ←∙→⇩C⦇a⦈" for a
    proof
      (
        elim_in_numeral,
        fold dg_field_simps,
        unfold op_cat_components;
        rule sym
      )
      show "←∙→⇩C⦇Comp⦈ = fflip (→∙←⇩C⦇Comp⦈)"
      proof(rule vsv_eqI, unfold cat_ss_cs_simps vdomain_fflip)
        fix gf assume prems: "gf ∈⇩∘ cat_sspan_composable"
        then obtain g f where gf_def: "gf = [g, f]⇩∘" by auto
        from prems have fg: "[f, g]⇩∘ ∈⇩∘ cat_scospan_composable"
          unfolding gf_def by auto
        have [cat_ss_cs_simps]: "g ∘⇩A⇘←∙→⇩C⇙ f = f ∘⇩A⇘→∙←⇩C⇙ g"
          if "[f, g]⇩∘ ∈⇩∘ cat_scospan_composable"
          using that
          by (elim cat_scospan_composableE; simp only:)
            (cs_concl cs_simp: cat_ss_cs_simps cs_intro: cat_ss_cs_intros)+
        from fg show 
          "←∙→⇩C⦇Comp⦈⦇gf⦈ = fflip (→∙←⇩C⦇Comp⦈)⦇gf⦈"
          unfolding gf_def 
          by (cs_concl cs_shallow cs_simp: cat_ss_cs_simps fflip_app)
      qed (auto intro: fflip_vsv cat_ss_cs_intros)
    qed (unfold the_cat_sspan_components the_cat_scospan_components, simp_all)
  qed (auto intro: cat_op_intros cat_ss_cs_intros)
qed

lemma (in 𝒵) the_cat_sspan_op[cat_op_simps]: "op_cat (←∙→⇩C) = →∙←⇩C"
proof-
  interpret scospan: finite_category α ‹→∙←⇩C› 
    by (rule finite_category_the_cat_scospan)
  interpret sspan: finite_category α ‹←∙→⇩C›
    by (rule scospan.finite_category_op[unfolded cat_op_simps])
  from the_cat_scospan_op have "op_cat (←∙→⇩C) = op_cat (op_cat (→∙←⇩C))" 
    by simp
  also have "… = →∙←⇩C" by (cs_concl cs_shallow cs_simp: cat_op_simps)
  finally show ?thesis by auto
qed

lemmas [cat_op_simps] = 𝒵.the_cat_sspan_op


subsubsection‹‹←∙→› is a finite category›

lemma (in 𝒵) finite_category_the_cat_sspan[cat_ss_cs_intros]:
  "finite_category α (←∙→⇩C)"
proof-
  interpret scospan: finite_category α ‹→∙←⇩C›
    by (rule finite_category_the_cat_scospan)
  show ?thesis by (rule scospan.finite_category_op[unfolded cat_op_simps])
qed


subsection‹Local assumptions for functors from ‹→∙←› and ‹←∙→››


text‹
The functors from ‹→∙←› and ‹←∙→› are introduced as
convenient abstractions for the definition of the 
pullbacks and the pushouts (e.g., see Chapter III-3 and 
Chapter III-4 in \<^cite>‹"mac_lane_categories_2010"›).
›


subsubsection‹Definitions and elementary properties›

locale cf_scospan = category α ℭ for α 𝔞 𝔤 𝔬 𝔣 𝔟 ℭ +
  assumes cf_scospan_𝔤[cat_ss_cs_intros]: "𝔤 : 𝔞 ↦⇘ℭ⇙ 𝔬"
    and cf_scospan_𝔣[cat_ss_cs_intros]: "𝔣 : 𝔟 ↦⇘ℭ⇙ 𝔬"

lemma (in cf_scospan) cf_scospan_𝔤'[cat_ss_cs_intros]:
  assumes "a = 𝔞" and "b = 𝔬"
  shows "𝔤 : a ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_scospan_𝔤)

lemma (in cf_scospan) cf_scospan_𝔤''[cat_ss_cs_intros]:
  assumes "g = 𝔤" and "b = 𝔬"
  shows "g : 𝔞 ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_scospan_𝔤) 

lemma (in cf_scospan) cf_scospan_𝔤'''[cat_ss_cs_intros]:
  assumes "g = 𝔤" and "a = 𝔞"
  shows "g : a ↦⇘ℭ⇙ 𝔬"
  unfolding assms by (rule cf_scospan_𝔤) 

lemma (in cf_scospan) cf_scospan_𝔣'[cat_ss_cs_intros]:
  assumes "a = 𝔟" and "b = 𝔬"
  shows "𝔣 : a ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_scospan_𝔣) 

lemma (in cf_scospan) cf_scospan_𝔣''[cat_ss_cs_intros]:
  assumes "f = 𝔣" and "b = 𝔬"
  shows "f : 𝔟 ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_scospan_𝔣) 

lemma (in cf_scospan) cf_scospan_𝔣'''[cat_ss_cs_intros]:
  assumes "g = 𝔣" and "b = 𝔟"
  shows "g : b ↦⇘ℭ⇙ 𝔬"
  unfolding assms by (rule cf_scospan_𝔣) 

locale cf_sspan = category α ℭ for α 𝔞 𝔤 𝔬 𝔣 𝔟 and ℭ +
  assumes cf_sspan_𝔤[cat_ss_cs_intros]: "𝔤 : 𝔬 ↦⇘ℭ⇙ 𝔞"
    and cf_sspan_𝔣[cat_ss_cs_intros]: "𝔣 : 𝔬 ↦⇘ℭ⇙ 𝔟"

lemma (in cf_sspan) cf_sspan_𝔤'[cat_ss_cs_intros]:
  assumes "a = 𝔬" and "b = 𝔞"
  shows "𝔤 : a ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_sspan_𝔤) 

lemma (in cf_sspan) cf_sspan_𝔤''[cat_ss_cs_intros]:
  assumes "g = 𝔤" and "a = 𝔞"
  shows "g : 𝔬 ↦⇘ℭ⇙ a"
  unfolding assms by (rule cf_sspan_𝔤) 

lemma (in cf_sspan) cf_sspan_𝔤'''[cat_ss_cs_intros]:
  assumes "g = 𝔤" and "a = 𝔬"
  shows "g : a ↦⇘ℭ⇙ 𝔞"
  unfolding assms by (rule cf_sspan_𝔤) 

lemma (in cf_sspan) cf_sspan_𝔣'[cat_ss_cs_intros]:
  assumes "a = 𝔬" and "b = 𝔟"
  shows "𝔣 : a ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_sspan_𝔣) 

lemma (in cf_sspan) cf_sspan_𝔣''[cat_ss_cs_intros]:
  assumes "f = 𝔣" and "b = 𝔟"
  shows "f : 𝔬 ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_sspan_𝔣) 

lemma (in cf_sspan) cf_sspan_𝔣'''[cat_ss_cs_intros]:
  assumes "f = 𝔣" and "b = 𝔬"
  shows "f : b ↦⇘ℭ⇙ 𝔟"
  unfolding assms by (rule cf_sspan_𝔣) 


text‹Rules.›

lemmas (in cf_scospan) [cat_ss_cs_intros] = cf_scospan_axioms

mk_ide rf cf_scospan_def[unfolded cf_scospan_axioms_def]
  |intro cf_scospanI|
  |dest cf_scospanD[dest]|
  |elim cf_scospanE[elim]|

lemmas [cat_ss_cs_intros] = cf_scospanD(1)

lemmas (in cf_sspan) [cat_ss_cs_intros] = cf_sspan_axioms

mk_ide rf cf_sspan_def[unfolded cf_sspan_axioms_def]
  |intro cf_sspanI|
  |dest cf_sspanD[dest]|
  |elim cf_sspanE[elim]|


text‹Duality.›

lemma (in cf_scospan) cf_sspan_op[cat_op_intros]: 
  "cf_sspan α 𝔞 𝔤 𝔬 𝔣 𝔟 (op_cat ℭ)"
  by (intro cf_sspanI, unfold cat_op_simps)
    (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_ss_cs_intros)+ 

lemmas [cat_op_intros] = cf_scospan.cf_sspan_op

lemma (in cf_sspan) cf_scospan_op[cat_op_intros]: 
  "cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 (op_cat ℭ)"
  by (intro cf_scospanI, unfold cat_op_simps)
    (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_ss_cs_intros)+ 

lemmas [cat_op_intros] = cf_sspan.cf_scospan_op



subsection‹Functors from ‹→∙←› and ‹←∙→››


subsubsection‹Definition and elementary properties›

definition the_cf_scospan :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V" 
  (‹⟨_→_→_←_←_⟩⇩C⇩Fı› [51, 51, 51, 51, 51] 999)
  where "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ =
    [
      (
        λa∈⇩∘→∙←⇩C⦇Obj⦈.
         if a = 𝔞⇩S⇩S ⇒ 𝔞
          | a = 𝔟⇩S⇩S ⇒ 𝔟
          | otherwise ⇒ 𝔬
      ),
      (
        λf∈⇩∘→∙←⇩C⦇Arr⦈.
         if f = 𝔞⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔞⦈
          | f = 𝔟⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔟⦈
          | f = 𝔤⇩S⇩S ⇒ 𝔤
          | f = 𝔣⇩S⇩S ⇒ 𝔣
          | otherwise ⇒ ℭ⦇CId⦈⦇𝔬⦈
      ),
      →∙←⇩C,
      ℭ
    ]⇩∘"

definition the_cf_sspan :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V" 
  (‹⟨_←_←_→_→_⟩⇩C⇩Fı› [51, 51, 51, 51, 51] 999)
  where "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ =
    [
      (
        λa∈⇩∘←∙→⇩C⦇Obj⦈.
         if a = 𝔞⇩S⇩S ⇒ 𝔞
          | a = 𝔟⇩S⇩S ⇒ 𝔟
          | otherwise ⇒ 𝔬
      ),
      (
        λf∈⇩∘←∙→⇩C⦇Arr⦈.
         if f = 𝔞⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔞⦈
          | f = 𝔟⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔟⦈
          | f = 𝔤⇩S⇩S ⇒ 𝔤
          | f = 𝔣⇩S⇩S ⇒ 𝔣
          | otherwise ⇒ ℭ⦇CId⦈⦇𝔬⦈
      ),
      ←∙→⇩C,
      ℭ
    ]⇩∘"


text‹Components.›

lemma the_cf_scospan_components:
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈ =
    (
      λa∈⇩∘→∙←⇩C⦇Obj⦈.
       if a = 𝔞⇩S⇩S ⇒ 𝔞
        | a = 𝔟⇩S⇩S ⇒ 𝔟
        | otherwise ⇒ 𝔬
    )"
    and "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈ =
      (
        λf∈⇩∘→∙←⇩C⦇Arr⦈.
         if f = 𝔞⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔞⦈
          | f = 𝔟⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔟⦈
          | f = 𝔤⇩S⇩S ⇒ 𝔤
          | f = 𝔣⇩S⇩S ⇒ 𝔣
          | otherwise ⇒ ℭ⦇CId⦈⦇𝔬⦈
      )"
    and [cat_ss_cs_simps]: "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇HomDom⦈ = →∙←⇩C"
    and [cat_ss_cs_simps]: "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇HomCod⦈ = ℭ"
  unfolding the_cf_scospan_def dghm_field_simps by (simp_all add: nat_omega_simps)

lemma the_cf_sspan_components:
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈ =
    (
      λa∈⇩∘←∙→⇩C⦇Obj⦈.
       if a = 𝔞⇩S⇩S ⇒ 𝔞
        | a = 𝔟⇩S⇩S ⇒ 𝔟
        | otherwise ⇒ 𝔬
    )"
    and "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈ =
      (
        λf∈⇩∘←∙→⇩C⦇Arr⦈.
         if f = 𝔞⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔞⦈
          | f = 𝔟⇩S⇩S ⇒ ℭ⦇CId⦈⦇𝔟⦈
          | f = 𝔤⇩S⇩S ⇒ 𝔤
          | f = 𝔣⇩S⇩S ⇒ 𝔣
          | otherwise ⇒ ℭ⦇CId⦈⦇𝔬⦈
      )"
    and [cat_ss_cs_simps]: "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇HomDom⦈ = ←∙→⇩C"
    and [cat_ss_cs_simps]: "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇HomCod⦈ = ℭ"
  unfolding the_cf_sspan_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Elementary properties.›

lemma the_cf_scospan_components_vsv[cat_ss_cs_intros]: "vsv (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙)"
  unfolding the_cf_scospan_def by auto

lemma the_cf_sspan_components_vsv[cat_ss_cs_intros]: "vsv (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙)"
  unfolding the_cf_sspan_def by auto


subsubsection‹Object map.›

mk_VLambda the_cf_scospan_components(1)
  |vsv the_cf_scospan_ObjMap_vsv[cat_ss_cs_intros]|
  |vdomain the_cf_scospan_ObjMap_vdomain[cat_ss_cs_simps]|
  |app the_cf_scospan_ObjMap_app|

lemma the_cf_scospan_ObjMap_app_𝔞[cat_ss_cs_simps]:
  assumes "x = 𝔞⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇x⦈ = 𝔞"
  by 
    (
      cs_concl 
        cs_simp: the_cf_scospan_ObjMap_app V_cs_simps assms
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ObjMap_app_𝔟[cat_ss_cs_simps]:
  assumes "x = 𝔟⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇x⦈ = 𝔟"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_scospan_ObjMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ObjMap_app_𝔬[cat_ss_cs_simps]:
  assumes "x = 𝔬⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇x⦈ = 𝔬"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_scospan_ObjMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ObjMap_vrange:
  "ℛ⇩∘ (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof
  (
    intro vsv.vsv_vrange_vsubset, 
    unfold the_cf_scospan_ObjMap_vdomain, 
    intro the_cf_scospan_ObjMap_vsv
  )
  fix a assume "a ∈⇩∘ →∙←⇩C⦇Obj⦈"
  then consider ‹a = 𝔞⇩S⇩S› | ‹a = 𝔟⇩S⇩S› | ‹a = 𝔬⇩S⇩S› 
    unfolding the_cat_scospan_components by auto
  then show "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇a⦈ ∈⇩∘ ℭ⦇Obj⦈"
    by cases 
      (
        cs_concl 
          cs_simp: cat_ss_cs_simps cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
qed

mk_VLambda the_cf_sspan_components(1)
  |vsv the_cf_sspan_ObjMap_vsv[cat_ss_cs_intros]|
  |vdomain the_cf_sspan_ObjMap_vdomain[cat_ss_cs_simps]|
  |app the_cf_sspan_ObjMap_app|

lemma the_cf_sspan_ObjMap_app_𝔞[cat_ss_cs_simps]:
  assumes "x = 𝔞⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇x⦈ = 𝔞"
  by 
    (
      cs_concl  
        cs_simp: the_cf_sspan_ObjMap_app V_cs_simps assms
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ObjMap_app_𝔟[cat_ss_cs_simps]:
  assumes "x = 𝔟⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇x⦈ = 𝔟"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_sspan_ObjMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ObjMap_app_𝔬[cat_ss_cs_simps]:
  assumes "x = 𝔬⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇x⦈ = 𝔬"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_sspan_ObjMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ObjMap_vrange:
  "ℛ⇩∘ (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof
  (
    intro vsv.vsv_vrange_vsubset, 
    unfold the_cf_sspan_ObjMap_vdomain, 
    intro the_cf_sspan_ObjMap_vsv
  )
  fix a assume "a ∈⇩∘ ←∙→⇩C⦇Obj⦈"
  then consider ‹a = 𝔞⇩S⇩S› | ‹a = 𝔟⇩S⇩S› | ‹a = 𝔬⇩S⇩S› 
    unfolding the_cat_sspan_components by auto
  then show "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇a⦈ ∈⇩∘ ℭ⦇Obj⦈"
    by cases 
      (
        cs_concl  
          cs_simp: cat_ss_cs_simps cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
qed


subsubsection‹Arrow map.›

mk_VLambda the_cf_scospan_components(2)
  |vsv the_cf_scospan_ArrMap_vsv[cat_ss_cs_intros]|
  |vdomain the_cf_scospan_ArrMap_vdomain[cat_ss_cs_simps]|
  |app the_cf_scospan_ArrMap_app|

lemma (in cf_scospan) the_cf_scospan_ArrMap_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔬⦈"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_scospan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ArrMap_app_𝔞[cat_ss_cs_simps]:
  assumes "f = 𝔞⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔞⦈"
  using cat_ss_ineq
  by 
    (
      cs_concl
        cs_simp: V_cs_simps the_cf_scospan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ArrMap_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔟⦈"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_scospan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ArrMap_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = 𝔤"
  using cat_ss_ineq
  by 
    (
      cs_concl 
        cs_simp: V_cs_simps the_cf_scospan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ArrMap_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣⇩S⇩S"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = 𝔣"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_scospan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_scospan) the_cf_scospan_ArrMap_vrange:
  "ℛ⇩∘ (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof
  (
    intro vsv.vsv_vrange_vsubset, 
    unfold the_cf_scospan_ArrMap_vdomain, 
    intro the_cf_scospan_ArrMap_vsv
  )
  fix a assume "a ∈⇩∘ →∙←⇩C⦇Arr⦈"
  then consider ‹a = 𝔞⇩S⇩S› | ‹a = 𝔟⇩S⇩S› | ‹a = 𝔬⇩S⇩S› | ‹a = 𝔤⇩S⇩S› | ‹a = 𝔣⇩S⇩S› 
    unfolding the_cat_scospan_components by auto
  then show "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇a⦈ ∈⇩∘ ℭ⦇Arr⦈"
    by cases 
      (
        cs_concl  
          cs_simp: cat_ss_cs_simps cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
qed

mk_VLambda the_cf_sspan_components(2)
  |vsv the_cf_sspan_ArrMap_vsv[cat_ss_cs_intros]|
  |vdomain the_cf_sspan_ArrMap_vdomain[cat_ss_cs_simps]|
  |app the_cf_sspan_ArrMap_app|

lemma (in cf_sspan) the_cf_sspan_ArrMap_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔬⦈"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_sspan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ArrMap_app_𝔞[cat_ss_cs_simps]:
  assumes "f = 𝔞⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔞⦈"
  using cat_ss_ineq
  by 
    (
      cs_concl 
        cs_simp: V_cs_simps the_cf_sspan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ArrMap_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔟⦈"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_sspan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ArrMap_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = 𝔤"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_sspan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ArrMap_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣⇩S⇩S"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ = 𝔣"
  using cat_ss_ineq
  by 
    (
      cs_concl  
        cs_simp: V_cs_simps the_cf_sspan_ArrMap_app assms 
        cs_intro: cat_ss_cs_intros
    )

lemma (in cf_sspan) the_cf_sspan_ArrMap_vrange:
  "ℛ⇩∘ (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof
  (
    intro vsv.vsv_vrange_vsubset,
    unfold the_cf_sspan_ArrMap_vdomain,
    intro the_cf_sspan_ArrMap_vsv
  )
  fix a assume "a ∈⇩∘ ←∙→⇩C⦇Arr⦈"
  then consider ‹a = 𝔞⇩S⇩S› | ‹a = 𝔟⇩S⇩S› | ‹a = 𝔬⇩S⇩S› | ‹a = 𝔤⇩S⇩S› | ‹a = 𝔣⇩S⇩S› 
    unfolding the_cat_sspan_components by auto
  then show "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇a⦈ ∈⇩∘ ℭ⦇Arr⦈"
    by cases
      (
        cs_concl 
          cs_simp: cat_ss_cs_simps cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
qed


subsubsection‹Functor from ‹→∙←› is a functor›

lemma (in cf_scospan) cf_scospan_the_cf_scospan_is_tm_functor:
  "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : →∙←⇩C ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof(intro is_functor.cf_is_tm_functor_if_HomDom_finite_category is_functorI')
  show "vfsequence (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙)" 
    unfolding the_cf_scospan_def by auto
  show "vcard (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙) = 4⇩ℕ"
    unfolding the_cf_scospan_def by (simp add: nat_omega_simps)
  show "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈ :
    ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇b⦈"
    if "f : a ↦⇘→∙←⇩C⇙ b" for a b f
    using that
    by (cases rule: the_cat_scospan_is_arrE; simp only:)
      (
        cs_concl  
          cs_simp: cat_ss_cs_simps cs_intro: cat_cs_intros cat_ss_cs_intros
      )+
  show "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇g ∘⇩A⇘→∙←⇩C⇙ f⦈ =
    ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘→∙←⇩C⇙ c" and "f : a ↦⇘→∙←⇩C⇙ b" for b c g a f
    using that
    by (elim the_cat_scospan_is_arrE) (*very slow*)
      (
        all‹simp only:›, 
        all‹
          solves‹simp add: cat_ss_ineq cat_ss_ineq[symmetric]› | 
          cs_concl  
            cs_simp: cat_cs_simps cat_ss_cs_simps 
            cs_intro: cat_cs_intros cat_ss_cs_intros
          ›
      )
  show 
    "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ArrMap⦈⦇→∙←⇩C⦇CId⦈⦇c⦈⦈ =
      ℭ⦇CId⦈⦇⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙⦇ObjMap⦈⦇c⦈⦈"
    if "c ∈⇩∘ →∙←⇩C⦇Obj⦈" for c
    using that
    by (elim the_cat_scospan_ObjE; simp only:)
      (
        cs_concl
          cs_simp: V_cs_simps cat_ss_cs_simps 
          cs_intro: V_cs_intros cat_ss_cs_intros
      )+

qed
  (
    cs_concl 
      cs_simp: cat_ss_cs_simps
      cs_intro: 
        the_cf_scospan_ObjMap_vrange
        cat_ss_cs_intros cat_cs_intros cat_small_cs_intros
  )+

lemma (in cf_scospan) cf_scospan_the_cf_scospan_is_tm_functor':
  assumes "𝔄' = →∙←⇩C" and "ℭ' = ℭ"
  shows "⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙ : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ'"
  unfolding assms by (rule cf_scospan_the_cf_scospan_is_tm_functor)

lemmas [cat_ss_cs_intros] = cf_scospan.cf_scospan_the_cf_scospan_is_tm_functor


subsubsection‹Duality for the functors from ‹→∙←› and ‹←∙→››

lemma op_cf_cf_scospan[cat_op_simps]: 
  "op_cf (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙) = ⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘op_cat ℭ⇙"
proof-
  have dom_lhs: "𝒟⇩∘ (op_cf (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙)) = 4⇩ℕ" 
    unfolding op_cf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘op_cat ℭ⇙) = 4⇩ℕ" 
    unfolding the_cf_sspan_def by (simp add: nat_omega_simps)
  show ?thesis
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "op_cf (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘ℭ⇙)⦇a⦈ = ⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘op_cat ℭ⇙⦇a⦈"
      if "a ∈⇩∘ 4⇩ℕ" for a
      using that
      by 
        (
          elim_in_numeral, 
          fold dghm_field_simps, 
          unfold cat_op_simps the_cf_sspan_components the_cf_scospan_components
        )
        (
          simp_all add: 
            the_cat_scospan_components(1,2)
            the_cat_sspan_components(1,2)
            cat_op_simps
        )
  qed (auto intro: cat_op_intros cat_ss_cs_intros)
qed

lemma (in 𝒵) op_cf_cf_scospan[cat_op_simps]: 
  "op_cf (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙) = ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘op_cat ℭ⇙"
proof-
  have dom_lhs: "𝒟⇩∘ (op_cf (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙)) = 4⇩ℕ" 
    unfolding op_cf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘op_cat ℭ⇙) = 4⇩ℕ" 
    unfolding the_cf_scospan_def by (simp add: nat_omega_simps)
  show ?thesis
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    show "op_cf (⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙)⦇a⦈ = ⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘op_cat ℭ⇙⦇a⦈"
      if "a ∈⇩∘ 4⇩ℕ" for a
      using that
      by 
        (
          elim_in_numeral, 
          fold dghm_field_simps, 
          unfold cat_op_simps the_cf_sspan_components the_cf_scospan_components
        )
        (
          simp_all add: 
            the_cat_scospan_components(1,2)
            the_cat_sspan_components(1,2)
            cat_op_simps
        )
  qed (auto intro: cat_op_intros cat_ss_cs_intros)
qed

lemmas [cat_op_simps] = 𝒵.op_cf_cf_scospan


subsubsection‹Functor from ‹←∙→› is a functor›

lemma (in cf_sspan) cf_sspan_the_cf_sspan_is_tm_functor:
  "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ : ←∙→⇩C ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof-
  interpret scospan: cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 ‹op_cat ℭ› by (rule cf_scospan_op)
  interpret scospan:
    is_tm_functor α ‹→∙←⇩C› ‹op_cat ℭ› ‹⟨𝔞→𝔤→𝔬←𝔣←𝔟⟩⇩C⇩F⇘op_cat ℭ⇙›
    by (rule scospan.cf_scospan_the_cf_scospan_is_tm_functor)
  show ?thesis by (rule scospan.is_tm_functor_op[unfolded cat_op_simps])
qed

lemma (in cf_sspan) cf_sspan_the_cf_sspan_is_tm_functor':
  assumes "𝔄' = ←∙→⇩C" and "ℭ' = ℭ"
  shows "⟨𝔞←𝔤←𝔬→𝔣→𝔟⟩⇩C⇩F⇘ℭ⇙ : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ'"
  unfolding assms by (rule cf_sspan_the_cf_sspan_is_tm_functor)

lemmas [cat_ss_cs_intros] = cf_sspan.cf_sspan_the_cf_sspan_is_tm_functor

text‹\newpage›

end