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 𝔬SS where [cat_ss_elem_simps]: "𝔬SS = 0"
definition 𝔞SS where [cat_ss_elem_simps]: "𝔞SS = 1"
definition 𝔟SS where [cat_ss_elem_simps]: "𝔟SS = 2"
definition 𝔤SS where [cat_ss_elem_simps]: "𝔤SS = 3"
definition 𝔣SS where [cat_ss_elem_simps]: "𝔣SS = 4"

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

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



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

abbreviation cat_scospan_composable :: V
  where "cat_scospan_composable  
    (set {𝔬SS} × set {𝔬SS, 𝔤SS, 𝔣SS})  
    (set {𝔤SS, 𝔞SS} × set {𝔞SS})  
    (set {𝔣SS, 𝔟SS} × set {𝔟SS})"

abbreviation cat_sspan_composable :: V
  where "cat_sspan_composable  (cat_scospan_composable)¯"


text‹Rules.›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma cat_sspan_composableE:
  assumes "[g, f]  cat_sspan_composable"
  obtains "g = 𝔬SS" and "f = 𝔬SS" 
        | "g = 𝔤SS" and "f = 𝔬SS"
        | "g = 𝔣SS" and "f = 𝔬SS"
        | "g = 𝔞SS" and "f = 𝔤SS"
        | "g = 𝔟SS" and "f = 𝔣SS"
        | "g = 𝔞SS" and "f = 𝔞SS"
        | "g = 𝔟SS" and "f = 𝔟SS"
  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 {𝔞SS, 𝔟SS, 𝔬SS},
      set {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS},
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | x = 𝔤SS  𝔞SS
          | x = 𝔣SS  𝔟SS
          | otherwise  𝔬SS
      ),
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | otherwise  𝔬SS
      ),
      (
        λgfcat_scospan_composable. 
         if gf = [𝔬SS, 𝔤SS]  𝔤SS
          | gf = [𝔬SS, 𝔣SS]  𝔣SS
          | otherwise  gf0
      ),
      vid_on (set {𝔞SS, 𝔟SS, 𝔬SS})
    ]"

definition the_cat_sspan :: V (←∙→C)
  where "←∙→C =
    [
      set {𝔞SS, 𝔟SS, 𝔬SS},
      set {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS},
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | otherwise  𝔬SS
      ),
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | x = 𝔤SS  𝔞SS
          | x = 𝔣SS  𝔟SS
          | otherwise  𝔬SS
      ),
      (
        λgfcat_sspan_composable. 
         if gf = [𝔞SS, 𝔤SS]  𝔤SS
          | gf = [𝔟SS, 𝔣SS]  𝔣SS
          | otherwise  gf0
      ),
      vid_on (set {𝔞SS, 𝔟SS, 𝔬SS})
    ]"


text‹Components.›

lemma the_cat_scospan_components: 
  shows "→∙←CObj = set {𝔞SS, 𝔟SS, 𝔬SS}"
    and "→∙←CArr = set {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}"
    and "→∙←CDom = 
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | x = 𝔤SS  𝔞SS
          | x = 𝔣SS  𝔟SS
          | otherwise  𝔬SS
      )"
    and "→∙←CCod = 
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | otherwise  𝔬SS
      )"
    and "→∙←CComp =
      (
        λgfcat_scospan_composable. 
         if gf = [𝔬SS, 𝔤SS]  𝔤SS
          | gf = [𝔬SS, 𝔣SS]  𝔣SS
          | otherwise  gf0
      )"
    and "→∙←CCId = vid_on (set {𝔞SS, 𝔟SS, 𝔬SS})"
  unfolding the_cat_scospan_def dg_field_simps by (simp_all add: nat_omega_simps)

