Theory Two_Catoid

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

section ‹2-Catoids›

theory Two_Catoid
  imports Catoids.Catoid

begin

text‹We define 2-catoids and in particular (strict) 2-categories as local functional 2-catoids. With Isabelle
we first need to make two copies of catoids for the 0-structure and 1-structure.›

subsection ‹0-Structures and 1-structures.›

class multimagma0 = 
  fixes mcomp0 :: "'a ⇒ 'a ⇒ 'a set" (infixl ‹⊙0› 70) 

begin 

sublocale mm0: multimagma mcomp0.

abbreviation "Δ0 ≡ mm0.Δ"

abbreviation conv0 :: "'a set ⇒ 'a set ⇒ 'a set" (infixl ‹*0› 70) where
 "X *0 Y ≡ mm0.conv X Y"

lemma "X *0 Y = (⋃x ∈ X. ⋃y ∈ Y. x ⊙0 y)"
  by (simp add: mm0.conv_def)

end

class multimagma1 = 
  fixes mcomp1 :: "'a ⇒ 'a ⇒ 'a set" (infixl ‹⊙1› 70) 

begin 

sublocale mm1: multimagma mcomp1.

abbreviation "Δ1 ≡ mm1.Δ"

abbreviation conv1 :: "'a set ⇒ 'a set ⇒ 'a set" (infixl ‹*1› 70) where
  "X *1 Y ≡ mm1.conv X Y"

end

class multisemigroup0 = multimagma0 +
  assumes assoc: "(⋃v ∈ y ⊙0 z. x ⊙0 v) = (⋃v ∈ x ⊙0 y. v ⊙0 z)"

sublocale multisemigroup0 ⊆ msg0: multisemigroup mcomp0
  by (unfold_locales, simp add: local.assoc)

class multisemigroup1 = multimagma1 +
  assumes assoc: "(⋃v ∈ y ⊙1 z. x ⊙1 v) = (⋃v ∈ x ⊙1 y. v ⊙1 z)"

sublocale  multisemigroup1 ⊆ msg1: multisemigroup mcomp1
  by (unfold_locales, simp add: local.assoc)

class st_multimagma0 = multimagma0 + 
fixes σ0 :: "'a ⇒ 'a"
  and τ0 :: "'a ⇒ 'a" 
  assumes Dst0: "x ⊙0 y ≠ {} ⟹ τ0 x = σ0 y"
  and src0_absorb [simp]: "σ0 x ⊙0 x = {x}" 
  and tgt0_absorb [simp]: "x ⊙0 τ0 x = {x}"

begin

sublocale stmm0: st_multimagma mcomp0 σ0 τ0
  by (unfold_locales, simp_all add: local.Dst0)

abbreviation "s0fix ≡ stmm0.sfix"

abbreviation "t0fix ≡ stmm0.tfix"

abbreviation "Src0 ≡ stmm0.Src"

abbreviation "Tgt0 ≡ stmm0.Tgt"

end

class st_multimagma1 = multimagma1 + 
fixes σ1 :: "'a ⇒ 'a" 
  and τ1 :: "'a ⇒ 'a"
  assumes Dst1: "x ⊙1 y ≠ {} ⟹ τ1 x = σ1 y"
  and src1_absorb [simp]: "σ1 x ⊙1 x = {x}" 
  and tgt1_absorb [simp]: "x ⊙1 τ1 x = {x}"

begin

sublocale stmm1: st_multimagma mcomp1 σ1 τ1
  by (unfold_locales, simp_all add: local.Dst1)

abbreviation "s1fix ≡ stmm1.sfix"

abbreviation "t1fix ≡ stmm1.tfix"

abbreviation "Src1 ≡ stmm1.Src"

abbreviation "Tgt1 ≡ stmm1.Tgt"

end

class catoid0 = st_multimagma0 + multisemigroup0

sublocale catoid0 ⊆ stmsg0: catoid mcomp0 σ0 τ0..

class catoid1 = st_multimagma1 + multisemigroup1

sublocale catoid1 ⊆ stmsg1: catoid mcomp1 σ1 τ1..

class local_catoid0 = catoid0 +
  assumes src0_local: "Src0 (x ⊙0 σ0 y) ⊆ Src0 (x ⊙0 y)"
  and tgt0_local: "Tgt0 (τ0 x ⊙0 y) ⊆ Tgt0 (x ⊙0 y)"

class local_catoid1 = catoid1 +
  assumes l1_local: "Src1 (x ⊙1 σ1 y) ⊆ Src1 (x ⊙1 y)"
  and r1_local: "Tgt1 (τ1 x ⊙1 y) ⊆ Tgt1 (x ⊙1 y)"

sublocale local_catoid0 ⊆ ssmsg0: local_catoid mcomp0 σ0 τ0
  apply unfold_locales using local.src0_local local.tgt0_local by auto

sublocale local_catoid1 ⊆ stmsg1: local_catoid mcomp1 σ1 τ1
  apply unfold_locales using local.l1_local local.r1_local by auto

class functional_magma0 = multimagma0 + 
  assumes functionality0: "x ∈ y ⊙0 z ⟹ x' ∈ y ⊙0 z ⟹ x = x'"

sublocale functional_magma0 ⊆ pm0: functional_magma mcomp0
  by (unfold_locales, simp add: local.functionality0)

class functional_magma1 = multimagma1 + 
  assumes functionality1: "x ∈ y ⊙1 z ⟹ x' ∈ y ⊙1 z ⟹ x = x'"

sublocale functional_magma1 ⊆ pm1: functional_magma mcomp1
  by (unfold_locales, simp add: local.functionality1)

class functional_semigroup0 = functional_magma0 + multisemigroup0

sublocale functional_semigroup0 ⊆ psg0: functional_semigroup mcomp0..

