Theory Omega_Catoid

(* 
Title: Omega-Catoids
Author: Cameron Calk, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹$\omega$-Catoids›

theory Omega_Catoid
  imports "Two_Catoid"

begin

subsection ‹Indexed catoids.›

text ‹We add an index to the operations of catoids.›

class imultimagma = 
  fixes imcomp :: "'a ⇒ nat ⇒ 'a ⇒ 'a set" ("_⊙ ⇘_⇙ _" [70,70,70]70) 

definition (in imultimagma) iconv  :: "'a set ⇒ nat ⇒ 'a set ⇒ 'a set" ("_⋆⇘_⇙_"[70,70,70]70) where
  "X ⋆⇘i⇙ Y = (⋃x ∈ X. ⋃y ∈ Y. x ⊙⇘i⇙ y)"

class imultisemigroup = imultimagma +
  assumes assoc: "(⋃v ∈ y ⊙⇘i⇙ z. x ⊙⇘i⇙ v) = (⋃v ∈ x ⊙⇘i⇙ y. v ⊙⇘i⇙ z)"

begin

sublocale ims: multisemigroup "λx y. x ⊙⇘i⇙ y"
  by unfold_locales (simp add: local.assoc)

abbreviation "DD ≡ ims.Δ"

lemma iconv_prop: "X ⋆⇘i⇙ Y ≡ ims.conv i X Y"
  by (simp add: local.iconv_def multimagma.conv_def)

end

class st_imultimagma = imultimagma + 
 fixes src :: "nat ⇒ 'a ⇒ 'a"
 and tgt :: "nat ⇒ 'a ⇒ 'a"
 assumes Dst: "x ⊙⇘i⇙ y ≠ {} ⟹ tgt i x = src i y"
 and src_absorb [simp]: "(src i x) ⊙⇘i⇙ x = {x}" 
 and tgt_absorb [simp]: "x ⊙⇘i⇙ (tgt i x) = {x}" 

begin

lemma inst: "(src 1 x) ⊙⇘1⇙ x = {x}"
  by simp 

sublocale stimm: st_multimagma "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales (simp_all add: local.Dst)

sublocale stimm0: st_multimagma0 "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales (simp_all add: local.Dst)

sublocale stimm1: st_multimagma1 "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales (simp_all add: local.Dst)

abbreviation "srcfix ≡ stimm.sfix"

abbreviation "tgtfix ≡ stimm.tfix"

abbreviation "Srci ≡ stimm.Src"

abbreviation "Tgti ≡ stimm.Tgt"

end

class icatoid = st_imultimagma + imultisemigroup

sublocale icatoid ⊆ icat: catoid  "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales

class local_icatoid = icatoid +
  assumes src_local: "Srci i (x ⊙⇘i⇙ src i y) ⊆ Srci i (x ⊙⇘i⇙ y)"
  and tgt_local: "Tgti i (tgt i x ⊙⇘i⇙ y) ⊆ Tgti i (x ⊙⇘i⇙ y)"

sublocale local_icatoid ⊆ licat: local_catoid  "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales(simp_all add: local.src_local local.tgt_local)

class functional_imagma = imultimagma + 
  assumes functionality: "x ∈ y ⊙⇘i⇙ z ⟹ x' ∈ y ⊙⇘i⇙ z ⟹ x = x'"

sublocale functional_imagma ⊆ pmi: functional_magma "λx y. x ⊙⇘i⇙ y"
  by unfold_locales(simp add: local.functionality)

class functional_isemigroup = functional_imagma + imultisemigroup

sublocale functional_isemigroup ⊆ psgi: functional_semigroup "λx y. x ⊙⇘i⇙ y"..

class functional_icatoid = functional_isemigroup + icatoid

sublocale functional_icatoid ⊆ psgi: functional_catoid  "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales

class icategory = functional_icatoid + local_icatoid

sublocale icategory ⊆ icatt: single_set_category "λx y. x ⊙⇘i⇙ y" "src i" "tgt i"
  by unfold_locales

subsection ‹$\omega$-Catoids›

text ‹Next we define $\omega$-catoids and $\omega$-categories.›

class omega_st_multimagma = st_imultimagma +
  assumes comm_sisj: "i ≠ j ⟹ src i (src j x) = src j (src i x)"
  and comm_sitj: "i ≠ j ⟹ src i (tgt j x) = tgt j (src i x)"
  and comm_titj: "i ≠ j ⟹ tgt i  (tgt j x) = tgt j (tgt i x)"
  and si_hom: "i ≠ j ⟹ Srci i (x ⊙⇘j⇙ y) ⊆ src i x ⊙⇘j⇙ src i y"
  and ti_hom: "i ≠ j ⟹ Tgti i (x ⊙⇘j⇙ y) ⊆ tgt i x ⊙⇘j⇙ tgt i y"
  and omega_interchange: "i < j ⟹ (w ⊙⇘j⇙ x) ⋆⇘i⇙ (y ⊙⇘j⇙ z) ⊆ (w ⊙⇘i⇙ y) ⋆⇘j⇙ (x ⊙⇘i⇙ z)"
  and sjsi [simp]: "i < j ⟹ src j (src i x) = src i x"
  and sjti [simp]: "i < j ⟹ src j (tgt i x) = tgt i x"
  and tjsi [simp]: "i < j ⟹ tgt j (src i x) = src i x"
  and tjti [simp]: "i < j ⟹ tgt j (tgt i x) = tgt i x"

class omega_catoid = omega_st_multimagma + icatoid

context omega_st_multimagma
begin

lemma omega_interchange_var: "(w ⊙⇘(i + k + 1)⇙ x) ⋆⇘i⇙ (y ⊙⇘(i + k + 1)⇙ z) ⊆ (w ⊙⇘i⇙ y) ⋆⇘(i + k + 1)⇙ (x ⊙⇘i⇙ z)"
  using local.omega_interchange by auto

lemma all_sisj: "src i (src j x) = src j (src i x)"
  by (metis local.comm_sisj)

lemma all_titj: "tgt i (tgt j x) = tgt j (tgt i x)"
  by (metis local.comm_titj)

lemma sjsi_var [simp]: "src (i + k) (src i x) = src i x"
  by (metis le_add1 local.sjsi local.stimm.stopp.tt_idem nless_le)

lemma sjti_var [simp]: "src (i + k) (tgt i x) = tgt i x"
  by (metis local.stimm.stopp.ts_compat sjsi_var)

lemma tjsi_var [simp]: "tgt (i + k) (src i x) = src i x"
  by (simp add: stimm.st_fix)

lemma tjti_var [simp]: "tgt (i + k) (tgt i x) = tgt i x"
  by (simp add: stimm.st_fix)

text ‹The following sublocale statement should help us to translate statements for 2-catoids to 
$\omega$-catoids. But it does not seem to work. Hence we duplicate the work done for 2-catoids, and
later also for semirings and quantales.›

sublocale otmm: two_st_multimagma  
  "λx y. x ⊙⇘i⇙ y"  
  "src i" 
  "tgt i" 
  "λx y. x ⊙⇘(i + k + 1)⇙ y"  
  "src (i + k + 1)" 
  "tgt (i + k + 1)"
  apply unfold_locales
              apply (simp_all add: comm_sisj comm_sitj comm_titj si_hom ti_hom)
  using less_add_Suc1 local.all_sisj local.sjsi apply simp
  apply (metis lessI less_add_Suc1 local.comm_sitj local.sjti not_add_less1)
  apply (metis less_add_Suc1 local.comm_titj local.tjti)
  using local.iconv_def local.omega_interchange local.stimm.conv_def by simp

end

class omega_st_multimagma_strong = omega_st_multimagma +
 assumes sj_hom_strong: "i < j ⟹ Srci j (x ⊙⇘i⇙ y) = src j x ⊙⇘i⇙ src j y"
 and tj_hom_strong: "i < j ⟹ Tgti j (x ⊙⇘i⇙ y) = tgt j x ⊙⇘i⇙ tgt j y"

begin

lemma sj_hom_strong_var: "Srci (i + k + 1) (x ⊙⇘i⇙ y) = src (i + k + 1) x ⊙⇘i⇙ src (i + k + 1) y"
  by (simp add: local.sj_hom_strong)

lemma tj_hom_strong_var: "Tgti (i + k + 1) (x ⊙⇘i⇙ y) = tgt (i + k + 1) x ⊙⇘i⇙ tgt (i + k + 1) y"
  by (simp add: local.tj_hom_strong)

end

sublocale omega_st_multimagma ⊆ olropp: omega_st_multimagma "λ x i y. y ⊙⇘i⇙ x" "tgt" "src"
  apply unfold_locales
  apply (simp_all add: local.Dst)
  using local.comm_titj apply simp
  using local.comm_sitj apply simp
  using local.all_sisj apply simp
  apply (simp add: local.ti_hom)
  apply (simp add: local.si_hom)
  unfolding imultimagma.iconv_def
  using local.iconv_def local.omega_interchange local.stimm.conv_def local.stimm.stopp.conv_def by simp

context omega_st_multimagma
begin

lemma sisj: "i ≤ j ⟹ src i (src j x) = src i x"
  using antisym_conv2 local.all_sisj local.sjsi by fastforce

lemma sisj_var [simp]: "src i (src (i + k) x) = src i x"
  by (simp add: sisj)

lemma sitj: "i < j ⟹ src i (tgt j x) = src i x"
  by (simp add: local.comm_sitj)

lemma sitj_var [simp]: "src i (tgt (i + k + 1) x) = src i x"
  using local.otmm.twolropp.t0s1 by auto

lemma tisj: "i < j ⟹ tgt i (src j x) = tgt i x"
  by (simp add: local.olropp.comm_sitj)

lemma tisj_var [simp]: "tgt i (src (i + k + 1) x) = tgt i x"
  using local.otmm.twolropp.s0t1 by auto

lemma titi: "i ≤ j ⟹ tgt i (tgt j x) = tgt i x"
  using antisym_conv2 local.olropp.all_sisj local.tjti by fastforce

lemma titi_var [simp]: "tgt i (tgt (i + k) x) = tgt i x"
  by (simp add: titi)

end

context omega_catoid
begin

lemma src_icat1:
  assumes "i ≤ j"
  and "DD j x y"
  shows "Srci i (x ⊙⇘j⇙ y) = {src i x}"
  by (smt (verit, ccfv_SIG) assms icat.src_comp_cond image_is_empty local.comm_sitj local.si_hom local.sisj local.stimm.stopp.Dst local.tgt_absorb subset_singletonD)

lemma src_icat2:
  assumes "i < j"
  and "DD j x y"
shows "Srci i (x ⊙⇘j⇙ y) = {src i y}"
  by (metis assms less_or_eq_imp_le local.all_sisj local.sitj local.sjsi local.stimm.stopp.Dst src_icat1)

lemma tgt_icat1:
  assumes "i < j"
  and "DD j x y"
  shows "Tgti i (x ⊙⇘j⇙ y) = {tgt i x}"
  by (smt (verit) assms image_is_empty local.olropp.all_sisj local.stimm.stopp.Dst local.ti_hom local.tisj local.tjti not_less_iff_gr_or_eq stimm.t_idem subset_singletonD)

lemma tgt_icat2:
  assumes "i ≤ j"
  and "DD j x y"
  shows "Tgti i (x ⊙⇘j⇙ y) = {tgt i y}"
  by (smt (verit, best) assms(1) assms(2) icat.tgt_comp_cond local.all_titj local.stimm.stopp.Dst local.tisj local.tjti nat_less_le tgt_icat1)

end
text ‹We lift the axioms to the powerset level.›

context omega_st_multimagma
begin

lemma comm_SiSj: "Srci i (Srci j X) = Srci j (Srci i X)"
  by (metis (mono_tags, lifting) image_cong image_image local.comm_sisj)

lemma comm_TiTj: "Tgti i (Tgti j X) = Tgti j (Tgti i X)"
  by (simp add: image_image local.olropp.all_sisj)

lemma comm_SiTj: "i ≠ j ⟹ Srci i (Tgti j x) = Tgti j (Srci i x)"
  by (metis (mono_tags, lifting) image_cong image_image local.comm_sitj)

lemma comm_TiSj: "i ≠ j ⟹ Tgti i (Srci j x) = Srci j (Tgti i x)"
  using local.comm_SiTj by simp

lemma interchange_lift: 
  assumes "i < j"
  shows "(W ⋆⇘j⇙ X) ⋆⇘i⇙ (Y ⋆⇘j⇙ Z) ⊆ (W ⋆⇘i⇙ Y) ⋆⇘j⇙ (X ⋆⇘i⇙ Z)"
proof-
  {fix a
  assume "a ∈ (W ⋆⇘j⇙ X) ⋆⇘i⇙ (Y ⋆⇘j⇙ Z)"
  hence "∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. a ∈ (w ⊙⇘j⇙ x) ⋆⇘i⇙ (y ⊙⇘j⇙ z)"
    unfolding iconv_def by force
  hence "∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. a ∈ (w ⊙⇘i⇙ y) ⋆⇘j⇙ (x ⊙⇘i⇙ z)"
    using assms local.omega_interchange by fastforce
  hence "a ∈ (W ⋆⇘i⇙ Y) ⋆⇘j⇙ (X ⋆⇘i⇙ Z)"
    unfolding iconv_def by force}
  thus ?thesis..
qed

lemma Srcj_hom: 
  assumes "i ≠ j"
  shows "Srci j (X ⋆⇘i⇙ Y) ⊆ Srci j X ⋆⇘i⇙ Srci j Y" 
  unfolding iconv_def by (clarsimp, metis assms image_subset_iff local.si_hom)

lemma Tgtj_hom:
  assumes "i ≠ j"
  shows "Tgti j (X ⋆⇘i⇙ Y) ⊆ Tgti j X ⋆⇘i⇙ Tgti j Y" 
  unfolding iconv_def by (clarsimp, metis assms image_subset_iff local.ti_hom)

lemma SjSi: "i ≤ j ⟹ Srci j (Srci i X) = Srci i X"
  by (smt (verit, best) antisym_conv2 imageE image_cong local.sjsi local.stimm.stopp.ST_compat local.stimm.stopp.ts_compat stimm.ts_compat)

lemma SjSi_var [simp]: "Srci (i + k) (Srci i X) = Srci i X"
  by (simp add: image_image)

lemma SjTi: "i ≤ j ⟹ Srci j (Tgti i X) = Tgti i X"
  by (metis SjSi_var less_eqE local.stimm.stopp.TS_compat)

lemma SjTi_var [simp]: "Srci (i + k) (Tgti i X) = Tgti i X"
  by (simp add: SjTi)

lemma TjSi: "i ≤ j ⟹ Tgti j (Srci i X) = Srci i X"
  by (metis local.SjSi local.stimm.stopp.ST_compat)

lemma TjSi_var [simp]: "Tgti (i + k) (Srci i X) = Srci i X"
  using TjSi le_add1 by presburger

lemma TjTi: "i ≤ j ⟹ Tgti j (Tgti i X) = Tgti i X"
  by (metis local.SjTi local.stimm.stopp.ST_compat)

lemma TjTi_var [simp]: "Tgti (i + k) (Tgti i X) = Tgti i X"
  by (simp add: TjTi)

lemma srcfixij: "i ≤ j ⟹ srcfix i ⊆ srcfix i ⋆⇘j⇙ srcfix i"
  by (smt (verit, ccfv_SIG) UN_iff antisym_conv2 local.iconv_def local.tgt_absorb local.tjti mem_Collect_eq singletonI stimm.ts_compat subsetI)

lemma srcfixij_var: "srcfix i ⊆ srcfix i ⋆⇘(j + k)⇙ srcfix i"
  by (smt (verit, ccfv_SIG) UN_iff local.comm_sitj local.iconv_def local.stimm.stopp.ts_compat local.tgt_absorb mem_Collect_eq singletonI subsetI)

lemma srcfixij_var2: "i ≤ j ⟹ srcfix i ⊆ srcfix j"
  by (metis local.SjSi local.stimm.stopp.Tgt_subid local.stimm.stopp.tfix_im)

lemma srcfixij_var3: "srcfix i ⊆ srcfix (i + k)"
  using le_add1 srcfixij_var2 by blast

end

context omega_st_multimagma_strong
begin

lemma Srcj_hom_strong: 
  assumes "i < j"
  shows "Srci j (X ⋆⇘i⇙ Y) = Srci j X ⋆⇘i⇙ Srci j Y"
proof-
  {fix a 
  have "(a ∈ Srci j (X ⋆⇘i⇙ Y)) = (∃b ∈ X ⋆⇘i⇙ Y. a = src j b)"
    by force
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Y. a = src j b ∧ b ∈ c ⊙⇘i⇙ d)"
    using local.iconv_def by auto
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ Srci j (c ⊙⇘i⇙ d))"
    by force
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ src j c ⊙⇘i⇙ src j d)"
    using assms local.sj_hom_strong by auto
  also have "… = (∃c ∈ Srci j X. ∃d ∈ Srci j Y. a ∈ c ⊙⇘i⇙ d)"
    by force
  also have "… = (a ∈ Srci j X ⋆⇘i⇙ Srci j Y)"
    by (simp add: local.iconv_def)
  finally have "(a ∈ Srci j (X ⋆⇘i⇙ Y)) = (a ∈ Srci j X ⋆⇘i⇙ Srci j Y)".}
  thus ?thesis
    by force