lemma the_cat_sspan_components: 
  shows "←∙→CObj = set {𝔞SS, 𝔟SS, 𝔬SS}"
    and "←∙→CArr = set {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}"
    and "←∙→CDom =
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | otherwise  𝔬SS
      )"
    and "←∙→CCod =
      (
        λxset {𝔞SS, 𝔤SS, 𝔬SS, 𝔣SS, 𝔟SS}. 
         if x = 𝔞SS  𝔞SS
          | x = 𝔟SS  𝔟SS
          | x = 𝔤SS  𝔞SS
          | x = 𝔣SS  𝔟SS
          | otherwise  𝔬SS
      )"
    and "←∙→CComp =
      (
        λgfcat_sspan_composable. 
         if gf = [𝔞SS, 𝔤SS]  𝔤SS
          | gf = [𝔟SS, 𝔣SS]  𝔣SS
          | otherwise  gf0
      )"
    and "←∙→CCId = vid_on (set {𝔞SS, 𝔟SS, 𝔬SS})"
  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 = 𝔬SS"
  shows "a  →∙←CObj"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Obj_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞SS"
  shows "a  →∙←CObj"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Obj_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟SS"
  shows "a  →∙←CObj"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_ObjE:
  assumes "a  →∙←CObj"
  obtains a = 𝔬SS | a = 𝔞SS | a = 𝔟SS
  using assms unfolding the_cat_scospan_components by auto

lemma the_cat_sspan_Obj_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬SS"
  shows "a  ←∙→CObj"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Obj_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞SS"
  shows "a  ←∙→CObj"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Obj_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟SS"
  shows "a  ←∙→CObj"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_ObjE:
  assumes "a  ←∙→CObj"
  obtains a = 𝔬SS | a = 𝔞SS | a = 𝔟SS
  using assms unfolding the_cat_sspan_components by auto


subsubsection‹Arrows›

lemma the_cat_scospan_Arr_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞SS"
  shows "a  →∙←CArr"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟SS"
  shows "a  →∙←CArr"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬SS"
  shows "a  →∙←CArr"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔤I[cat_ss_cs_intros]:
  assumes "a = 𝔤SS"
  shows "a  →∙←CArr"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_Arr_𝔣I[cat_ss_cs_intros]:
  assumes "a = 𝔣SS"
  shows "a  →∙←CArr"
  using assms unfolding the_cat_scospan_components by simp

lemma the_cat_scospan_ArrE:
  assumes "f  →∙←CArr"
  obtains f = 𝔞SS | f = 𝔟SS | f = 𝔬SS | f = 𝔤SS | f = 𝔣SS 
  using assms unfolding the_cat_scospan_components by auto

lemma the_cat_sspan_Arr_𝔞I[cat_ss_cs_intros]:
  assumes "a = 𝔞SS"
  shows "a  ←∙→CArr"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔟I[cat_ss_cs_intros]:
  assumes "a = 𝔟SS"
  shows "a  ←∙→CArr"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔬I[cat_ss_cs_intros]:
  assumes "a = 𝔬SS"
  shows "a  ←∙→CArr"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔤I[cat_ss_cs_intros]:
  assumes "a = 𝔤SS"
  shows "a  ←∙→CArr"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_Arr_𝔣I[cat_ss_cs_intros]:
  assumes "a = 𝔣SS"
  shows "a  ←∙→CArr"
  using assms unfolding the_cat_sspan_components by simp

lemma the_cat_sspan_ArrE:
  assumes "f  ←∙→CArr"
  obtains f = 𝔞SS | f = 𝔟SS | f = 𝔬SS | f = 𝔤SS | f = 𝔣SS 
  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 = 𝔞SS"
  shows "→∙←CDomf = 𝔞SS"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Dom_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟SS"
  shows "→∙←CDomf = 𝔟SS"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Dom_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬SS"
  shows "→∙←CDomf = 𝔬SS"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Dom_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤SS"
  shows "→∙←CDomf = 𝔞SS"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Dom_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣SS"
  shows "→∙←CDomf = 𝔟SS"
  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 = 𝔞SS"
  shows "←∙→CDomf = 𝔞SS"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Dom_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟SS"
  shows "←∙→CDomf = 𝔟SS"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Dom_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬SS"
  shows "←∙→CDomf = 𝔬SS"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Dom_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤SS"
  shows "←∙→CDomf = 𝔬SS"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Dom_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣SS"
  shows "←∙→CDomf = 𝔬SS"
  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 = 𝔞SS"
  shows "→∙←CCodf = 𝔞SS"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Cod_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟SS"
  shows "→∙←CCodf = 𝔟SS"
  unfolding the_cat_scospan_components assms by simp