class functional_semigroup1 = functional_magma1 + multisemigroup1

sublocale functional_semigroup1 ⊆ psg1: functional_semigroup mcomp1..

class functional_catoid0 = functional_semigroup0 + catoid0

sublocale functional_catoid0 ⊆ psg0: functional_catoid mcomp0  σ0 τ0..

class functional_catoid1 = functional_semigroup1 + catoid1

sublocale functional_catoid1 ⊆ psg1: functional_catoid mcomp1 σ1 τ1..

class single_set_category0 = functional_catoid0 + local_catoid0

sublocale single_set_category0 ⊆ sscat0: single_set_category mcomp0 σ0 τ0..

class single_set_category1 = functional_catoid1 + local_catoid1

sublocale single_set_category1 ⊆ sscat1: single_set_category mcomp1  σ1 τ1..


subsection ‹2-Catoids›

text ‹We define 2-catoids and 2-categories.›

class two_st_multimagma = st_multimagma0 + st_multimagma1 +
  assumes comm_s0s1: "σ0 (σ1 x) = σ1 (σ0 x)"
  and comm_s0t1: "σ0 (τ1 x) = τ1 (σ0 x)"
  and comm_t0s1: "τ0 (σ1 x) = σ1 (τ0 x)"
  and comm_t0t1: "τ0 (τ1 x) = τ1 (τ0 x)"
  assumes interchange: "(w ⊙1 x) *0 (y ⊙1 z) ⊆ (w ⊙0 y) *1 (x ⊙0 z)"
  and s1_hom: "Src1 (x ⊙0 y) ⊆ σ1 x ⊙0 σ1 y"
  and t1_hom: "Tgt1 (x ⊙0 y) ⊆ τ1 x ⊙0 τ1 y"
  and s0_hom: "Src0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y"
  and t0_hom: "Tgt0 (x ⊙1 y) ⊆ τ0 x ⊙1 τ0 y"
  and s1s0 [simp]: "σ1 (σ0 x) = σ0 x"
  and s1t0 [simp]: "σ1 (τ0 x) = τ0 x"
  and t1s0 [simp]: "τ1 (σ0 x) = σ0 x"
  and t1t0 [simp]: "τ1 (τ0 x) = τ0 x"

class two_st_multimagma_strong = two_st_multimagma +
  assumes s1_hom_strong: "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y"
  and t1_hom_strong: "Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y"

context two_st_multimagma
begin

sublocale twolropp: two_st_multimagma "λx y. y ⊙0 x" "τ0" "σ0" "λx y. y ⊙1 x" "τ1" "σ1"
  apply unfold_locales
                    apply (simp_all add: stmm0.stopp.Dst stmm1.stopp.Dst comm_t0t1 comm_t0s1 comm_s0t1 comm_s0s1 s1_hom t1_hom s0_hom t0_hom)
  by (metis local.interchange local.stmm0.stopp.conv_exp local.stmm1.stopp.conv_exp multimagma.conv_exp)

lemma s0s1 [simp]: "σ0 (σ1 x) = σ0 x"
 by (simp add: local.comm_s0s1)

lemma s0t1 [simp]: "σ0 (τ1 x) = σ0 x"
  by (simp add: local.comm_s0t1)

lemma t0s1 [simp]: "τ0 (σ1 x) = τ0 x"
  by (simp add: local.comm_t0s1)

lemma t1t1 [simp]: "τ0 (τ1 x) = τ0 x"
  by (simp add: local.comm_t0t1)

lemma src0_comp1: "Δ1 x y ⟹ Src0 (x ⊙1 y) = {σ0 x}"
  by (metis empty_is_image local.Dst1 local.comm_s0t1 local.s1s0 local.src1_absorb local.t1s0 s0s1 subset_singleton_iff twolropp.t0_hom)

lemma src0_comp1_var: "Δ1 x y ⟹ Src0 (x ⊙1 y) = {σ0 y}"
  by (metis local.Dst1 s0s1 s0t1 src0_comp1)

lemma tgt0_comp1: "Δ1 x y ⟹ Tgt0 (x ⊙1 y) = {τ0 x}"
  by (metis empty_is_image local.Dst1 local.comm_t0t1 local.s1t0 local.src1_absorb local.t1t0 subset_singleton_iff t0s1 twolropp.s0_hom)

lemma tgt0_comp1_var:"Δ1 x y ⟹ Tgt0 (x ⊙1 y) = {τ0 y}"
  by (metis local.Dst1 t0s1 t1t1 tgt0_comp1)

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

lemma comm_S0S1: "Src0 (Src1 X) = Src1 (Src0 X)"
  by (simp add: image_image)

lemma comm_T0T1: "Tgt0 (Tgt1 X) = Tgt1 (Tgt0 X)"
  by (metis (mono_tags, lifting) image_cong image_image local.comm_t0t1)

lemma comm_S0T1: "Src0 (Tgt1 x) = Tgt1 (Src0 x)"
  by (simp add: image_image)

lemma comm_T0S1: "Tgt0 (Src1 x) = Src1 (Tgt0 x)"
  by (metis (mono_tags, lifting) image_cong image_image local.comm_t0s1)

lemma interchange_lifting: "(W *1 X) *0 (Y *1 Z) ⊆ (W *0 Y) *1 (X *0 Z)"
proof-
  {fix a
  assume "a ∈ (W *1 X) *0 (Y *1 Z)"
  hence "∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. a ∈ (w ⊙1 x) *0 (y ⊙1 z)"
    using local.mm0.conv_exp2 local.mm1.conv_exp2 by fastforce
  hence "∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. a ∈ (w ⊙0 y) *1 (x ⊙0 z)"
    using local.interchange by blast
  hence "a ∈ (W *0 Y) *1 (X *0 Z)"
    using local.mm0.conv_exp2 local.mm1.conv_exp2 by auto}
  thus ?thesis..