qed

lemma Srcj_hom_strong_var: "Srci (i + k + 1) (X ⋆⇘i⇙ Y) = Srci (i + k + 1) X ⋆⇘i⇙ Srci (i + k + 1) Y"
  by (simp add: Srcj_hom_strong)

lemma Tgtj_hom_strong: 
  assumes "i < j"
  shows "Tgti j (X ⋆⇘i⇙ Y) = Tgti j X ⋆⇘i⇙ Tgti j Y" 
proof-
  {fix a 
    have "(a ∈ Tgti j (X ⋆⇘i⇙ Y)) = (∃c ∈ X. ∃d ∈ Y. a ∈ Tgti j (c ⊙⇘i⇙ d))"
      using local.iconv_def by force
    also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ tgt j c ⊙⇘i⇙ tgt j d)"
      using assms local.tj_hom_strong by force
    also have "… = (a ∈ Tgti j X ⋆⇘i⇙ Tgti j Y)"
      by (simp add: local.iconv_def)
  finally have "(a ∈ Tgti j (X ⋆⇘i⇙ Y)) = (a ∈ Tgti j X ⋆⇘i⇙ Tgti j Y)".}
  thus ?thesis
    by force
qed

lemma Tgtj_hom_strong_var: "Tgti (i + k + 1) (X ⋆⇘i⇙ Y) = Tgti (i + k + 1) X ⋆⇘i⇙ Tgti (i + k + 1) Y"
  using Tgtj_hom_strong by auto 