lemma the_cat_scospan_Cod_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬SS"
  shows "→∙←CCodf = 𝔬SS"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Cod_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤SS"
  shows "→∙←CCodf = 𝔬SS"
  unfolding the_cat_scospan_components assms using cat_ss_ineq by auto

lemma the_cat_scospan_Cod_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣SS"
  shows "→∙←CCodf = 𝔬SS"
  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 = 𝔞SS"
  shows "←∙→CCodf = 𝔞SS"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Cod_app_𝔟[cat_ss_cs_simps]:
  assumes "f = 𝔟SS"
  shows "←∙→CCodf = 𝔟SS"
  unfolding the_cat_sspan_components assms by simp

lemma the_cat_sspan_Cod_app_𝔬[cat_ss_cs_simps]:
  assumes "f = 𝔬SS"
  shows "←∙→CCodf = 𝔬SS"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Cod_app_𝔤[cat_ss_cs_simps]:
  assumes "f = 𝔤SS"
  shows "←∙→CCodf = 𝔞SS"
  unfolding the_cat_sspan_components assms using cat_ss_ineq by auto

lemma the_cat_sspan_Cod_app_𝔣[cat_ss_cs_simps]:
  assumes "f = 𝔣SS"
  shows "←∙→CCodf = 𝔟SS"
  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 = 𝔞SS" and "f = 𝔞SS"
  shows "g A→∙←Cf = g" "g A→∙←Cf = f"
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  with assms show "g A→∙←Cf = g" "g A→∙←Cf = 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 = 𝔟SS" and "f = 𝔟SS"
  shows "g A→∙←Cf = g" "g A→∙←Cf = f"
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  with assms show "g A→∙←Cf = g" "g A→∙←Cf = 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 = 𝔬SS" and "f = 𝔬SS"
  shows "g A→∙←Cf = g" "g A→∙←Cf = f"
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  with assms show "g A→∙←Cf = g" "g A→∙←Cf = 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 = 𝔬SS" and "f = 𝔤SS"
  shows "g A→∙←Cf = f" 
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  then show "g A→∙←Cf = 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 = 𝔬SS" and "f = 𝔣SS"
  shows "g A→∙←Cf = f" 
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  then show "g A→∙←Cf = 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 = 𝔤SS" and "f = 𝔞SS"
  shows "g A→∙←Cf = g"  
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  then show "g A→∙←Cf = 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 = 𝔣SS" and "f = 𝔟SS"
  shows "g A→∙←Cf = g"  
proof-
  from assms have "[g, f]  cat_scospan_composable" by auto
  then show "g A→∙←Cf = 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 = 𝔞SS" and "f = 𝔞SS"
  shows "g A←∙→Cf = g" "g A←∙→Cf = f"
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  with assms show "g A←∙→Cf = g" "g A←∙→Cf = 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 = 𝔟SS" and "f = 𝔟SS"
  shows "g A←∙→Cf = g" "g A←∙→Cf = f"
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  with assms show "g A←∙→Cf = g" "g A←∙→Cf = 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 = 𝔬SS" and "f = 𝔬SS"
  shows "g A←∙→Cf = g" "g A←∙→Cf = f"
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  with assms show "g A←∙→Cf = g" "g A←∙→Cf = 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 = 𝔞SS" and "f = 𝔤SS"
  shows "g A←∙→Cf = f" 
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  then show "g A←∙→Cf = 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 = 𝔟SS" and "f = 𝔣SS"
  shows "g A←∙→Cf = f" 
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  then show "g A←∙→Cf = 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 = 𝔤SS" and "f = 𝔬SS"
  shows "g A←∙→Cf = g"  
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  then show "g A←∙→Cf = 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 = 𝔣SS" and "f = 𝔬SS"
  shows "g A←∙→Cf = g"  