qed

lemma Src1_hom: "Src1 (X *0 Y) ⊆ Src1 X *0 Src1 Y" 
proof-
  {fix a 
  have "(a ∈ Src1 (X *0 Y)) = (∃b ∈ X *0 Y. a = σ1 b)"
    by blast
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Y. a = σ1 b ∧ b ∈ c ⊙0 d)"
    by (metis multimagma.conv_exp2)
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ Src1 (c ⊙0 d))"
    by blast
  also have "… ⟶ (∃c ∈ X. ∃d ∈ Y. a ∈ σ1 c ⊙0 σ1 d)"
    using local.s1_hom by fastforce
  also have "… = (∃c ∈ Src1 X. ∃d ∈ Src1 Y. a ∈ c ⊙0 d)"
    by blast
  also have "… = (a ∈ Src1 X *0 Src1 Y)"
    using local.mm0.conv_exp2 by auto  
  finally have "(a ∈ Src1 (X *0 Y)) ⟶ (a ∈ Src1 X *0 Src1 Y)".}
  thus ?thesis
    by force
qed

lemma Tgt1_hom: "Tgt1 (X *0 Y) ⊆ Tgt1 X *0 Tgt1 Y" 
proof-
  {fix a 
  have "(a ∈ Tgt1 (X *0 Y)) = (∃c ∈ X. ∃d ∈ Y. a ∈ Tgt1 (c ⊙0 d))"
    by (smt (verit, best) image_iff multimagma.conv_exp2)
  also have "… ⟶ (∃c ∈ X. ∃d ∈ Y. a ∈ τ1 c ⊙0 τ1 d)"
    using local.t1_hom by fastforce
  also have "… = (a ∈ Tgt1 X *0 Tgt1 Y)"
    using local.mm0.conv_exp2 by auto  
  finally have "(a ∈ Tgt1 (X *0 Y)) ⟶ (a ∈ Tgt1 X *0 Tgt1 Y)".}
  thus ?thesis
    by force
qed

lemma Src0_hom: "Src0 (X *1 Y) ⊆ Src0 X *1 Src0 Y" 
proof-
  {fix a
  assume "a ∈ Src0 (X *1 Y)"
  hence "∃c ∈ X. ∃d ∈ Y. a ∈ Src0 (c ⊙1 d)"
    using local.mm1.conv_exp2 by fastforce
  hence "∃c ∈ X. ∃d ∈ Y. a ∈ σ0 c ⊙1 σ0 d"
    using local.s0_hom by blast
  hence "a ∈ Src0 X *1 Src0 Y"
    using local.mm1.conv_exp2 by auto}
  thus ?thesis
    by force
qed

lemma Tgt0_hom: "Tgt0 (X *1 Y) ⊆ Tgt0 X *1 Tgt0 Y" 
proof-
  {fix a
  assume "a ∈ Tgt0 (X *1 Y)"
  hence "∃c ∈ X. ∃d ∈ Y. a ∈ Tgt0 (c ⊙1 d)"
    using local.mm1.conv_exp2 by fastforce
  hence "∃c ∈ X. ∃d ∈ Y. a ∈ τ0 c ⊙1 τ0 d"
    using local.t0_hom by blast
  hence "a ∈ Tgt0 X *1 Tgt0 Y"
    using local.mm1.conv_exp2 by auto}
  thus ?thesis
    by force
qed

lemma S1S0 [simp]: "Src1 (Src0 X) = Src0 X"
  by force

lemma S1T0 [simp]: "Src1 (Tgt0 X) = Tgt0 X"
  by force

lemma T1S0 [simp]: "Tgt1 (Src0 X) = Src0 X"
  by force

lemma T1T0 [simp]: "Tgt1 (Tgt0 X) = Tgt0 X"
  by force

lemma (in two_st_multimagma) 
  "s1fix *0 s1fix ⊆ s1fix"
  (*nitpick [expect = genuine]*)
  oops

lemma id1_comp0_eq: "s1fix ⊆ s1fix *0 s1fix"
  by (metis S1S0 local.stmm0.stopp.conv_isor local.stmm0.stopp.conv_uns local.stmm0.stopp.stfix_set local.stmm0.stopp.tfix_im local.stmm1.stopp.Tgt_subid)

lemma (in two_st_multimagma) id01: 
  "s0fix ⊆ s1fix"
proof-
  {fix a
    have "(a ∈ s0fix) = (∃b. a = σ0 b)"
      by (metis imageE local.stmm0.stopp.tfix_im rangeI)
    hence "(a ∈ s0fix) = (∃b. a = σ1 (σ0 b))"
    by fastforce
  hence "(a ∈ s0fix) ⟹ (∃b. a = σ1 b)"
    by blast
  hence "(a ∈ s0fix) ⟹ (a ∈ s1fix)"
    using local.stmm1.stopp.tfix_im by blast}
  thus ?thesis
    by blast
qed

end

context two_st_multimagma_strong
begin

lemma Src1_hom_strong: "Src1 (X *0 Y) = Src1 X *0 Src1 Y" 
proof-
  {fix a 
  have "(a ∈ Src1 (X *0 Y)) = (∃b ∈ X *0 Y. a = σ1 b)"
    by blast
  also have "… = (∃b. ∃c ∈ X. ∃d ∈ Y. a = σ1 b ∧ b ∈ c ⊙0 d)"
    by (metis multimagma.conv_exp2)
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ Src1 (c ⊙0 d))"
    by blast
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ σ1 c ⊙0 σ1 d)"
    using local.s1_hom_strong by fastforce
  also have "… = (∃c ∈ Src1 X. ∃d ∈ Src1 Y. a ∈ c ⊙0 d)"
    by blast
  also have "… = (a ∈ Src1 X *0 Src1 Y)"
    using local.mm0.conv_exp2 by auto  
  finally have "(a ∈ Src1 (X *0 Y)) = (a ∈ Src1 X *0 Src1 Y)".}
  thus ?thesis
    by force