lemma srcfixij_var2: "i < j ⟹ srcfix j ⋆⇘i⇙ srcfix j ⊆ srcfix j"
  by (metis local.Srcj_hom_strong local.stimm.stopp.Tgt_subid local.stimm.stopp.tfix_im)

lemma srcfixij_var22: "srcfix (i + k + 1) ⋆⇘i⇙ srcfix (i + k + 1) ⊆ srcfix (i + k + 1)"
  using Suc_eq_plus1 less_add_Suc1 local.srcfixij_var2 by presburger
 
lemma srcfixij_eq: "i < j ⟹ srcfix j ⋆⇘i⇙ srcfix j = srcfix j"
  unfolding iconv_def
  apply safe
   apply (metis imageE local.sj_hom_strong local.stimm.stopp.tt_idem)
  by (smt (verit, ccfv_threshold) UN_iff local.sjsi local.stimm.stopp.ts_compat local.tgt_absorb mem_Collect_eq singletonI)

lemma srcfixij_eq_var [simp]: "srcfix (i + k + 1) ⋆⇘i⇙ srcfix (i + k + 1) = srcfix (i + k + 1)"
  using Suc_eq_plus1 less_add_Suc1 srcfixij_eq by presburger

end

subsection‹$\omega$-Catoids and single-set $\omega$-categories›