proof-
  from assms have "[g, f]  cat_sspan_composable" by auto
  then show "g A←∙→Cf = 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' = 𝔞SS" and "b' = 𝔞SS" and "f = 𝔞SS"
  shows "f : a' →∙←Cb'"
proof(intro is_arrI, unfold assms)
  show "→∙←CDom𝔞SS = 𝔞SS" "→∙←CCod𝔞SS = 𝔞SS"
    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' = 𝔟SS" and "b' = 𝔟SS" and "f = 𝔟SS"
  shows "f : a' →∙←Cb'"
proof(intro is_arrI, unfold assms)
  show "→∙←CDom𝔟SS = 𝔟SS" "→∙←CCod𝔟SS = 𝔟SS"
    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' = 𝔬SS" and "b' = 𝔬SS" and "f = 𝔬SS"
  shows "f : a' →∙←Cb'"
proof(intro is_arrI, unfold assms)
  show "→∙←CDom𝔬SS = 𝔬SS" "→∙←CCod𝔬SS = 𝔬SS"
    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' = 𝔞SS" and "b' = 𝔬SS" and "f = 𝔤SS"
  shows "f : a' →∙←Cb'"
proof(intro is_arrI, unfold assms)
  show "→∙←CDom𝔤SS = 𝔞SS" "→∙←CCod𝔤SS = 𝔬SS"
    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' = 𝔟SS" and "b' = 𝔬SS" and "f = 𝔣SS"
  shows "f : a' →∙←Cb'"
proof(intro is_arrI, unfold assms)
  show "→∙←CDom𝔣SS = 𝔟SS" "→∙←CCod𝔣SS = 𝔬SS"
    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' →∙←Cb'"
  obtains "a' = 𝔞SS" and "b' = 𝔞SS" and "f' = 𝔞SS"
        | "a' = 𝔟SS" and "b' = 𝔟SS" and "f' = 𝔟SS"
        | "a' = 𝔬SS" and "b' = 𝔬SS" and "f' = 𝔬SS"
        | "a' = 𝔞SS" and "b' = 𝔬SS" and "f' = 𝔤SS"
        | "a' = 𝔟SS" and "b' = 𝔬SS" and "f' = 𝔣SS"