qed

lemma Tgt1_hom_strong: "Tgt1 (X *0 Y) = Tgt1 X *0 Tgt1 Y" 
proof-
  {fix a 
  have "(a ∈ Tgt1 (X *0 Y)) = (∃c ∈ X. ∃d ∈ Y. a ∈ Tgt1 (c ⊙0 d))"
    by (smt (verit, best) image_iff multimagma.conv_exp2)
  also have "… = (∃c ∈ X. ∃d ∈ Y. a ∈ τ1 c ⊙0 τ1 d)"
    using local.t1_hom_strong by fastforce
  also have "… = (a ∈ Tgt1 X *0 Tgt1 Y)"
    using local.mm0.conv_exp2 by auto  
  finally have "(a ∈ Tgt1 (X *0 Y)) = (a ∈ Tgt1 X *0 Tgt1 Y)".}
  thus ?thesis
    by force
qed

lemma id1_comp0: "s1fix *0 s1fix ⊆ s1fix"
proof-
  {fix a
  have "(a ∈ s1fix *0 s1fix) = (∃b ∈ s1fix.∃c ∈ s1fix. a ∈ b ⊙0 c)"
    by (meson local.mm0.conv_exp2)
  also have "… = (∃b c. a ∈ σ1 b ⊙0 σ1 c)"
    by (metis image_iff local.stmm1.stopp.tfix_im rangeI)
  finally have "(a ∈ s1fix *0 s1fix) = (∃b c. a ∈ Src1 (b ⊙0 c))"
    using local.s1_hom_strong by presburger
  hence "(a ∈ s1fix *0 s1fix) ⟹ (∃b. a = σ1 b)"
    by blast
  hence  "(a ∈ s1fix *0 s1fix) ⟹ (a ∈ s1fix)"
    using local.stmm1.stopp.Tgt_subid by blast}
  thus ?thesis
    by blast
qed


lemma id1_comp0_eq [simp]: "s1fix *0 s1fix = s1fix"
  using local.id1_comp0 local.id1_comp0_eq by force

end


subsection‹2-Catoids and single-set 2-categories›

class two_catoid = two_st_multimagma + catoid0 + catoid1

lemma (in two_catoid) "Δ0 x y ⟹ Src1 (x ⊙0 y) = {σ1 x}"
  (*nitpick[expect = genuine]*)
  oops

lemma (in two_catoid) "Δ0 x y ⟹ Tgt1 (x ⊙0 y) = {τ1 x}"
  (*nitpick[expect = genuine]*)
  oops

class two_catoid_strong = two_st_multimagma_strong + catoid0 + catoid1

class local_two_catoid = two_st_multimagma + local_catoid0 + local_catoid1

begin

text ‹local 2-catoids need not be strong›

lemma "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y"
  (*nitpick[expect = genuine]*)
  oops

lemma "Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y"
  (*nitpick[expect = genuine]*)
  oops

lemma "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y ∨ Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y"
  (*nitpick[expect = genuine]*)
  oops

end

class functional_two_catoid = two_st_multimagma  + functional_catoid0 + functional_catoid1

begin

lemma "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y"
  (*nitpick[expect = genuine]*)
  oops

lemma "Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y"
  (*nitpick[expect = genuine]*)
  oops

lemma "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y ∨ Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y"
  (*nitpick[expect = genuine]*)
  oops

end

class local_two_catoid_strong = two_st_multimagma_strong + local_catoid0 + local_catoid1

class two_category = two_st_multimagma + single_set_category0 + single_set_category1

begin

lemma s1_hom_strong [simp]: "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y"
proof cases
  assume "σ1 x ⊙0 σ1 y = {}"
  thus ?thesis
    using local.twolropp.t1_hom by blast
next
  assume h: "σ1 x ⊙0 σ1 y ≠ {}"
  hence "(τ0 (σ1 x) = σ0 (σ1 y))"
    using local.Dst0 by blast
  hence "τ0 x = σ0 y"
    by auto
  hence "x ⊙0 y ≠ {}"
    by (simp add: ssmsg0.st_local)
  thus ?thesis
    by (metis h image_is_empty local.pm0.fun_in_sgl local.pm0.functionality_lem local.twolropp.t1_hom subset_singletonD)
qed

lemma s1_hom_strong_delta: "Δ0 x y = Δ0 (σ1 x) (σ1 y)"
  by (simp add: ssmsg0.st_local)

lemma t1_hom_strong [simp]: "Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y"
  by (metis (no_types, lifting) empty_is_image local.pm0.functionality_lem_var local.s0t1 local.t1t1 local.twolropp.s1_hom ssmsg0.st_local subset_singleton_iff)

lemma t1_hom_strong_delta: "Δ0 x y = Δ0 (τ1 x) (τ1 y)"
  by (simp add: ssmsg0.st_local)

lemma conv0_sgl: "a ∈ x ⊙0 y ⟹ {a} = x ⊙0 y"
  using local.functionality0 by fastforce

lemma conv1_sgl: "a ∈ {x} *1 {y} ⟹ {a} = {x} *1 {y}"
  using local.functionality1 local.mm1.conv_exp by force

text ‹Next we derive some simple globular properties.›

lemma strong_interchange_St1: 
  assumes "a ∈ (w ⊙0 x) *1 (y ⊙0 z)"
  shows "Tgt1 (w ⊙0 x) = Src1 (y ⊙0 z)"
  by (smt (verit, ccfv_threshold) assms empty_iff image_insert image_is_empty insertE local.Dst1 local.mm1.conv_exp2 local.pm0.functionality_lem_var)