class omega_catoid_strong = omega_st_multimagma_strong + omega_catoid

class local_omega_catoid = omega_st_multimagma + local_icatoid

class functional_omega_catoid = omega_st_multimagma  + functional_icatoid

class local_omega_catoid_strong = omega_st_multimagma_strong + local_icatoid

class omega_category = omega_st_multimagma + icategory

begin

lemma sj_hom_strong: 
  assumes "i < j"
  shows "Srci j (x ⊙⇘i⇙ y) = src j x ⊙⇘i⇙ src j y"
  by (smt (verit, best) assms image_is_empty less_or_eq_imp_le licat.src_local_eq local.pmi.functionality_lem_var local.si_hom local.sisj local.stimm.stopp.Dst local.tgt_absorb local.tisj nat_neq_iff subset_singletonD)

lemma sj_hom_strong_var: "Srci (i + k + 1) (x ⊙⇘i⇙ y) = src (i + k + 1) x ⊙⇘i⇙ src (i + k + 1) y"
  using local.sj_hom_strong by force

lemma sj_hom_strong_delta: "i < j ⟹ DD i x y = DD i (src j x) (src j y)"
  using local.sisj local.tisj stimm.locality by simp

lemma tj_hom_strong: "i < j ⟹ Tgti j (x ⊙⇘i⇙ y) = tgt j x ⊙⇘i⇙ tgt j y"
  by (smt (verit, best) empty_is_image licat.st_local local.olropp.si_hom local.pmi.functionality_lem_var local.sitj local.titi order.strict_iff_order subset_singleton_iff)