proof-
  note f = is_arrD[OF assms]
  from f(1) consider (𝔞SS) f' = 𝔞SS 
                   | (𝔟SS) f' = 𝔟SS 
                   | (𝔬SS) f' = 𝔬SS 
                   | (𝔤SS) f' = 𝔤SS 
                   | (𝔣SS) f' = 𝔣SS 
    by (elim the_cat_scospan_ArrE)
  then show ?thesis
  proof cases
    case 𝔞SS
    moreover from f(2,3)[unfolded 𝔞SS, symmetric] have "a' = 𝔞SS" "b' = 𝔞SS"
      by (simp_all add: cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔟SS
    moreover from f(2,3)[unfolded 𝔟SS, symmetric] have "a' = 𝔟SS" "b' = 𝔟SS"
      by (simp_all add: cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔬SS
    moreover from f(2,3)[unfolded 𝔬SS, symmetric] have "a' = 𝔬SS" "b' = 𝔬SS"
      by (simp_all add: cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔤SS
    moreover have "a' = 𝔞SS" "b' = 𝔬SS"
      by (simp_all add: f(2,3)[unfolded 𝔤SS, symmetric] cat_ss_cs_simps)
    ultimately show ?thesis using that by auto
  next
    case 𝔣SS
    moreover have "a' = 𝔟SS" "b' = 𝔬SS"
      by (simp_all add: f(2,3)[unfolded 𝔣SS, 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 " (→∙←CDom)  →∙←CObj" by (auto simp: the_cat_scospan_components)
  show " (→∙←CCod)  →∙←CObj" by (auto simp: the_cat_scospan_components)
  show "(gf  𝒟 (→∙←CComp)) =
    (g f b c a. gf = [g, f]  g : b →∙←Cc  f : a →∙←Cb)"
    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 →∙←Cc  f : a →∙←Cb"
      unfolding gf_def
      by (*slow*)
        (
          cases rule: cat_scospan_composableE; 
          (intro exI conjI)?; 
          cs_concl_step?;
          (simp only:)?,
          allintro 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' →∙←Cc'  f : a' →∙←Cb'"
    then obtain g f b c a
      where gf_def: "gf = [g, f]"
        and g: "g : b →∙←Cc"
        and f: "f : a →∙←Cb"
      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 "𝒟 (→∙←CCId) = →∙←CObj"
    by (simp add: cat_ss_cs_simps the_cat_scospan_components)
  show "g A→∙←Cf : a →∙←Cc"
    if "g : b →∙←Cc" and "f : a →∙←Cb" for b c g a f
    using that
    by (elim the_cat_scospan_is_arrE; simp only:)
      (
        allsolvessimp 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→∙←Cg A→∙←Cf = h A→∙←C(g A→∙←Cf)"
    if "h : c →∙←Cd" and "g : b →∙←Cc" and "f : a →∙←Cb"
    for c d h b g a f
    using that 
    by (elim the_cat_scospan_is_arrE; simp only:) (*slow*)
      (
        allsolvessimp only: cat_ss_ineq cat_ss_ineq[symmetric] | 
          cs_concl cs_simp: cat_ss_cs_simps cs_intro: cat_ss_cs_intros
      )
  show "→∙←CCIda : a →∙←Ca" if "a  →∙←CObj" for a
    using that
    by (elim the_cat_scospan_ObjE) 
      (
        allcs_concl 
            cs_simp: V_cs_simps cat_ss_cs_simps
            cs_intro: V_cs_intros cat_ss_cs_intros
      )
  show "→∙←CCIdb A→∙←Cf = f" if "f : a →∙←Cb" 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→∙←CCIdb = f" if "f : b →∙←Cc" 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 = ←∙→Ca" for a
    proof
      (
        elim_in_numeral,
        fold dg_field_simps,
        unfold op_cat_components;
        rule sym
      )
      show "←∙→CComp = fflip (→∙←CComp)"
      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←∙→Cf = f A→∙←Cg"
          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 
          "←∙→CCompgf = fflip (→∙←CComp)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" 
  (_____CFı› [51, 51, 51, 51, 51] 999)
  where "𝔞𝔤𝔬𝔣𝔟CF=
    [
      (
        λa→∙←CObj.
         if a = 𝔞SS  𝔞
          | a = 𝔟SS  𝔟
          | otherwise  𝔬
      ),
      (
        λf→∙←CArr.
         if f = 𝔞SS  CId𝔞
          | f = 𝔟SS  CId𝔟
          | f = 𝔤SS  𝔤
          | f = 𝔣SS  𝔣
          | otherwise  CId𝔬
      ),
      →∙←C,
      
    ]"

definition the_cf_sspan :: "V  V  V  V  V  V  V" 
  (_____CFı› [51, 51, 51, 51, 51] 999)
  where "𝔞𝔤𝔬𝔣𝔟CF=
    [
      (
        λa←∙→CObj.
         if a = 𝔞SS  𝔞
          | a = 𝔟SS  𝔟
          | otherwise  𝔬
      ),
      (
        λf←∙→CArr.
         if f = 𝔞SS  CId𝔞
          | f = 𝔟SS  CId𝔟
          | f = 𝔤SS  𝔤
          | f = 𝔣SS  𝔣
          | otherwise  CId𝔬
      ),
      ←∙→C,
      
    ]"


text‹Components.›

lemma the_cf_scospan_components:
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMap =
    (
      λa→∙←CObj.
       if a = 𝔞SS  𝔞
        | a = 𝔟SS  𝔟
        | otherwise  𝔬
    )"
    and "𝔞𝔤𝔬𝔣𝔟CFArrMap =
      (
        λf→∙←CArr.
         if f = 𝔞SS  CId𝔞
          | f = 𝔟SS  CId𝔟
          | f = 𝔤SS  𝔤
          | f = 𝔣SS  𝔣
          | otherwise  CId𝔬
      )"
    and [cat_ss_cs_simps]: "𝔞𝔤𝔬𝔣𝔟CFHomDom = →∙←C"
    and [cat_ss_cs_simps]: "𝔞𝔤𝔬𝔣𝔟CFHomCod = "
  unfolding the_cf_scospan_def dghm_field_simps by (simp_all add: nat_omega_simps)

lemma the_cf_sspan_components:
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMap =
    (
      λa←∙→CObj.
       if a = 𝔞SS  𝔞
        | a = 𝔟SS  𝔟
        | otherwise  𝔬
    )"
    and "𝔞𝔤𝔬𝔣𝔟CFArrMap =
      (
        λf←∙→CArr.
         if f = 𝔞SS  CId𝔞
          | f = 𝔟SS  CId𝔟
          | f = 𝔤SS  𝔤
          | f = 𝔣SS  𝔣
          | otherwise  CId𝔬
      )"
    and [cat_ss_cs_simps]: "𝔞𝔤𝔬𝔣𝔟CFHomDom = ←∙→C"
    and [cat_ss_cs_simps]: "𝔞𝔤𝔬𝔣𝔟CFHomCod = "
  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 (𝔞𝔤𝔬𝔣𝔟CF)"
  unfolding the_cf_scospan_def by auto

lemma the_cf_sspan_components_vsv[cat_ss_cs_intros]: "vsv (𝔞𝔤𝔬𝔣𝔟CF)"
  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 = 𝔞SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMapx = 𝔞"
  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 = 𝔟SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMapx = 𝔟"
  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 = 𝔬SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMapx = 𝔬"
  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:
  " (𝔞𝔤𝔬𝔣𝔟CFObjMap)  Obj"
proof
  (
    intro vsv.vsv_vrange_vsubset, 
    unfold the_cf_scospan_ObjMap_vdomain, 
    intro the_cf_scospan_ObjMap_vsv
  )
  fix a assume "a  →∙←CObj"
  then consider a = 𝔞SS | a = 𝔟SS | a = 𝔬SS 
    unfolding the_cat_scospan_components by auto
  then show "𝔞𝔤𝔬𝔣𝔟CFObjMapa  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 = 𝔞SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMapx = 𝔞"
  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 = 𝔟SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMapx = 𝔟"
  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 = 𝔬SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFObjMapx = 𝔬"
  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:
  " (𝔞𝔤𝔬𝔣𝔟CFObjMap)  Obj"
proof
  (
    intro vsv.vsv_vrange_vsubset, 
    unfold the_cf_sspan_ObjMap_vdomain, 
    intro the_cf_sspan_ObjMap_vsv
  )
  fix a assume "a  ←∙→CObj"
  then consider a = 𝔞SS | a = 𝔟SS | a = 𝔬SS 
    unfolding the_cat_sspan_components by auto
  then show "𝔞𝔤𝔬𝔣𝔟CFObjMapa  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 = 𝔬SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 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 = 𝔞SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 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 = 𝔟SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 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 = 𝔤SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 𝔤"
  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 = 𝔣SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 𝔣"
  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:
  " (𝔞𝔤𝔬𝔣𝔟CFArrMap)  Arr"
proof
  (
    intro vsv.vsv_vrange_vsubset, 
    unfold the_cf_scospan_ArrMap_vdomain, 
    intro the_cf_scospan_ArrMap_vsv
  )
  fix a assume "a  →∙←CArr"
  then consider a = 𝔞SS | a = 𝔟SS | a = 𝔬SS | a = 𝔤SS | a = 𝔣SS 
    unfolding the_cat_scospan_components by auto
  then show "𝔞𝔤𝔬𝔣𝔟CFArrMapa  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 = 𝔬SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 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 = 𝔞SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 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 = 𝔟SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 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 = 𝔤SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 𝔤"
  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 = 𝔣SS"
  shows "𝔞𝔤𝔬𝔣𝔟CFArrMapf = 𝔣"
  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:
  " (𝔞𝔤𝔬𝔣𝔟CFArrMap)  Arr"
proof
  (
    intro vsv.vsv_vrange_vsubset,
    unfold the_cf_sspan_ArrMap_vdomain,
    intro the_cf_sspan_ArrMap_vsv
  )
  fix a assume "a  ←∙→CArr"
  then consider a = 𝔞SS | a = 𝔟SS | a = 𝔬SS | a = 𝔤SS | a = 𝔣SS 
    unfolding the_cat_sspan_components by auto
  then show "𝔞𝔤𝔬𝔣𝔟CFArrMapa  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:
  "𝔞𝔤𝔬𝔣𝔟CF: →∙←C ↦↦C.tmα"
proof(intro is_functor.cf_is_tm_functor_if_HomDom_finite_category is_functorI')
  show "vfsequence (𝔞𝔤𝔬𝔣𝔟CF)" 
    unfolding the_cf_scospan_def by auto
  show "vcard (𝔞𝔤𝔬𝔣𝔟CF) = 4"
    unfolding the_cf_scospan_def by (simp add: nat_omega_simps)
  show "𝔞𝔤𝔬𝔣𝔟CFArrMapf :
    𝔞𝔤𝔬𝔣𝔟CFObjMapa 𝔞𝔤𝔬𝔣𝔟CFObjMapb"
    if "f : a →∙←Cb" 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 "𝔞𝔤𝔬𝔣𝔟CFArrMapg A→∙←Cf =
    𝔞𝔤𝔬𝔣𝔟CFArrMapg A𝔞𝔤𝔬𝔣𝔟CFArrMapf"
    if "g : b →∙←Cc" and "f : a →∙←Cb" for b c g a f
    using that
    by (elim the_cat_scospan_is_arrE) (*very slow*)
      (
        allsimp only:, 
        allsolvessimp 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 
    "𝔞𝔤𝔬𝔣𝔟CFArrMap→∙←CCIdc =
      CId𝔞𝔤𝔬𝔣𝔟CFObjMapc"
    if "c  →∙←CObj" 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 "𝔞𝔤𝔬𝔣𝔟CF: 𝔄' ↦↦C.tmαℭ'"
  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 (𝔞𝔤𝔬𝔣𝔟CF) = 𝔞𝔤𝔬𝔣𝔟CFop_cat ⇙"
proof-
  have dom_lhs: "𝒟 (op_cf (𝔞𝔤𝔬𝔣𝔟CF)) = 4" 
    unfolding op_cf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟 (𝔞𝔤𝔬𝔣𝔟CFop_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 (𝔞𝔤𝔬𝔣𝔟CF)a = 𝔞𝔤𝔬𝔣𝔟CFop_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 (𝔞𝔤𝔬𝔣𝔟CF) = 𝔞𝔤𝔬𝔣𝔟CFop_cat ⇙"
proof-
  have dom_lhs: "𝒟 (op_cf (𝔞𝔤𝔬𝔣𝔟CF)) = 4" 
    unfolding op_cf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟 (𝔞𝔤𝔬𝔣𝔟CFop_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 (𝔞𝔤𝔬𝔣𝔟CF)a = 𝔞𝔤𝔬𝔣𝔟CFop_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:
  "𝔞𝔤𝔬𝔣𝔟CF: ←∙→C ↦↦C.tmα"
proof-
  interpret scospan: cf_scospan α 𝔞 𝔤 𝔬 𝔣 𝔟 op_cat  by (rule cf_scospan_op)
  interpret scospan:
    is_tm_functor α →∙←C op_cat  𝔞𝔤𝔬𝔣𝔟CFop_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 "𝔞𝔤𝔬𝔣𝔟CF: 𝔄' ↦↦C.tmαℭ'"
  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