lemma strong_interchange_ll0: 
  assumes "a ∈ (w ⊙0 x) *1 (y ⊙0 z)"
  shows "σ0 w = σ0 y"
  by (metis assms empty_iff local.Dst1 local.s0s1 local.s0t1 local.stmm1.stopp.conv_exp2 stmsg0.src_comp_aux)

text ‹There is no strong interchange law, and the homomorphism laws for zero sources and targets stay weak, too.›

lemma "(w ⊙1 y) *0 (x ⊙1 z) = (w ⊙0 x) *1 (y ⊙0 z)"
  (*nitpick [expect = genuine]*)
  oops

lemma "R0 (x ⊙1 y) = r0 x ⊙1 r0 y"
    (*nitpick [expect = genuine]*)
  oops

lemma "L0 (x ⊙1 y) = l0 x ⊙1 l0 y"
    (*nitpick [expect = genuine]*)
  oops
 
lemma "(W *0 Y) *1 (X *0 Z) = (W *1 X) *0 (Y *1 Z)"
    (*nitpick [expect = genuine]*)
  oops

lemma "Δ0 x y ⟹ Src1 (x ⊙0 y) = {σ1 x}"
    (*nitpick [expect = genuine]*)
  oops

lemma "Δ0 x y ⟹ Tgt1 (x ⊙0 y) = {τ1 x}"
    (*nitpick [expect = genuine]*)
  oops

end


subsection ‹Reduced axiomatisations›

class two_st_multimagma_red = st_multimagma0 + st_multimagma1 +
  assumes interchange: "(w ⊙1 x) *0 (y ⊙1 z) ⊆ (w ⊙0 y) *1 (x ⊙0 z)" (* irredundant *)
  assumes src1_hom: "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y"  (* irredundant *)
  and tgt1_hom: "Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y" (* irredundant *)
  and src0_weak_hom: "Src0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y" (* no proof no counterexample *)
  and tgt0_weak_hom: "Tgt0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y" (* no proof no counterexample *) 

begin

lemma s0t1s0 [simp]: "σ0 (τ1 (σ0 x)) = σ0 x"
proof-
  have "{τ1 (σ0 x)} = Tgt1 (σ0 x ⊙0 σ0 x)"
    by simp
  also have "… = τ1 (σ0 x) ⊙0 τ1 (σ0 x)"
    by (meson local.tgt1_hom)
  also have "… = τ1 (σ0 x) ⊙0 τ1 (τ1 (σ0 x))"
    by simp
  also have "… = Tgt1 (σ0 x ⊙0 τ1 (σ0 x))"
    by (simp add: local.tgt1_hom)
  finally have "Tgt1 (σ0 x ⊙0 τ1 (σ0 x)) ≠ {}"
    by force
  hence "σ0 x ⊙0 τ1 (σ0 x) ≠ {}"
    by blast
  thus ?thesis
    using stmm0.s_absorb_var3 by auto
qed

lemma t0s1s0 [simp]: "τ0 (σ1 (σ0 x)) = σ0 x"
proof-
  have "{σ1 (σ0 x)} = Src1 (σ0 x ⊙0 σ0 x)"
    by simp
  also have "… =  σ1 (σ0 x) ⊙0 σ1 (σ0 x)"
    by (meson local.src1_hom)
  also have "… = σ1 (σ1 (σ0 x)) ⊙0 σ1 (σ0 x)"
    by simp
  also have "… = Src1 (σ1 (σ0 x) ⊙0 σ0 x)"
    using local.src1_hom by force
  finally  have "Src1 (σ1 (σ0 x) ⊙0 σ0 x) ≠ {}"
    by force 
  hence "σ1 (σ0 x) ⊙0 σ0 x ≠ {}"
    by blast
  thus ?thesis
    by (simp add: local.Dst0)
qed

lemma s1s0 [simp]: "σ1 (σ0 x) = σ0 x"
proof-
  have "{σ0 x} = σ0 x ⊙0 σ0 x"
    by simp
  also have "… = (σ1 (σ0 x) ⊙1 σ0 x) *0 (σ0 x ⊙1 τ1 (σ0 x))"
    by (simp add: multimagma.conv_atom)
  also have "… ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))"
    using local.interchange by blast
  also have "… = (σ1 (σ0 x) ⊙0 τ0 (σ1 (σ0 x))) *1 (σ0 (τ1 (σ0 x)) ⊙0 τ1 (σ0 x))"
    by simp
  also have "… = σ1 (σ0 x) ⊙1 τ1 (σ0 x)"
    using local.mm1.conv_atom local.src0_absorb local.tgt0_absorb by presburger
  finally have "{σ0 x} ⊆ σ1 (σ0 x) ⊙1 τ1 (σ0 x)".
  thus ?thesis
    by (metis empty_iff insert_subset singletonD stmm1.st_comm stmm1.st_prop stmm1.t_idem)
qed

lemma s1t0 [simp]: "σ1 (τ0 x) = τ0 x"
  by (metis local.s1s0 local.stmm0.stopp.ts_compat)

lemma t1s0 [simp]: "τ1 (σ0 x) = σ0 x"
  by (simp add: stmm1.st_fix)

lemma t1t0 [simp]: "τ1 (τ0 x) = τ0 x"
  by (simp add: stmm1.st_fix)

lemma comm_s0s1: "σ0 (σ1 x) = σ1 (σ0 x)"
proof-
  have "{σ1 x} = σ1 (σ0 x) ⊙0 σ1 x"
    by (metis image_empty image_insert local.src0_absorb local.src1_hom)
  also have "… = σ0 x ⊙0 σ1 x"
    by simp
  finally have "σ0 x ⊙0 σ1 x ≠ {}"
    by force
  hence "τ0 (σ0 x) = σ0 (σ1 x)"
    by (meson local.Dst0)
  hence "σ0 x = σ0 (σ1 x)"
    by simp
  thus ?thesis
    by simp