lemma tj_hom_strong_var: "Tgti (i + k + 1) (x ⊙⇘i⇙ y) = tgt (i + k + 1) x ⊙⇘i⇙ tgt (i + k + 1) y"
  by (simp add: local.tj_hom_strong)

lemma tj_hom_strong_delta: " i < j ⟹ DD i x y = DD i (tgt j x) (tgt j y)"
  using less_or_eq_imp_le licat.st_local local.sitj local.titi by simp

lemma convi_sgl: "a ∈ x ⊙⇘i⇙ y ⟹ {a} = x ⊙⇘i⇙ y"
  by (simp add: local.pmi.fun_in_sgl)

text ‹Next we derive some simple globular properties.›

lemma strong_interchange_STj: 
  assumes "i < j"
  and "a ∈ (w ⊙⇘i⇙ x) ⋆⇘j⇙ (y ⊙⇘i⇙ z)"
  shows "Tgti j (w ⊙⇘i⇙ x) = Srci j (y ⊙⇘i⇙ z)"
  by (smt (verit) assms(2) image_empty image_insert local.iconv_prop local.pmi.fun_in_sgl local.pmi.pcomp_def_var local.stimm.stopp.Dst multimagma.conv_exp2)

lemma strong_interchange_ssi: 
  assumes "i < j"
  and "a ∈ (w ⊙⇘i⇙ x) ⋆⇘j⇙ (y ⊙⇘i⇙ z)"