qed

lemma comm_s0t1: "σ0 (τ1 x) = τ1 (σ0 x)"
proof-
  have "{τ1 x} = τ1 (σ0 x) ⊙0 τ1 x"
    by (metis local.src0_absorb local.t1s0 local.tgt1_hom stmm0.s_absorb_var)
  hence "τ1 (σ0 x) ⊙0 τ1 x ≠ {}"
    by force 
  hence "τ0 (τ1 (σ0 x)) = σ0 (τ1 x)"
    using local.Dst0 by blast
  thus ?thesis
    by simp
qed

lemma comm_t0s1: "τ0 (σ1 x) = σ1 (τ0 x)"
proof-
  have "{σ1 x} = σ1 x ⊙0 σ1 (τ0 x)"
    by (metis local.s1t0 local.src1_hom local.stmm0.stopp.s_absorb_var local.tgt0_absorb)
  hence "σ1 x ⊙0 σ1 (τ0 x) ≠ {}"
    by force
  hence "τ0 (σ1 x) = τ0 (σ1 (τ0 x))"
    by (metis local.s1t0 local.stmm0.stopp.s_absorb_var stmm0.tt_idem)
  thus ?thesis
    by simp
qed

lemma comm_t0t1: "τ0 (τ1 x) = τ1 (τ0 x)"
  by (metis local.s1t0 local.stmm0.stopp.s_absorb_var3 local.tgt1_hom stmm1.st_fix)

lemma "σ0 x = σ1 x"
  (*nitpick [expect = genuine]*)
  oops

lemma "σ0 x = τ1 x"
  (*nitpick [expect = genuine]*)
  oops 

lemma "τ0 x = τ1 x"
  (*nitpick [expect = genuine]*)
  oops

lemma "σ0 x = τ0 x"
  (*nitpick [expect = genuine]*)
  oops

lemma "σ1 x = τ1 x"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙0 y = x ⊙1 y"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙0 y = y ⊙0 x"
  (*nitpick [expect = genuine]*)
  oops

lemma "x ⊙1 y = y ⊙1 x"
  (*nitpick [expect = genuine]*)
  oops

end

class two_catoid_red = catoid0 + catoid1 +
  assumes interchange: "(w ⊙1 x) *0 (y ⊙1 z) ⊆ (w ⊙0 y) *1 (x ⊙0 z)" (* irredundant *)
  and s1_hom: "Src1 (x ⊙0 y) ⊆ σ1 x ⊙0 σ1 y"  (* irredundant *)
  and t1_hom: "Tgt1 (x ⊙0 y) ⊆ τ1 x ⊙0 τ1 y" (* irredundant *)

begin

lemma s0t1s0 [simp]: "σ0 (τ1 (σ0 x)) = σ0 x"
proof-
  have "{σ0 x} = (σ1 (σ0 x) ⊙1 σ0 x) *0 (σ0 x ⊙1 τ1 (σ0 x))"
    by simp
  also have "… ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))"
    using local.interchange by blast
  finally have "{σ0 x} ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))".
  hence "(σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x)) ≠ {}"
    by fastforce
  hence "σ0 x ⊙0 τ1 (σ0 x) ≠ {}"
    using local.mm1.conv_exp2 by force
  thus ?thesis
    by (simp add: stmm0.s_absorb_var3)
qed

lemma t0s1s0 [simp]: "τ0 (σ1 (σ0 x)) = σ0 x"
proof-
  have "{σ0 x} = (σ1 (σ0 x) ⊙1 σ0 x) *0 (σ0 x ⊙1 τ1 (σ0 x))"
    by simp
  also have "… ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))"
    using local.interchange by blast
  finally have "{σ0 x} ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))".
  hence "(σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x)) ≠ {}"
    by fastforce
  hence "σ1 (σ0 x) ⊙0 σ0 x ≠ {}"
    using local.mm1.conv_exp2 by force
  thus ?thesis
    by (simp add: local.Dst0)
qed

lemma s1s0 [simp]: "σ1 (σ0 x) = σ0 x"
proof-
  have "{σ0 x} = σ0 x ⊙0 σ0 x"
    by simp
  also have "… = (σ1 (σ0 x) ⊙1 σ0 x) *0 (σ0 x ⊙1 τ1 (σ0 x))"
    by (simp add: multimagma.conv_atom)
  also have "… ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))"
    using local.interchange by blast
  also have "… = (σ1 (σ0 x) ⊙0 τ0 (σ1 (σ0 x))) *1 (σ0 (τ1 (σ0 x)) ⊙0 τ1 (σ0 x))"
    by (metis calculation empty_iff insert_subset local.t0s1s0 multimagma.conv_exp2 stmm0.s_absorb_var)
  also have "… = σ1 (σ0 x) ⊙1 τ1 (σ0 x)"
    using local.mm1.conv_atom local.src0_absorb local.tgt0_absorb by presburger
  finally have "{σ0 x} ⊆ σ1 (σ0 x) ⊙1 τ1 (σ0 x)".
  thus ?thesis
    using local.stmm1.stopp.Dst by fastforce
qed
 
lemma s1t0 [simp]: "σ1 (τ0 x) = τ0 x"
  by (metis local.s1s0 local.stmm0.stopp.ts_compat)

lemma t1s0 [simp]: "τ1 (σ0 x) = σ0 x" 
  by (simp add: stmm1.st_fix)

lemma t1t0 [simp]: "τ1 (τ0 x) = τ0 x"
  by (simp add: stmm1.st_fix)

lemma comm_s0s1: "σ0 (σ1 x) = σ1 (σ0 x)"
  by (metis image_empty image_insert local.s1_hom local.s1s0 local.src0_absorb order_class.order_eq_iff stmm0.s_absorb_var3)