shows "src i w = src i y"
  by (smt (verit, ccfv_threshold) assms icat.src_comp_aux icat.tgt_comp_aux less_or_eq_imp_le local.iconv_prop local.sisj local.sitj multimagma.conv_exp2)

end


subsection ‹Reduced axiomatisations›

class omega_st_multimagma_red = st_imultimagma +
  assumes interchange: "i < j ⟹ (w ⊙⇘j⇙ x) ⋆⇘i⇙ (y ⊙⇘j⇙ z) ⊆ (w ⊙⇘i⇙ y) ⋆⇘j⇙ (x ⊙⇘i⇙ z)" (* irredundant *)
  assumes srcj_hom: "i < j ⟹ Srci j (x ⊙⇘i⇙ y) = src j x ⊙⇘i⇙ srcj y"  (* irredundant *)
  and tgtj_hom: "i < j ⟹ Tgti j (x ⊙⇘i⇙ y) = tgt j x ⊙⇘i⇙ tgt j y" (* irredundant *)
  and srci_weak_hom: "i < j ⟹ Srci i (x ⊙⇘j⇙ y) ⊆ src i x ⊙⇘j⇙ src i y" (* no proof no counterexample *)
  and tgti_weak_hom: "i < j ⟹ Tgti i (x ⊙⇘j⇙ y) ⊆ src i x ⊙⇘j⇙ src i y" (* no proof no counterexample *) 

begin

lemma sitjsi [simp]: "src i (tgt j (src i x)) = src i x"
  by (smt (z3) empty_iff image_empty image_insert insert_subset less_add_Suc1 local.srcj_hom local.stimm.stopp.t_idem stimm.s_absorb_var2 subset_empty)

lemma tisjsi [simp]: "tgt i (src j (src i x)) = src i x"
  by (smt (verit) local.srcj_hom local.stimm.stopp.s_absorb_var3 local.stimm.stopp.ts_compat not_less_iff_gr_or_eq sitjsi)

lemma sjsi: 
  assumes "i ≤ j"
  shows "src j (src i x) = src i x"
  by (smt (verit) antisym_conv2 assms insertE insert_absorb insert_subset local.Dst local.iconv_def local.interchange local.src_absorb local.stimm.conv_def local.stimm.stopp.conv_atom local.tgt_absorb local.tgtj_hom stimm.s_absorb_var2 stimm.t_export tisjsi)

lemma sjti: "i ≤ j ⟹ src j (tgt i x) = tgt i x"
  by (metis local.sjsi local.stimm.stopp.ts_compat)

lemma tjsi: "i ≤ j ⟹ tgt j (src i x) = src i x"
  by (metis antisym_conv2 local.sjsi stimm.ts_compat)

lemma tjti: "i ≤ j ⟹ tgt j  (tgt i x) = tgt i x"
  by (simp add: local.sjti stimm.st_fix)

lemma comm_sisj: "i ≠ j ⟹ src i (src j x) = src j (src i x)"
  by (smt (verit, ccfv_threshold) less_or_eq_imp_le local.sjsi local.srcj_hom not_less_iff_gr_or_eq stimm.s_ortho_iff tisjsi)

lemma comm_sitj: "i ≠ j ⟹ src i (tgt j x) = tgt j (src i x)"
  by (smt (verit, best) local.srcj_hom local.stimm.stopp.ts_compat local.tjsi nat_less_le nle_le stimm.s_absorb_var)

lemma comm_titj: "i ≠ j ⟹ tgt i (tgt j x) = tgt j (tgt i x)"
  by (smt (verit, ccfv_SIG) local.comm_sisj local.comm_sitj local.stimm.stopp.ts_compat tisjsi)

end

class omega_catoid_red = icatoid +
  assumes interchange: "i < j ⟹ (w ⊙⇘j⇙ x) ⋆⇘i⇙ (y ⊙⇘j⇙ z) ⊆ (w ⊙⇘i⇙ y) ⋆⇘j⇙ (x ⊙⇘i⇙ z)" (* irredundant *)
  and sj_hom: "i < j ⟹ Srci j (x ⊙⇘i⇙ y) ⊆ src j x ⊙⇘i⇙ src j y"  (* irredundant *)
  and tj_hom: "i < j ⟹ Tgti j (x ⊙⇘i⇙ y) ⊆ tgt j x ⊙⇘i⇙ tgt j y" (* irredundant *)

begin

lemma sitjsi: 
  assumes "i < j"
  shows "src i (tgt j (src i x)) = src i x"
  by (metis (no_types, lifting) SUP_empty assms local.iconv_prop local.interchange local.src_absorb local.stimm.stopp.conv_atom local.stimm.stopp.conv_def local.tgt_absorb order_less_imp_le stimm.s_absorb_var3 subset_empty)

lemma tisjsi: "i < j ⟹ tgt i (src j (src i x)) = src i x"
  by (smt (verit, ccfv_SIG) image_is_empty local.sitjsi local.sj_hom local.stimm.stopp.Dst local.stimm.stopp.st_ortho_iff stimm.s_absorb_var subset_empty)

lemma sjsi: 
  assumes "i < j"
  shows "src j (src i x) = src i x"
  by (smt (verit, ccfv_SIG) assms empty_iff insert_iff insert_subset less_or_eq_imp_le local.iconv_prop local.interchange local.sitjsi local.src_absorb local.stimm.stopp.conv_atom local.stimm.stopp.s_absorb_var2 local.tgt_absorb local.tisjsi stimm.s_ortho_iff)
 
lemma sjti: "i < j ⟹ src j (tgt i x) = tgt i x"
  by (metis local.sjsi local.stimm.stopp.ts_compat)

lemma tjsi: "i < j ⟹ tgt j (src i x) = src i x"
  by (simp add: local.sjsi stimm.st_fix)

lemma tjti: "i < j ⟹ tgt j  (tgt i x) = tgt i x"
  by (simp add: local.sjti stimm.st_fix)

lemma comm_sisj: "i < j ⟹ src i (src j x) = src j (src i x)"
  by (metis (no_types, opaque_lifting) empty_iff image_insert insert_subset local.sj_hom local.sjsi local.src_absorb local.stimm.stopp.Dst stimm.ts_compat)

lemma comm_sitj: "i < j ⟹ src i (tgt j x) = tgt j (src i x)"
  by (metis empty_iff image_insert insert_subset local.src_absorb local.tj_hom local.tjsi stimm.s_absorb_var2)

lemma comm_tisj: "i < j ⟹ tgt i (src j x) = src j (tgt i x)"
  by (metis empty_iff image_insert insert_subset local.sj_hom local.sjti local.stimm.stopp.s_absorb_var3 local.tgt_absorb)

lemma comm_titj: "i < j ⟹ tgt i (tgt j x) = tgt j (tgt i x)"
  by (smt (verit) bot.extremum_uniqueI local.sjti local.stimm.stopp.s_absorb_var local.stimm.stopp.s_export local.tgt_absorb local.tj_hom stimm.st_fix)

lemma si_hom: "i < j ⟹ Srci i  (x ⊙⇘j⇙ y) ⊆ src i x ⊙⇘j⇙ src i y"
  by (smt (verit, del_insts) icat.tgt_comp_aux image_subset_iff local.comm_sisj local.comm_sitj local.icat.ts_msg.src_twisted_aux local.src_absorb local.stimm.stopp.Dst local.tjsi singletonI)

lemma ti_hom: "i < j ⟹ Tgti i (x ⊙⇘j⇙ y) ⊆ tgt i x ⊙⇘j⇙ tgt i y"
  by (smt (verit, ccfv_SIG) comm_tisj icat.tgt_comp_aux image_subset_iff local.comm_titj local.stimm.stopp.Dst local.tgt_absorb local.tjti singletonI)

end 