lemma comm_s0t1: "σ0 (τ1 x) = τ1 (σ0 x)"
  by (metis local.src0_absorb local.src1_absorb local.stmsg1.ts_msg.src_comp_cond local.t1_hom local.t1s0 order_antisym_conv stmm0.s_absorb_var3 subset_insertI)

lemma comm_t0s1: "τ0 (σ1 x) = σ1 (τ0 x)"
  by (metis equalityI image_empty image_insert local.s1_hom local.s1t0 local.stmm0.stopp.s_absorb local.stmm0.stopp.s_absorb_var2)

lemma comm_t0t1: "τ0 (τ1 x) = τ1 (τ0 x)"
  by (metis empty_is_image local.src1_absorb local.stmm0.stopp.s_absorb_var2 local.stmsg1.ts_msg.src_comp_cond local.t1_hom local.t1t0 local.tgt0_absorb subset_antisym)

lemma s0_hom: "Src0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y"
proof cases
  assume "Src0 (x ⊙1 y) = {}"
  thus ?thesis
    by auto 
next
  assume h: "Src0 (x ⊙1 y) ≠ {}"
  hence h1: "τ1 x = σ1 y"
    by (simp add: local.Dst1)
  hence "Src0 (x ⊙1 y) = Src0 (Src1 (x ⊙1 y))"
    unfolding image_def using local.comm_s0s1 by auto 
  also have "… = Src0 (Src1 (x ⊙1 σ1 y))"
    using h stmsg1.src_local_cond by auto
  also have "… = Src0 (Src1 (x ⊙1 τ1 x))"
    using h1 by presburger
  also have  "… = {σ0 x}"
    by (simp add: local.comm_s0s1)
  also have "… = σ0 x ⊙1 τ1 (σ0 x)"
    using local.tgt1_absorb by presburger
  also have "… = σ0 x ⊙1 σ0 (τ1 x)"
    by (simp add: local.comm_s0t1)
  also have "… = σ0 x ⊙1 σ0 (σ1 y)"
    by (simp add: h1)
  also have "… = σ0 x ⊙1 σ0 y"
    by (simp add: local.comm_s0s1)
  finally show ?thesis
    by blast
qed

lemma t0_hom: "Tgt0 (x ⊙1 y) ⊆ τ0 x ⊙1 τ0 y"
  by (metis equals0D image_subsetI local.Dst1 local.comm_t0s1 local.comm_t0t1 local.stmsg1.ts_msg.src_comp_aux local.t1t0 local.tgt1_absorb singletonI)

end 

class two_catoid_red_strong = catoid0 + catoid1 +
  assumes interchange: "(w ⊙1 x) *0 (y ⊙1 z) ⊆ (w ⊙0 y) *1 (x ⊙0 z)" (* irredundant *)
  and s1_hom_strong: "Src1 (x ⊙0 y) = σ1 x ⊙0 σ1 y"  (* irredundant *)
  and t1_hom_strong: "Tgt1 (x ⊙0 y) = τ1 x ⊙0 τ1 y" (* irredundant *)

begin

lemma s0t1s0 [simp]: "σ0 (τ1 (σ0 x)) = σ0 x"
proof-
  have "{τ1 (σ0 x)} = Tgt1 (σ0 x ⊙0 σ0 x)"
    by simp
  also have "… = τ1 (σ0 x) ⊙0 τ1 (σ0 x)"
    using local.t1_hom_strong by blast
  also have "… = τ1 (σ0 x) ⊙0 τ1 (τ1 (σ0 x))"
    by simp
  also have "… = Tgt1 (σ0 x ⊙0 τ1 (σ0 x))"
    by (simp add: local.t1_hom_strong)
  finally have "Tgt1 (σ0 x ⊙0 τ1 (σ0 x)) ≠ {}"
    by force
  hence "σ0 x ⊙0 τ1 (σ0 x) ≠ {}"
    by blast
  thus ?thesis
    using stmm0.s_absorb_var3 by blast
qed

lemma t0s1s0 [simp]: "τ0 (σ1 (σ0 x)) = σ0 x"
proof-
  have "{σ1 (σ0 x)} = Src1 (σ0 x ⊙0 σ0 x)"
    by simp
  also have "… = σ1 (σ0 x) ⊙0 σ1 (σ0 x)"
    using local.s1_hom_strong by blast
  also have "… = σ1 (σ1 (σ0 x)) ⊙0 σ1 (σ0 x)"
    by simp
  also have "… = Src1 (σ1 (σ0 x) ⊙0 σ0 x)"
    using local.s1_hom_strong by auto
  finally  have "Src1 (σ1 (σ0 x) ⊙0 σ0 x) ≠ {}"
    by force 
  hence "σ1 (σ0 x) ⊙0 σ0 x ≠ {}"
    by blast
  thus ?thesis
    by (simp add: local.Dst0)
qed

lemma s1s0 [simp]: "σ1 (σ0 x) = σ0 x"
proof-
  have "{σ0 x} = σ0 x ⊙0 σ0 x"
    by simp
  also have "… = (σ1 (σ0 x) ⊙1 σ0 x) *0 (σ0 x ⊙1 τ1 (σ0 x))"
    by (simp add: multimagma.conv_atom)
  also have "… ⊆ (σ1 (σ0 x) ⊙0 σ0 x) *1 (σ0 x ⊙0 τ1 (σ0 x))"
    using local.interchange by blast
  also have "… = (σ1 (σ0 x) ⊙0 τ0 (σ1 (σ0 x))) *1 (σ0 (τ1 (σ0 x)) ⊙0 τ1 (σ0 x))"
    by simp
  also have "… = σ1 (σ0 x) ⊙1 τ1 (σ0 x)"
    using local.mm1.conv_atom local.src0_absorb local.tgt0_absorb by presburger
  finally have "{σ0 x} ⊆ σ1 (σ0 x) ⊙1 τ1 (σ0 x)".
  thus ?thesis
    using local.stmm1.stopp.Dst by fastforce
qed
 
lemma s1t0 [simp]: "σ1 (τ0 x) = τ0 x"
  by (metis local.s1s0 local.stmm0.stopp.ts_compat)

lemma t1s0 [simp]: "τ1 (σ0 x) = σ0 x"
  by (simp add: stmm1.st_fix)

lemma t1t0 [simp]: "τ1 (τ0 x) = τ0 x"
  by (simp add: stmm1.st_fix)

lemma comm_s0s1: "σ0 (σ1 x) = σ1 (σ0 x)"
  by (metis local.s1_hom_strong local.s1s0 stmm0.s_absorb_var)

lemma comm_s0t1: "σ0 (τ1 x) = τ1 (σ0 x)"
  by (metis local.t1_hom_strong local.t1s0 stmm0.s_absorb_var)

lemma comm_t0s1: "τ0 (σ1 x) = σ1 (τ0 x)"
  by (metis empty_not_insert local.Dst0 local.s1_hom_strong local.s1t0 local.tgt0_absorb)

lemma comm_t0t1: "τ0 (τ1 x) = τ1 (τ0 x)"
  using local.t1_hom_strong local.stmm0.stopp.s_absorb_var2 by fastforce

lemma s0_weak_hom: "Src0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y"
proof cases
  assume "Src0 (x ⊙1 y) = {}"
  thus ?thesis
    by auto 
next
  assume h: "Src0 (x ⊙1 y) ≠ {}"
  hence h1: "τ1 x = σ1 y"
    by (simp add: local.Dst1)
  hence "Src0 (x ⊙1 y) = Src0 (Src1 (x ⊙1 y))"
    unfolding image_def using local.comm_s0s1 by auto 
  also have "… = Src0 (Src1 (x ⊙1 σ1 y))"
    using h stmsg1.src_local_cond by auto
  also have "… = Src0 (Src1 (x ⊙1 τ1 x))"
    using h1 by presburger
  also have  "… = {σ0 x}"
    by (simp add: local.comm_s0s1)
  also have "… = σ0 x ⊙1 τ1 (σ0 x)"
    using local.tgt1_absorb by presburger
  also have "… = σ0 x ⊙1 σ0 (τ1 x)"
    by (simp add: local.comm_s0t1)
  also have "… = σ0 x ⊙1 σ0 (σ1 y)"
    by (simp add: h1)
  also have "… = σ0 x ⊙1 σ0 y"
    by (simp add: local.comm_s0s1)
  finally show ?thesis
    by blast
qed

lemma t0_weak_hom: "Tgt0 (x ⊙1 y) ⊆ τ0 x ⊙1 τ0 y"
  by (metis equals0D image_subsetI local.Dst1 local.comm_t0s1 local.comm_t0t1 local.stmsg1.ts_msg.src_comp_aux local.t1t0 local.tgt1_absorb singletonI)

end

class two_catoid_red2 = single_set_category0 + single_set_category1 +
  assumes comm_s0s1: "σ0 (σ1 x) = σ1 (σ0 x)"
  and comm_s0t1: "σ0 (τ1 x) = τ1 (σ0 x)"
  and comm_t0s1: "τ0 (σ1 x) = σ1 (τ0 x)"
  and comm_t0t1: "τ0 (τ1 x) = τ1 (τ0 x)"
  and s1s0 [simp]: "σ1 (σ0 x) = σ0 x"
  and s1t0 [simp]: "σ1 (τ0 x) = τ0 x"
  and t1s0 [simp]: "τ1 (σ0 x) = σ0 x"
  and t1t0 [simp]: "τ1 (τ0 x) = τ0 x"

begin

lemma "(w ⊙1 x) *0 (y ⊙1 z) ⊆ (w ⊙0 y) *1 (x ⊙0 z)"
  (*nitpick [expect = genuine]*)
  oops

lemma "Src1 (x ⊙0 y) ⊆ σ1 x ⊙0 σ1 y"
  (*nitpick [expect = genuine]*)
  oops

lemma "Tgt1 (x ⊙0 y) ⊆ τ1 x ⊙0 τ1 y"
  (*nitpick [expect = genuine]*)
  oops

lemma s0_hom: "Src0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y"
  by (smt (verit, ccfv_SIG) image_subsetI insertCI local.Dst1 local.comm_s0s1 local.comm_s0t1 local.src0_absorb local.t1s0 local.tgt1_absorb stmm0.s_absorb_var3 stmsg1.src_twisted_aux)
  

lemma t0_hom: "Tgt0 (x ⊙1 y) ⊆ τ0 x ⊙1 τ0 y"
  by (metis equals0D image_subsetI insertI1 local.comm_t0s1 local.comm_t0t1 local.stmm1.stopp.Dst local.t1t0 local.tgt1_absorb stmsg1.tgt_comp_aux)

end

class two_catoid_red3 = catoid0 + catoid1 +
  assumes interchange: "(w ⊙1 x) *0 (y ⊙1 z) ⊆ (w ⊙0 y) *1 (x ⊙0 z)" 
  and s1_hom: "Src0 (x ⊙1 y) ⊆ σ0 x ⊙1 σ0 y" 
  and t1_hom: "Tgt0 (x ⊙1 y) ⊆ τ0 x ⊙1 τ0 y" 

lemma (in two_catoid_red3)
  "Src1 (x ⊙0 y) ⊆ σ1 x ⊙0 σ1 y"
  (*nitpick [expect = genuine]*)
  oops

lemma (in two_catoid_red3)
  "Tgt1 (x ⊙0 y) ⊆ τ1 x ⊙0 τ1 y"
  (*nitpick [expect = genuine]*)
  oops

end