class omega_catoid_red_strong = icatoid +
  assumes interchange: "i < j ⟹ (w ⊙⇘j⇙ x) ⋆⇘i⇙ (y ⊙⇘j⇙ z) ⊆ (w ⊙⇘i⇙ y) ⋆⇘j⇙ (x ⊙⇘i⇙ z)" (* irredundant *)
  and sj_hom_strong: "i ≤ j ⟹ Srci j (x ⊙⇘i⇙y) = src j x ⊙⇘i⇙ src j y"  (* irredundant *)
  and tj_hom_strong: "i ≤ j ⟹ Tgti j (x ⊙⇘i⇙ y) = tgt j x ⊙⇘i⇙ tgt j y" (* irredundant *)

begin

lemma sitjsi: "i < j ⟹ src i (tgt j (src i x)) = src i x"
  by (metis UN_empty Union_empty dual_order.strict_iff_not local.src_absorb local.stimm.stopp.s_ortho_id local.tj_hom_strong stimm.Tgt_Sup_pres stimm.s_absorb_var stimm.s_ortho_id stimm.t_export stimm.tt_idem)

lemma tisjsi: "i < j ⟹ tgt i (src j (src i x)) = src i x"
  by (metis image_empty less_or_eq_imp_le local.sj_hom_strong local.stimm.stopp.Dst local.stimm.stopp.s_absorb_var2 stimm.ts_compat)

lemma sjsi: 
  assumes "i < j"
  shows "src j (src i x) = src i x"
proof-
  have "{src i x} = src i x ⊙⇘i⇙ src i x"
    by simp
  also have "… = (src j (src i x) ⊙⇘j⇙ src i x) ⋆⇘i⇙ (src i x ⊙⇘j⇙ tgt j (src i x))"
    by (simp add: local.iconv_prop)
  also have "… ⊆ (src j (src i x) ⊙⇘i⇙ src i x) ⋆⇘j⇙ (src i x ⊙⇘i⇙ tgt j (src i x))"
    by (meson assms local.interchange)
  also have "… = (src j (src i x) ⊙⇘i⇙ tgt i (src j (src i x))) ⋆⇘j⇙ (src i (tgt j (src i x)) ⊙⇘i⇙ tgt j (src i x))"
    by (simp add: assms local.sitjsi local.tisjsi)
  also have "… = src j (src i x) ⊙⇘j⇙ tgt j (src i x)"
    using local.iconv_prop by simp
  finally have "{src i x} ⊆ src j (src i x) ⊙⇘j⇙ tgt j (src i x)".
  thus ?thesis
    using local.stimm.stopp.Dst by force
qed
 
lemma sjti: "i < j ⟹ src j (tgt i x) = tgt i x"
  by (metis local.sjsi local.stimm.stopp.ts_compat)

lemma tjsi: "i < j ⟹ tgt j (src i x) = src i x"
  using local.sjsi stimm.st_fix by blast

lemma tjti: "i < j ⟹ tgt j (tgt i x) = tgt i x"
  by (simp add: local.sjti stimm.st_fix)

lemma comm_sisj: "i < j ⟹ src i (src j x) = src j (src i x)"
  by (smt (verit) less_or_eq_imp_le local.sj_hom_strong local.sjsi local.src_absorb stimm.s_absorb_var3)

lemma comm_sitj: "i < j ⟹ src i (tgt j x) = tgt j (src i x)"
  by (metis local.tj_hom_strong local.tjsi order.strict_iff_not stimm.s_absorb_var2)

lemma comm_tisj: "i < j ⟹ tgt i (src j x) = src j (tgt i x)"
  by (metis dual_order.strict_implies_order local.sj_hom_strong local.sjti local.stimm.stopp.s_absorb_var)

lemma comm_titj: "i < j ⟹ tgt i (tgt j x) = tgt j (tgt i x)"
  by (metis image_empty less_or_eq_imp_le local.comm_sitj local.sj_hom_strong local.stimm.stopp.Dst stimm.s_ortho_iff)

lemma s0_weak_hom: "i < j ⟹ Srci i (x ⊙⇘j⇙ y) ⊆ src i x ⊙⇘j⇙ src i y"
  by (smt (verit, best) image_subsetI insertI1 local.comm_sisj local.comm_sitj local.icat.ts_msg.tgt_comp_aux local.sjsi local.src_absorb local.stimm.stopp.Dst local.tjsi)

lemma t0_weak_hom: "i < j ⟹ Tgti i (x ⊙⇘j⇙ y) ⊆ tgt i x ⊙⇘j⇙ tgt i y"
  by (smt (verit, ccfv_SIG) icat.tgt_comp_aux image_subset_iff local.comm_tisj local.comm_titj local.sjsi local.stimm.stopp.Dst local.stimm.stopp.ts_compat local.tgt_absorb singletonI stimm.ts_compat)

end

end