Theory CubicalCategories

(*
Title: Cubical Categories
Authors: Tanguy Massacrier, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section‹Cubical Categories›

theory CubicalCategories
  imports ICatoids

begin

text ‹All categories considered in this component are single-set categories.›

subsection ‹Semi-cubical $\omega$-categories›

text ‹We first define a class for cubical $\omega$-categories without symmetries.›

class semi_cubical_omega_category = icategory +
  assumes face_comm: "i ≠ j ⟹ ∂ i α ∘ ∂ j β = ∂ j β ∘ ∂ i α"
  and face_func: "i ≠ j ⟹ DD j x y ⟹ ∂ i α (x ⊗⇘j⇙ y) = ∂ i α x ⊗⇘j⇙ ∂ i α y"
  and interchange: "i ≠ j ⟹ DD i w x ⟹ DD i y z ⟹ DD j w y ⟹ DD j x z 
                           ⟹ (w ⊗⇘i⇙ x) ⊗⇘j⇙ (y ⊗⇘i⇙ z) = (w ⊗⇘j⇙ y) ⊗⇘i⇙ (x ⊗⇘j⇙ z)"
  and fin_fix: "∃k.∀i. k ≤ i ⟶ fFx i x"

begin

lemma pcomp_face_func_DD: "i ≠ j ⟹ DD j x y ⟹ DD j (∂ i α x) (∂ i α y)"
  by (metis comp_apply icat.st_local local.face_comm)

lemma comp_face_func: "i ≠ j ⟹ (∂∂ i α) (x ⊙⇘j⇙ y) ⊆ ∂ i α x ⊙⇘j⇙ ∂ i α y"
  using local.icat.pcomp_def_var local.icat.pcomp_def_var4 local.face_func pcomp_face_func_DD by fastforce

lemma interchange_var: 
  assumes "i ≠ j"
  and "(w ⊙⇘i⇙ x) ⋆⇘j⇙ (y ⊙⇘i⇙ z) ≠ {}"
  and "(w ⊙⇘j⇙ y) ⋆⇘i⇙ (x ⊙⇘j⇙ z) ≠ {}"
  shows "(w ⊙⇘i⇙ x) ⋆⇘j⇙ (y ⊙⇘i⇙ z) = (w ⊙⇘j⇙ y) ⋆⇘i⇙ (x ⊙⇘j⇙ z)" 
proof-
  have h1: "DD i w x"
    using assms(2) local.ims.conv_def by force
  have h2: "DD i y z"
    using assms(2) multimagma.conv_distl by force
  have h3: "DD j w y"
    using assms(3) multimagma.conv_def by force
  have h4: "DD j x z"
    using assms(3) local.icid.stopp.conv_def by force
  have "(w ⊙⇘i⇙ x) ⋆⇘j⇙ (y ⊙⇘i⇙ z) = {w ⊗⇘i⇙ x} ⋆⇘j⇙ {y ⊗⇘i⇙ z}"
    using h1 h2 local.icat.pcomp_def_var4 by force
  also have "… = {(w ⊗⇘i⇙ x) ⊗⇘j⇙ (y ⊗⇘i⇙ z)}"
    using assms(2) calculation local.icat.pcomp_def_var4 by force
  also have "… = {(w ⊗⇘j⇙ y) ⊗⇘i⇙ (x ⊗⇘j⇙ z)}"
    by (simp add: assms(1) h1 h2 h3 h4 local.interchange)
  also have "… = {w ⊗⇘j⇙ y} ⋆⇘i⇙ {x ⊗⇘j⇙ z}"
    by (metis assms(3) h3 h4 local.icat.pcomp_def_var4 multimagma.conv_atom)
  also have "… = (w ⊙⇘j⇙ y) ⋆⇘i⇙ (x ⊙⇘j⇙ z)"
    using h3 h4 local.icat.pcomp_def_var4 by force
  finally show ?thesis.
qed

lemma interchange_var2: 
  assumes "i ≠ j"
  and "(⋃a ∈ w ⊙⇘i⇙ x. ⋃b ∈ y ⊙⇘i⇙ z. a ⊙⇘j⇙ b) ≠ {}"
  and "(⋃c ∈ w ⊙⇘j⇙ y. ⋃d ∈ x ⊙⇘j⇙ z. c ⊙⇘i⇙ d) ≠ {}"
  shows "(⋃a ∈ w ⊙⇘i⇙ x. ⋃b ∈ y ⊙⇘i⇙ z. a ⊙⇘j⇙ b) = (⋃c ∈ w ⊙⇘j⇙ y. ⋃d ∈ x ⊙⇘j⇙ z. c ⊙⇘i⇙ d)"
proof-
  have "{(w ⊗⇘i⇙ x) ⊗⇘j⇙ (y ⊗⇘i⇙ z)} = {(w ⊗⇘j⇙ y) ⊗⇘i⇙ (x ⊗⇘j⇙ z)}"
    using assms(1) assms(2) assms(3) local.interchange by fastforce
  thus ?thesis
    by (metis assms(1) assms(2) assms(3) interchange_var multimagma.conv_def)
qed

lemma face_compat: "∂ i α ∘ ∂ i β  = ∂ i β"
  by (metis (full_types, lifting) ext comp_def[of "∂ i tt" "∂ i tt"] comp_def[of "∂ i tt" "∂ i ff"]
      comp_def[of "∂ i ff" "∂ i tt"] comp_def[of "∂ i ff" "∂ i ff"] icid.ts_compat[of i]
      local.icid.stopp.ts_compat[of i])

lemma face_compat_var [simp]: "∂ i α (∂ i β x) = ∂ i β x"
  by (metis (full_types) icid.ts_compat local.icid.stopp.ts_compat)

lemma face_comm_var: "i ≠ j ⟹ ∂ i α (∂ j β x) = ∂ j β (∂ i α x)"
  by (meson comp_eq_dest local.face_comm)

lemma face_comm_lift: "i ≠ j ⟹ ∂∂ i α (∂∂ j β X) = ∂∂ j β (∂∂ i α X)"
  by (simp add: image_comp local.face_comm)

lemma face_func_lift: "i ≠ j ⟹ (∂∂ i α) (X ⋆⇘j⇙ Y) ⊆ ∂∂ i α X ⋆⇘j⇙ ∂∂  i α Y"
  using ims.conv_def comp_face_func dual_order.refl image_subset_iff by fastforce

lemma pcomp_lface: "DD i x y ⟹ ∂ i ff (x ⊗⇘i⇙ y) = ∂ i ff x"
  by (simp add: icat.st_local local.icat.sscatml.locall_var)

lemma pcomp_uface: "DD i x y ⟹ ∂ i tt (x ⊗⇘i⇙ y) = ∂ i tt y"
  using icat.st_local local.icat.sscatml.localr_var by force

lemma interchange_DD1:
  assumes "i ≠ j"
  and "DD i w x"
  and "DD i y z"
  and "DD j w y"
  and "DD j x z"
  shows "DD j (w ⊗⇘i⇙ x) (y ⊗⇘i⇙ z)"
proof-
  have a: "∂ j tt (w ⊗⇘i⇙ x) = ∂ j tt w ⊗⇘i⇙ ∂ j tt x"
    using assms(1) assms(2) face_func by simp
  also have "…  = ∂ j ff y ⊗⇘i⇙ ∂ j ff z"
    using assms(4) assms(5) local.iDst by simp
  also have "… = ∂ j ff (y ⊗⇘i⇙ z)"
    using assms(1) assms(3) face_func by simp
  finally show ?thesis
    using local.locality by simp
qed

lemma interchange_DD2:
  assumes "i ≠ j"
  and "DD i w x"
  and "DD i y z"
  and "DD j w y"
  and "DD j x z"
  shows "DD i (w ⊗⇘j⇙ y) (x ⊗⇘j⇙ z)"
  using assms interchange_DD1 by simp
                             
lemma face_idem1: "∂ i α x = ∂ i β y ⟹ ∂ i α x ⊙⇘i⇙ ∂ i β y = {∂ i α x}"
  by (metis face_compat_var local.it_absorb)

lemma face_pidem1: "∂ i α x = ∂ i β y ⟹ ∂ i α x ⊗⇘i⇙ ∂ i β y = ∂ i α x"
  by (metis face_compat_var local.icat.sscatml.l0_absorb)

lemma face_pidem2: "∂ i α x ≠ ∂ i β y ⟹ ∂ i α x ⊙⇘i⇙ ∂ i β y = {}"
  using icat.st_local by force

lemma face_fix_comp_var: "i ≠ j ⟹ ∂∂ i α (∂ i α x ⊙⇘j⇙ ∂ i α y) = ∂ i α x ⊙⇘j⇙ ∂ i α y"
  by (metis (mono_tags, lifting) comp_face_func empty_is_image face_compat_var local.icat.pcomp_def_var4 subset_singletonD)

lemma interchange_lift_aux: "x ∈ X ⟹ y ∈ Y ⟹ DD i x y ⟹ x ⊗⇘i⇙ y ∈ X ⋆⇘i⇙ Y"
  using local.icat.pcomp_def_var local.ims.conv_exp2 by blast

lemma interchange_lift1:
  assumes "i ≠ j"
  and "∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. DD i w x ∧ DD i y z ∧ DD j w y ∧ DD j x z"
  shows "((W ⋆⇘i⇙ X) ⋆⇘j⇙ (Y ⋆⇘i⇙ Z)) ∩ ((W ⋆⇘j⇙ Y) ⋆⇘i⇙ (X ⋆⇘j⇙ Z)) ≠ {}"
proof-
  obtain w x y z where h1: "w ∈ W ∧ x ∈ X ∧ y ∈ Y ∧ z ∈ Z ∧ DD i w x ∧ DD i y z ∧ DD j w y ∧ DD j x z"
    using assms(2) by blast
  have h5: "(w ⊗⇘i⇙ x) ⊗⇘j⇙ (y ⊗⇘i⇙ z) ∈ (W ⋆⇘i⇙ X) ⋆⇘j⇙ (Y ⋆⇘i⇙ Z)"
    using assms(1) h1 interchange_lift_aux interchange_DD2 by presburger
  have "(w ⊗⇘j⇙ y) ⊗⇘i⇙ (x ⊗⇘j⇙ z) ∈ (W ⋆⇘j⇙ Y) ⋆⇘i⇙ (X ⋆⇘j⇙ Z)"
    by (simp add: assms(1) h1 interchange_lift_aux interchange_DD2)
  thus ?thesis
    using assms(1) h1 h5 local.interchange by fastforce
qed

lemma interchange_lift2:
  assumes "i ≠ j"
  and "∀w ∈ W. ∀x ∈ X. ∀y ∈ Y. ∀z ∈ Z. DD i w x ∧ DD i y z ∧ DD j w y ∧ DD j x z"
  shows "((W ⋆⇘i⇙ X) ⋆⇘j⇙ (Y ⋆⇘i⇙ Z)) = ((W ⋆⇘j⇙ Y) ⋆⇘i⇙ (X ⋆⇘j⇙ Z))"
proof-
  {fix t
    have "(t ∈ (W ⋆⇘i⇙ X) ⋆⇘j⇙ (Y ⋆⇘i⇙ Z)) = (∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. DD i w x ∧ DD i y z ∧ DD j (w ⊗⇘i⇙ x) (y ⊗⇘i⇙ z) ∧ t = (w ⊗⇘i⇙ x) ⊗⇘j⇙ (y ⊗⇘i⇙ z))"
    unfolding iconv_prop by force
  also have "… = (∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. DD i w x ∧ DD i y z ∧ DD j w y ∧ DD j x z ∧ t = (w ⊗⇘i⇙ x) ⊗⇘j⇙ (y ⊗⇘i⇙ z))"
    using assms(1) assms(2) interchange_DD2 by simp
  also have "… = (∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. DD j w y ∧ DD j x z ∧ DD j w y ∧ DD j x z ∧ t = (w ⊗⇘j⇙ y) ⊗⇘i⇙ (x ⊗⇘j⇙ z))"
    by (simp add: assms(1) assms(2) local.interchange)
  also have "… = (∃w ∈ W. ∃x ∈ X. ∃y ∈ Y. ∃z ∈ Z. DD j w y ∧ DD j x z ∧ DD i (w ⊗⇘j⇙ y) (x ⊗⇘j⇙ z) ∧ t = (w ⊗⇘j⇙ y) ⊗⇘i⇙ (x ⊗⇘j⇙ z))"
    using assms(1) assms(2) interchange_DD1 by simp
  also have "… = (t ∈ (W ⋆⇘j⇙ Y) ⋆⇘i⇙ (X ⋆⇘j⇙ Z))"
    unfolding iconv_prop by force
  finally have "(t ∈ (W ⋆⇘i⇙ X) ⋆⇘j⇙ (Y ⋆⇘i⇙ Z)) = (t ∈ (W ⋆⇘j⇙ Y) ⋆⇘i⇙ (X ⋆⇘j⇙ Z))"
    by blast}
  thus ?thesis
    by force
qed

lemma double_fix_prop: "(∂ i α (∂ j β x) = x) = (fFx i x ∧ fFx j x)"
  by (metis face_comm_var face_compat_var)

end


subsection ‹Type classes for cubical $\omega$-categories›

abbreviation diffSup :: "nat ⇒ nat ⇒ nat ⇒ bool" where
  "diffSup i j k ≡ (i - j ≥ k ∨ j - i ≥ k)"

class symmetry_ops =
  fixes symmetry :: "nat ⇒ 'a ⇒ 'a" (‹σ›)
  and inv_symmetry :: "nat ⇒ 'a ⇒ 'a" (‹θ›) 

begin

abbreviation "σσ i ≡ image (σ i)"

abbreviation "θθ i ≡ image (θ i)"

text ‹symcomp i j composes the symmetry maps from index i to index i+j-1.›

primrec symcomp :: "nat ⇒ nat ⇒ 'a ⇒ 'a" (‹Σ›) where
    "Σ i 0 x = x"
  | "Σ i (Suc j) x = σ (i + j) (Σ i j x)"

text ‹inv-symcomp i j composes the inverse symmetries from i+j-1 to i.›

primrec inv_symcomp :: "nat ⇒ nat ⇒ 'a ⇒ 'a" (‹Θ›) where
    "Θ i 0 x = x"
  | "Θ i (Suc j) x = Θ i j (θ (i + j) x)"

end

text ‹Next we define a class for cubical $\omega$-categories.›

class cubical_omega_category = semi_cubical_omega_category + symmetry_ops +
  assumes sym_type: "σσ i (face_fix i) ⊆ face_fix (i + 1)"
  and inv_sym_type: "θθ i (face_fix (i + 1)) ⊆ face_fix i"
  and sym_inv_sym: "fFx (i + 1) x ⟹ σ i (θ i x) = x"
  and inv_sym_sym: "fFx i x  ⟹ θ i (σ i x) = x"
  and sym_face1: "fFx i x ⟹ ∂ i α (σ i x) = σ i (∂ (i + 1) α x)"
  and sym_face2: "i ≠ j ⟹ i ≠ j + 1 ⟹ fFx j x ⟹ ∂ i α (σ j x) = σ j (∂ i α x)"
  and sym_func: "i ≠ j ⟹ fFx i x ⟹ fFx i y ⟹ DD j x y ⟹ 
                     σ i (x ⊗⇘j⇙ y) = (if j = i + 1 then σ i x ⊗⇘i⇙ σ i y else σ i x ⊗⇘j⇙ σ i y)"
  and sym_fix: "fFx i x ⟹ fFx (i + 1) x ⟹ σ i x = x"
  and sym_sym_braid: "diffSup i j 2 ⟹ fFx i x ⟹ fFx j x  ⟹ σ i (σ j x) = σ j (σ i x)"

begin

text ‹First we prove variants of the axioms.›

lemma sym_type_var: "fFx i x ⟹ fFx (i + 1) (σ i x)"
  by (meson image_subset_iff local.face_fix_prop local.sym_type)

lemma sym_type_var1 [simp]: "∂ (i + 1) α (σ i (∂ i α x)) = σ i (∂ i α x)"
  by (metis local.face_compat_var sym_type_var)

lemma sym_type_var2 [simp]: "∂ (i + 1) α ∘ σ i ∘ ∂ i α = σ i ∘ ∂ i α"
  unfolding comp_def fun_eq_iff using sym_type_var1 by simp

lemma sym_type_var_lift_var [simp]: "∂∂ (i + 1) α (σσ i (∂∂ i α X)) = σσ i (∂∂ i α X)"
  by (metis image_comp sym_type_var2)

lemma sym_type_var_lift [simp]: 
  assumes "FFx i X"
  shows "∂∂ (i + 1) α (σσ i X) = σσ i X"
proof-
  have "∂∂ (i + 1) α (σσ i X) = {∂ (i + 1) α (σ i x) |x. x ∈ X}"
    by blast
  also have "…  = {σ i x |x. x ∈ X}"
    by (metis assms local.fFx_prop sym_type_var)
  also have "… = σσ i X"
    by (simp add: setcompr_eq_image)
  finally show ?thesis.
qed

lemma inv_sym_type_var: "fFx (i + 1) x ⟹ fFx i (θ i x)"
  by (meson image_subset_iff local.face_fix_prop local.inv_sym_type)

lemma inv_sym_type_var1 [simp]: "∂ i α (θ i (∂ (i + 1) α x)) = θ i (∂ (i + 1) α x)"
  by (metis inv_sym_type_var local.face_compat_var)

lemma inv_sym_type_var2 [simp]: "∂ i α ∘ θ i ∘ ∂ (i + 1) α = θ i ∘ ∂ (i + 1) α"
  unfolding comp_def fun_eq_iff using inv_sym_type_var1 by simp

lemma inv_sym_type_lift_var [simp]: "∂∂ i α (θθ i (∂∂ (i + 1) α X)) = θθ i (∂∂ (i + 1) α X)"
  by (metis image_comp inv_sym_type_var2)

lemma inv_sym_type_lift: 
  assumes "FFx (i + 1) X"
  shows "∂∂ i α (θθ i X) = θθ i X"
  by (smt (verit, best) assms image_cong image_ident inv_sym_type_lift_var
      local.icid.stopp.ST_compat)

lemma sym_inv_sym_var1 [simp]: "σ i (θ i (∂ (i + 1) α x)) = ∂ (i + 1) α x"
  by (simp add: local.sym_inv_sym)

lemma sym_inv_sym_var2 [simp]: "σ i ∘ θ i ∘ ∂ (i + 1) α = ∂ (i + 1) α"
  unfolding comp_def fun_eq_iff using sym_inv_sym_var1 by simp

lemma sym_inv_sym_lift_var: "σσ i (θθ i (∂∂ (i + 1) α X)) = ∂∂ (i + 1) α X"
  by (metis image_comp sym_inv_sym_var2)

lemma sym_inv_sym_lift: 
  assumes "FFx (i + 1) X"
  shows "σσ i (θθ i X) = X"
proof-
  have "σσ i (θθ i X) = {σ i (θ i x) |x. x ∈ X}"
    by blast
  thus ?thesis
    using assms local.sym_inv_sym by force
qed

lemma inv_sym_sym_var1 [simp]: "θ i (σ i (∂ i α x)) = ∂ i α x"
  by (simp add: local.inv_sym_sym)

lemma inv_sym_sym_var2 [simp]: "θ i ∘ σ i ∘ ∂ i α = ∂ i α"
  unfolding comp_def fun_eq_iff by simp

lemma inv_sym_sym_lift_var [simp]: "θθ i (σσ i (∂∂ i α X)) = ∂∂ i α X"
  by (simp add: image_comp)

lemma inv_sym_sym_lift: 
  assumes "FFx i X"
  shows "θθ i (σσ i X) = X"
  by (metis assms image_cong image_ident inv_sym_sym_lift_var)

lemma sym_fix_var1 [simp]: "σ i (∂ i α (∂ (i + 1) β x)) = ∂ i α (∂ (i + 1) β x)"
  by (simp add: local.face_comm_var local.sym_fix)

lemma sym_fix_var2 [simp]: "σ i ∘ ∂ i α ∘ ∂ (i + 1) β = ∂ i α ∘ ∂ (i + 1) β"
  unfolding comp_def fun_eq_iff using sym_fix_var1 by simp

lemma sym_fix_lift_var: "σσ i (∂∂ i α (∂∂ (i + 1) β X)) = ∂∂ i α (∂∂ (i + 1) β X)"
  by (metis image_comp sym_fix_var2)

lemma sym_fix_lift: 
  assumes "FFx i X"
  and "FFx (i + 1) X"
  shows "σσ i X = X"
  using assms local.sym_fix by simp

lemma sym_face1_var1: "∂ i α (σ i (∂ i β x)) = σ i (∂ (i + 1) α (∂ i β x))"
  by (simp add: local.sym_face1)

lemma sym_face1_var2: "∂ i α ∘ σ i ∘ ∂ i β  = σ i ∘ ∂ (i + 1) α ∘ ∂ i β"
  by (simp add: comp_def local.sym_face1)

lemma sym_face1_lift_var: "∂∂ i α (σσ i (∂∂ i β X)) = σσ i (∂∂ (i + 1) α (∂∂ i β X))"
  by (metis image_comp sym_face1_var2)

lemma sym_face1_lift: 
  assumes "FFx i X"
  shows "∂∂ i α (σσ i X) = σσ i (∂∂ (i + 1) α X)"
  by (metis (lifting) ext assms inv_sym_sym_lift inv_sym_type_lift_var sym_face1_lift_var
      sym_type_var_lift)

lemma sym_face2_var1: 
  assumes "i ≠ j"
  and "i ≠ j + 1"
  shows "∂ i α (σ j (∂ j β x)) = σ j (∂ i α (∂ j β x))"
  using assms local.sym_face2 by simp

lemma sym_face2_var2: 
  assumes "i ≠ j"
  and "i ≠ j + 1"
  shows  "∂ i α ∘ σ j ∘ ∂ j β = σ j ∘ ∂ i α ∘ ∂ j β"
  unfolding comp_def fun_eq_iff using assms sym_face2_var1 by simp

lemma sym_face2_lift_var: 
  assumes "i ≠ j"
  and "i ≠ j + 1"
  shows "∂∂ i α (σσ j (∂∂ j β X)) = σσ j (∂∂ i α (∂∂ j β X))"
  by (metis assms image_comp sym_face2_var2)

lemma sym_face2_lift: 
  assumes "i ≠ j"
  and "i ≠ j + 1"
  and "FFx j X"
  shows "∂∂ i α (σσ j X) = σσ j (∂∂ i α X)"
  by (smt (z3) assms image_cong image_image sym_face2_var1)

lemma sym_sym_braid_var1: 
  assumes "diffSup i j 2"
  shows "σ i (σ j (∂ i α (∂ j β x))) = σ j (σ i (∂ i α (∂ j β x)))"
  using assms local.face_comm_var local.sym_sym_braid by force

lemma sym_sym_braid_var2: 
  assumes "diffSup i j 2"
  shows "σ i ∘ σ j ∘ ∂ i α ∘ ∂ j β = σ j ∘ σ i ∘ ∂ i α ∘ ∂ j β"
  using assms sym_sym_braid_var1 by fastforce

lemma sym_sym_braid_lift_var: 
  assumes "diffSup i j 2"
  shows "σσ i (σσ j (∂∂ i α (∂∂ j β X))) = σσ j (σσ i (∂∂ i α (∂∂ j β X)))"
proof-
  have "σσ i (σσ j (∂∂ i α (∂∂ j β X))) = {σ i (σ j (∂ i α (∂ j β x))) |x. x ∈ X}"
    by blast
  also have "… = {σ j (σ i (∂ i α (∂ j β x))) |x. x ∈ X}"
    by (metis (full_types, opaque_lifting) assms sym_sym_braid_var1)
  finally show ?thesis
    by (simp add: Setcompr_eq_image image_image)
qed

lemma sym_sym_braid_lift: 
  assumes "diffSup i j 2"
  and "FFx i X"
  and "FFx j X"
  shows "σσ i (σσ j X) = σσ j (σσ i X)"
  by (smt (verit, best) assms(1,2,3) comp_apply image_comp image_cong local.sym_sym_braid)

lemma sym_func2: 
  assumes "fFx i x" 
  and "fFx i y" 
  and "DD (i + 1) x y"
  shows "σ i (x ⊗⇘(i + 1)⇙ y) = σ i x ⊗⇘i⇙ σ i y"
  using assms local.sym_func by simp

lemma sym_func3: 
  assumes "i ≠ j"
  and "j ≠ i + 1"
  and "fFx i x"
  and "fFx i y"
  and "DD j x y" 
  shows "σ i (x ⊗⇘j⇙ y) = σ i x ⊗⇘j⇙ σ i y"
  using assms local.sym_func by simp

lemma sym_func2_var1:
  assumes "DD (i + 1) (∂ i α x) (∂ i β y)"
  shows "σ i (∂ i α x ⊗⇘(i + 1)⇙ ∂ i β y) = σ i (∂ i α x) ⊗⇘i⇙ σ i (∂ i β y)"
  using assms local.face_compat_var local.sym_func2 by simp

lemma sym_func3_var1: 
  assumes "i ≠ j" 
  and "j ≠ i + 1"
  and "DD j (∂ i α x) (∂ i β y)" 
  shows "σ i (∂ i α x ⊗⇘j⇙ ∂ i β y) = σ i (∂ i α x) ⊗⇘j⇙ σ i (∂ i β y)"
  using assms local.face_compat_var local.sym_func3 by simp

lemma sym_func2_DD: 
  assumes "fFx i x"
  and "fFx i y" 
  shows "DD (i + 1) x y = DD i (σ i x) (σ i y)"
  by (metis assms icat.st_local local.face_comm_var local.sym_face1 sym_fix_var1)

lemma func2_var2: "σσ i (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = σ i (∂ i α x) ⊙⇘i⇙ σ i (∂ i β y)"
proof (cases "DD (i + 1) (∂ i α x) (∂ i β y)")
  case True
  have "σσ i (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = σσ i {∂ i α x ⊗⇘(i + 1)⇙ ∂ i β y}"
    using True local.icat.pcomp_def_var4 by simp
  also have "… = {σ i (∂ i α x ⊗⇘(i + 1)⇙ ∂ i β y)}"
    by simp
  also have "… = {σ i (∂ i α x) ⊗⇘i⇙ σ i (∂ i β y)}"
    using True sym_func2_var1 by simp
  also have "… = σ i (∂ i α x) ⊙⇘i⇙ σ i (∂ i β y)"
    using True local.icat.pcomp_def_var4 sym_func2_DD by simp
  finally show ?thesis.
next
  case False
  thus ?thesis
    using local.sym_func2_DD by simp
qed

lemma sym_func2_lift_var1: "σσ i (∂∂ i α X ⋆⇘(i + 1)⇙ ∂∂ i β Y) = σσ i (∂∂ i α X) ⋆⇘i⇙ σσ i (∂∂ i β Y)"
proof-
  have "σσ i (∂∂ i α X ⋆⇘(i + 1)⇙ ∂∂ i β Y) = σσ i {x ⊗⇘(i + 1)⇙ y |x y. x ∈ ∂∂ i α X ∧ y ∈ ∂∂ i β Y ∧ DD (i + 1) x y}"
    using local.iconv_prop by presburger
  also have "… = {σ i (∂ i α x ⊗⇘(i + 1)⇙ ∂ i β y) |x y. x ∈ X ∧ y ∈ Y ∧ DD (i + 1) (∂ i α x) (∂ i β y)}"
    by blast
  also have "… = {σ i (∂ i α x) ⊗⇘i⇙ σ i (∂ i β y) |x y. x ∈ X ∧ y ∈ Y ∧ DD i (σ i (∂ i α x)) (σ i (∂ i β y))}"
    using func2_var2 sym_func2_var1 by fastforce
  also have "… = {x ⊗⇘i⇙ y |x y. x ∈ σσ i (∂∂ i α X) ∧ y ∈ σσ i (∂∂ i β Y) ∧ DD i x y}"
    by blast
  also have "… = σσ i (∂∂ i α X) ⋆⇘i⇙ σσ i (∂∂ i β Y)"
    using local.iconv_prop by presburger
  finally show ?thesis.
qed

lemma sym_func2_lift: 
  assumes "FFx i X"
  and "FFx i Y"
  shows "σσ i (X ⋆⇘(i + 1)⇙ Y) = σσ i X ⋆⇘i⇙ σσ i Y"
proof-
  have "σσ i (X ⋆⇘(i + 1)⇙ Y) = σσ i (∂∂ i tt X ⋆⇘(i + 1)⇙ ∂∂ i tt Y)"
    by (smt (verit) assms image_cong image_ident local.icid.stopp.ST_compat)
  also have "… = σσ i (∂∂ i tt X) ⋆⇘i⇙ σσ i (∂∂ i tt Y)"
    using sym_func2_lift_var1 by simp
  also have "… = σσ i X ⋆⇘i⇙ σσ i Y"
    using assms icid.st_eq1 by simp
  finally show ?thesis.
qed

lemma func3_var1: 
  assumes "i ≠ j"
  and "j ≠ i + 1" 
  shows "σσ i (∂ i α x ⊙⇘j⇙ ∂ i β y) = σ i (∂ i α x) ⊙⇘j⇙ σ i (∂ i β y)"
proof (cases "DD j (∂ i α x) (∂ i β y)")
  case True
  have "σσ i (∂ i α x ⊙⇘j⇙ ∂ i β y) = σσ i {∂ i α x ⊗⇘j⇙ ∂ i β y}"
    using True local.icat.pcomp_def_var4 by simp
  also have "… = {σ i (∂ i α x ⊗⇘j⇙ ∂ i β y)}"
    by simp
  also have "… = {σ i (∂ i α x) ⊗⇘j⇙ σ i (∂ i β y)}"
    using True assms sym_func3_var1 by simp
  also have "… = σ i (∂ i α x) ⊙⇘j⇙ σ i (∂ i β y)"
    using True assms icat.st_local local.icat.pcomp_def_var4 sym_face2_var1 by simp
  finally show ?thesis.
next
  case False
  thus ?thesis
    by (metis assms empty_is_image icat.st_local inv_sym_sym_var1 local.face_comm_var sym_face2_var1)
qed

lemma sym_func3_lift_var1: 
  assumes "i ≠ j"
  and "j ≠ i + 1" 
  shows "σσ i (∂∂ i α X ⋆⇘j⇙ ∂∂ i β Y) = σσ i (∂∂ i α X) ⋆⇘j⇙ σσ i (∂∂ i β Y)"
proof-
  have "σσ i (∂∂ i α X ⋆⇘j⇙ ∂∂ i β Y) = σσ i {x ⊗⇘j⇙ y |x y. x ∈ ∂∂ i α X ∧ y ∈ ∂∂ i β Y ∧ DD j x y}"
    using local.iconv_prop by presburger
  also have "… = {σ i (∂ i α x ⊗⇘j⇙ ∂ i β y) |x y. x ∈ X ∧ y ∈ Y ∧ DD j (∂ i α x) (∂ i β y)}"
    by force
  also have "… = {σ i (∂ i α x) ⊗⇘j⇙ σ i (∂ i β y) |x y. x ∈ X ∧ y ∈ Y ∧ DD j (σ i (∂ i α x)) (σ i (∂ i β y))}"
    using assms func3_var1 sym_func3_var1 by fastforce
  also have "… = {x ⊗⇘j⇙ y |x y. x ∈ σσ i (∂∂ i α X) ∧ y ∈ σσ i (∂∂ i β Y) ∧ DD j x y}"
    by force
  also have "… = σσ i (∂∂ i α X) ⋆⇘j⇙ σσ i (∂∂ i β Y)"
    using local.iconv_prop by presburger
  finally show ?thesis.
qed

lemma sym_func3_lift: 
  assumes "i ≠ j"
  and "j ≠ i + 1"
  and "FFx i X"
  and "FFx i Y"
  shows "σσ i (X ⋆⇘j⇙ Y) = σσ i X ⋆⇘j⇙ σσ i Y"
proof-
  have "σσ i (X ⋆⇘j⇙ Y) = σσ i (∂∂ i tt X ⋆⇘j⇙ ∂∂ i tt Y)"
    by (smt (verit) assms(3) assms(4) image_cong image_ident local.icid.stopp.ST_compat)
  also have "… = σσ i (∂∂ i tt X) ⋆⇘j⇙ σσ i (∂∂ i tt Y)"
    using assms(1) assms(2) sym_func3_lift_var1 by presburger
  also have "… = σσ i X ⋆⇘j⇙ σσ i Y"
    using assms(3) assms(4) icid.st_eq1 by simp
  finally show ?thesis.
qed

lemma sym_func3_var2: "i ≠ j ⟹ σσ i (∂ i α x ⊙⇘j⇙ ∂ i β y) = (if j = i + 1 then σ i (∂ i α x) ⊙⇘i⇙ σ i (∂ i β y) else σ i (∂ i α x) ⊙⇘j⇙ σ i (∂ i β y))"
  using func2_var2 func3_var1 by simp

text ‹Symmetries and inverse symmetries form a bijective pair on suitable fixpoints of the face maps.›

lemma sym_inj: "inj_on (σ i) (face_fix i)"
  by (smt (verit, del_insts) CollectD inj_onI local.inv_sym_sym)

lemma sym_inj_var: 
  assumes "fFx i x"
  and "fFx i y"
  and "σ i x = σ i y"
  shows "x = y"
  by (metis assms inv_sym_sym_var1)

lemma inv_sym_inj: "inj_on (θ i) (face_fix (i + 1))"
  by (smt (verit, del_insts) CollectD inj_onI local.sym_inv_sym)

lemma inv_sym_inj_var: 
  assumes "fFx (i + 1) x"
  and "fFx (i + 1) y"
  and "θ i x = θ i y"
  shows "x = y"
  by (metis assms local.sym_inv_sym)

lemma surj_sym: "image (σ i) (face_fix i) = face_fix (i + 1)"
  by (safe, metis sym_type_var1, smt (verit, del_insts) imageI inv_sym_type_var1 mem_Collect_eq sym_inv_sym_var1)

lemma surj_inv_sym: "image (θ i) (face_fix (i + 1)) = face_fix i"
  by (safe, metis inv_sym_type_var1, smt (verit, del_insts) imageI inv_sym_sym_var1 mem_Collect_eq sym_type_var1)

lemma sym_adj: 
  assumes "fFx i x"
  and "fFx (i + 1) y "
  shows "(σ i x = y) = (x = θ i y)"
  using assms local.inv_sym_sym local.sym_inv_sym by force

text ‹Next we list properties for inverse symmetries corresponding to the axioms.›

lemma inv_sym: 
  assumes "fFx i x"
  and "fFx (i + 1) x"
  shows "θ i x = x"
proof-
  have "x = σ i x"
    using assms local.sym_fix by simp
  thus ?thesis
    using assms sym_adj by force
qed

lemma inv_sym_face2:
  assumes "i ≠ j"
  and "i ≠ j + 1"
  and "fFx (j + 1) x"
  shows "∂ i α (θ j x) = θ j (∂ i α x)"
proof-
  have "σ j (∂ i α (θ j x)) = σ j (∂ i α (∂ j ff (θ j x)))"
    using assms(3) inv_sym_type_var by simp
  also have "… = ∂ i α (σ j (∂ j α (θ j x)))"
    by (metis assms inv_sym_type_var local.fFx_prop sym_face2_var1)
  also have "… = ∂ i α (σ j (θ j x))"
    using assms calculation inv_sym_type_var local.sym_face2 by presburger
  also have "… = ∂ i α (∂ (j + 1) α x)"
    by (metis assms(3) local.face_compat_var sym_inv_sym_var1)
  finally have "σ j (∂ i α (θ j x)) = ∂ i α (∂ (j + 1) α x)".
  thus ?thesis
    by (metis assms(3) inv_sym_type_var local.fFx_prop local.face_comm_var local.inv_sym_sym)
qed

lemma sym_braid: 
  assumes "fFx i x"
  and "fFx (i + 1) x"
  shows "σ i (σ (i + 1) (σ i x)) = σ (i + 1) (σ i (σ (i + 1) x))"
  using assms local.sym_face2 local.sym_fix sym_type_var by simp

lemma inv_sym_braid:
  assumes "fFx (i + 1) x"
  and "fFx (i + 2) x"
  shows "θ i (θ (i + 1) (θ i x)) = θ (i + 1) (θ i (θ (i + 1) x))"
  using assms inv_sym inv_sym_face2 inv_sym_type_var by simp

lemma sym_inv_sym_braid: 
  assumes "diffSup i j 2" 
  and "fFx (j + 1) x"
  and "fFx i x"
  shows "σ i (θ j x) = θ j (σ i x)"
  by (metis (no_types, lifting) ext assms(1,2,3) diff_add_0 diff_add_inverse inv_sym_face2
      inv_sym_type_var local.inv_sym_sym local.sym_face2 local.sym_inv_sym not_numeral_le_zero
      numeral_le_one_iff semiring_norm(69) sym_sym_braid_var1)

lemma sym_func1: 
  assumes "fFx i x"
  and "fFx i y"
  and "DD i x y"
  shows "σ i (x ⊗⇘i⇙ y) = σ i x ⊗⇘(i + 1)⇙ σ i y"
  by (metis assms icid.ts_compat local.iDst local.icat.sscatml.l0_absorb sym_type_var1)

lemma sym_func1_var1: "σσ i (∂ i α x ⊙⇘i⇙ ∂ i β y) = σ i (∂ i α x) ⊙⇘(i + 1)⇙ σ i (∂ i β y)"
  by (metis icid.t_idem image_empty image_insert inv_sym_sym_var1 local.face_compat_var local.icid.stopp.Dst sym_type_var1)

lemma inv_sym_func2_var1: "θθ i (∂ (i + 1) α x ⊙⇘i⇙ ∂ (i + 1) β y) = θ i (∂ (i + 1) α x) ⊙⇘(i + 1)⇙ θ i (∂ (i + 1) β y)"
proof-
  have "σσ i (θ i (∂ (i + 1) α x) ⊙⇘(i + 1)⇙ θ i (∂ (i + 1) β y)) = ∂ (i + 1) α x ⊙⇘i⇙ ∂ (i + 1) β y"
    by (metis func2_var2 inv_sym_type_var1 sym_inv_sym_var1)
  hence "σσ i (∂∂ i ff (θ i (∂ (i + 1) α x) ⊙⇘(i + 1)⇙ θ i (∂ (i + 1) β y))) = ∂∂ (i + 1) ff (∂ (i + 1) α x ⊙⇘i⇙ ∂ (i + 1) β y)"
    by (smt (verit) diff_add_0 diff_add_inverse inv_sym_type_var1 local.face_fix_comp_var
        local.icid.stopp.ts_compat numerals(1) zero_neq_numeral)
  hence "∂∂ i ff (θ i (∂ (i + 1) α x) ⊙⇘(i + 1)⇙ θ i (∂ (i + 1) β y)) = θθ i (∂∂ (i + 1) ff (∂ (i + 1) α x ⊙⇘i⇙ ∂ (i + 1) β y))"
    by (metis inv_sym_sym_lift_var)
  thus ?thesis
    by (metis add_cancel_right_right dual_order.eq_iff inv_sym_type_var1 local.face_compat_var local.face_fix_comp_var not_one_le_zero)
qed

lemma inv_sym_func3_var1: "θθ i ((∂ (i + 1) α x) ⊙⇘(i + 1)⇙ (∂ (i + 1) β y)) = θ i (∂ (i + 1) α x) ⊙⇘i⇙ θ i (∂ (i + 1) β y)"
  by (smt (z3) empty_is_image image_insert inv_sym_type_var1 local.face_idem1 local.face_pidem2 sym_inv_sym_var1)

lemma inv_sym_func_var1: 
  assumes "i ≠ j"
  and "j ≠ i + 1"
shows "θθ i ((∂ (i + 1) α x) ⊙⇘j⇙ (∂ (i + 1) β y)) = θ i (∂ (i + 1) α x) ⊙⇘j⇙ θ i (∂ (i + 1) β y)"
  by (smt (z3) assms(1) assms(2) inv_sym_sym_lift_var inv_sym_type_var1 local.face_fix_comp_var local.icid.stopp.ts_compat sym_func3_var2 sym_inv_sym_var1)

lemma inv_sym_func2:
  assumes "fFx (i + 1) x"
  and "fFx (i + 1) y"
  and "DD i x y"
  shows "θ i (x ⊗⇘i⇙ y) = θ i x ⊗⇘(i + 1)⇙ θ i y"
proof-
  have "{θ i (x ⊗⇘i⇙ y)} = θθ i (x ⊙⇘i⇙ y)"
    using assms(3) local.icat.pcomp_def_var4 by fastforce
  also have "… = θ i x ⊙⇘(i + 1)⇙ θ i y"
    by (metis assms(1) assms(2) inv_sym_func2_var1)
  also have "… = {θ i x ⊗⇘(i + 1)⇙ θ i y}"
    by (metis calculation insert_not_empty local.icat.pcomp_def_var4)
  finally show ?thesis
    by simp
qed

lemma inv_sym_func3: 
  assumes "fFx (i + 1) x"
  and "fFx (i + 1) y"
  and "DD (i + 1) x y"
  shows "θ i (x ⊗⇘(i + 1)⇙ y) = θ i x ⊗⇘i⇙ θ i y"
  by (metis assms icat.st_local icid.st_fix inv_sym_type_var1 local.icat.sscatml.l0_absorb)

lemma inv_sym_func: 
  assumes "i ≠ j"
  and "j ≠ i + 1"
  and "fFx (i + 1) x"
  and "fFx (i + 1) y"
  and "DD j x y"
  shows "θ i (x ⊗⇘j⇙ y) = θ i x ⊗⇘j⇙ θ i y"
proof-
  have "{θ i (x ⊗⇘j⇙ y)} = θθ i (x ⊙⇘j⇙ y)"
    using assms(5) local.icat.pcomp_def_var4 by fastforce
  also have "… = θ i x ⊙⇘j⇙ θ i y"
    by (metis assms(1) assms(2) assms(3) assms(4) inv_sym_func_var1)
  also have "… =  {θ i x ⊗⇘j⇙ θ i y}"
    by (metis calculation insert_not_empty local.icat.pcomp_def_var4)
  finally show ?thesis
    by simp
qed

text ‹The following properties are related to faces and braids.›

lemma sym_face3:
  assumes "fFx i x"
  shows "∂ (i + 1) α (σ i x) = σ i (∂ i α x)"
  by (metis assms local.fFx_prop sym_type_var1)

lemma sym_face3_var1: "∂ (i + 1) α (σ i (∂ i β x)) = σ i (∂ i α (∂ i β x))"
proof-
  have "∂ (i + 1) α (σ i (∂ i β x)) = ∂ (i + 1) α (σ i (∂ i α (∂ i β x)))"
    by simp
  also have "… = σ i (∂ i α (∂ i β x))"
    using local.sym_type_var1 by fastforce
  also have "… = σ i (∂ i β x)"
    by simp
  thus ?thesis
    using calculation by simp
qed

lemma sym_face3_simp [simp]: 
  assumes "fFx i x"
  shows "∂ (i + 1) α (σ i x) = σ i x"
  by (metis assms local.fFx_prop sym_face3)

lemma sym_face3_simp_var1 [simp]: "∂ (i + 1) α (σ i (∂ i β x)) = σ i (∂ i β x)"
  using sym_face3 by simp

lemma inv_sym_face3: 
  assumes "fFx (i + 1) x"
  shows "∂ i α (θ i x) = θ i (∂ (i + 1) α x)"
  by (metis assms inv_sym_type_var1 local.face_compat_var)

lemma inv_sym_face3_var1: "∂ i α (θ i (∂ (i + 1) β x)) = θ i (∂ (i + 1) α (∂ (i + 1) β x))"
  by (metis inv_sym_type_var1 local.face_compat_var)

lemma inv_sym_face3_simp: 
  assumes "fFx (i + 1) x"
  shows "∂ i α (θ i x) = θ i x"
  using assms inv_sym_type_var local.fFx_prop by force
 
lemma inv_sym_face3_simp_var1 [simp]: "∂ i α (θ i (∂ (i + 1) β x)) = θ i (∂ (i + 1) β x)"
  using inv_sym_face3 local.face_compat_var by simp

lemma inv_sym_face1: 
  assumes "fFx (i + 1) x"
  shows "∂ (i + 1) α (θ i x) = θ i (∂ i α x)"
  by (metis assms inv_sym_face3_simp inv_sym_sym_var1 local.face_comm_var local.sym_inv_sym sym_face1_var1)

lemma inv_sym_face1_var1: "∂ (i + 1) α (θ i (∂ (i + 1) β x)) = θ i (∂ i α (∂ (i + 1) β x))"
  using inv_sym_face1 local.face_compat_var by simp

lemma inv_sym_sym_braid: 
  assumes "diffSup i j 2"
  and "fFx j x"
  and "fFx (i + 1) x"
  shows "θ i (σ j x) = σ j (θ i x)"
  using assms sym_inv_sym_braid by force

lemma inv_sym_sym_braid_var1: "diffSup i j 2 ⟹ θ i (σ j (∂ (i + 1) α (∂ j β x))) = σ j (θ i (∂ (i + 1) α (∂ j β x)))"
  using local.face_comm_var local.sym_inv_sym_braid by force

lemma inv_sym_inv_sym_braid: 
  assumes "diffSup i j 2"
  and "fFx (i + 1) x"
  and "fFx (j + 1) x"
  shows "θ i (θ j x) = θ j (θ i x)"
  by (metis Suc_eq_plus1 add_right_cancel assms inv_sym_face2 inv_sym_face3 inv_sym_sym_braid_var1 local.inv_sym_sym local.sym_inv_sym nat_le_linear not_less_eq_eq)

lemma inv_sym_inv_sym_braid_var1: "diffSup i j 2 ⟹ θ i (θ j (∂ (i + 1) α (∂ (j + 1) β x))) = θ j (θ i (∂ (i + 1) α (∂ (j + 1) β x)))"
  using inv_sym_inv_sym_braid local.face_comm_var by force


text ‹The following properties are related to symcomp and inv-symcomp.›

lemma symcomp_type_var: 
  assumes "fFx i x"
  shows "fFx (i + j) (Σ i j x)" using ‹fFx i x›
  apply (induct j)
  using sym_face3 by simp_all

lemma symcomp_type: "image (Σ i j) (face_fix i) ⊆ face_fix (i + j)"
  using symcomp_type_var by force

lemma symcomp_type_var1 [simp]: "∂ (i + j) α (Σ i j (∂ i β x)) = Σ i j (∂ i β x)"
  by (metis local.face_compat_var symcomp_type_var)

lemma inv_symcomp_type_var: 
  assumes "fFx (i + j) x"
  shows "fFx i (Θ i j x)" using ‹fFx (i + j) x›
  by (induct j arbitrary: x, simp_all add: inv_sym_type_var)

lemma inv_symcomp_type: "image (Θ i j) (face_fix (i + j)) ⊆ face_fix i"
  using inv_symcomp_type_var by force

lemma inv_symcomp_type_var1 [simp]: "∂ i α (Θ i j (∂ (i + j) β x)) = Θ i j (∂ (i + j) β x)"
  by (meson inv_symcomp_type_var local.fFx_prop local.face_compat_var)

lemma symcomp_inv_symcomp: 
  assumes "fFx (i + j) x"
  shows "Σ i j (Θ i j x) = x" using ‹fFx (i + j) x›
  by (induct j arbitrary: i x, simp_all add: inv_sym_type_var local.sym_inv_sym)

lemma inv_symcomp_symcomp: 
  assumes "fFx i x"
  shows "Θ i j (Σ i j x) = x" using ‹fFx i x›
  by (induct j arbitrary: i x, simp_all add: local.inv_sym_sym symcomp_type_var)

lemma symcomp_adj: 
  assumes "fFx i x"
  and "fFx (i + j) y "
  shows "(Σ i j x = y) = (x = Θ i j y)"
  using assms inv_symcomp_symcomp symcomp_inv_symcomp by force

lemma decomp_symcomp1: 
  assumes "k ≤ j" 
  and "fFx i x"
  shows " Σ i j x = Σ (i + k) (j - k) (Σ i k x)" using ‹k ≤ j›
  apply (induct j)
  using Suc_diff_le le_Suc_eq by force+

lemma decomp_symcomp2:
  assumes "1 ≤ k"
  and "k ≤ j"
  and "fFx i x"
  shows "Σ i j x = Σ (i + k) (j - k) (σ (i + k - 1) (Σ i (k - 1) x))"
  by (metis Nat.add_diff_assoc add_diff_cancel_left' assms decomp_symcomp1 local.symcomp.simps(2) plus_1_eq_Suc)

lemma decomp_symcomp3:
  assumes "i ≤ l"
  and "l + 1 ≤ i + j"
  and "fFx i x"
  shows "Σ i j x = Σ (l + 1) (i + j - l - 1) (σ l (Σ i (l - i) x))"
  by (smt (verit, del_insts) add.commute add_le_cancel_left assms decomp_symcomp2 diff_add_inverse2 diff_diff_left le_add1 le_add_diff_inverse)

lemma symcomp_face2: 
  assumes "l < i ∨ i + j < l"
  and  "fFx i x" 
  shows "∂ l α (Σ i j x) = Σ i j (∂ l α x)" using ‹l < i ∨ i + j < l›
proof (induct j)
  case 0
  show ?case 
    by simp
next
  case (Suc j)
  have "∂ l α (Σ i (Suc j) x) = ∂ l α (σ (i + j) (Σ i j x))"
    by simp
  also have "… = σ (i + j) (∂ l α (Σ i j x))"
    using Suc.prems add.commute assms(2) local.sym_face2 symcomp_type_var by auto
  also have "… = σ (i + j) (Σ i j (∂ l α x))"
    using Suc.hyps Suc.prems by fastforce
  also have "… = (Σ i (Suc j) (∂ l α x))"
    by simp
  finally show ?case.
qed

lemma symcomp_face3: "fFx i x ⟹ ∂ (i + j) α (Σ i j x) = Σ i j (∂ i α x)"
  by (metis local.face_compat_var symcomp_type_var1)

lemma symcomp_face1:
  assumes "i ≤ l"
  and "l < i + j"
  and "fFx i x"
  shows "∂ l α (Σ i j x) = Σ i j (∂ (l + 1) α x)"
proof-
  have "∂ l α (Σ i j x) = ∂ l α (Σ (l + 1) (i + j - l - 1) (σ l (Σ i (l - i) x)))"
    using Suc_eq_plus1 Suc_leI assms(1) assms(2) assms(3) decomp_symcomp3 by presburger
  also have "… = Σ (l + 1) (i + j - l - 1) (∂ l α (σ l (Σ i (l - i) x)))"
    by (metis assms(1) assms(3) less_add_one ordered_cancel_comm_monoid_diff_class.add_diff_inverse sym_type_var symcomp_face2 symcomp_face3)
  also have "… = Σ (l + 1) (i + j - l - 1) (σ l (∂ (l + 1) α (Σ i (l - i) x)))"
    by (metis assms(1) assms(3) local.sym_face1 ordered_cancel_comm_monoid_diff_class.add_diff_inverse symcomp_face3)
  also have "… = Σ (l + 1) (i + j - l - 1) (σ l (Σ i (l - i) (∂ (l + 1) α x)))"
    by (simp add: assms(1) assms(3) symcomp_face2)
  also have "… = Σ i j (∂ (l + 1) α x)"
    by (metis Suc_eq_plus1 Suc_leI assms(1) assms(2) assms(3) decomp_symcomp3 local.fFx_prop local.face_comm_var)
  finally show ?thesis.
qed

lemma inv_symcomp_face2: 
  assumes "l < i ∨ i + j < l"
  and "fFx (i + j) x"
  shows "∂ l α (Θ i j x) = Θ i j (∂ l α x)" using ‹l < i ∨ i + j < l› ‹fFx (i + j) x›
proof (induct j arbitrary: x)
  case 0
  show ?case
    using local.inv_sym_face2 by force
next
  case (Suc j)
  have "∂ l α (Θ i (Suc j) x) = Θ i j (∂ l α (θ (i + j) x))"
    using Suc.hyps Suc.prems(1) Suc.prems(2) inv_sym_type_var by force
  also have "… = Θ i j (θ (i + j) (∂ l α x))"
    using Suc.prems inv_sym_face2 by force
  also have "… = (Θ i (Suc j) (∂ l α x))"
    by simp
  finally show ?case.
qed

lemma inv_symcomp_face3: "fFx (i + j) x ⟹ ∂ i α (Θ i j x) = Θ i j (∂ (i + j) α x)"
  by (metis inv_symcomp_type_var1 local.face_compat_var)

lemma inv_symcomp_face1:
  assumes "i < l"
  and "l ≤ i + j"
  and "fFx (i + j) x"
  shows "∂ l α (Θ i j x) = Θ i j (∂ (l - 1) α x)"
proof-
  have "(∂ (l - 1) α (Σ i j (Θ i j x)) = ∂ (l - 1) α x)"
    using assms(3) symcomp_inv_symcomp by force
  hence "(Σ i j (∂ l α (Θ i j x)) = ∂ (l - 1) α x)"
    using assms inv_symcomp_type_var symcomp_face1 by auto
  thus ?thesis
    by (metis assms(1) assms(3) inv_symcomp_symcomp inv_symcomp_type_var local.face_comm_var nat_neq_iff)
qed

lemma symcomp_comp1: 
  assumes "fFx i x"
  and "fFx i y"
  and "DD i x y"
  shows "Σ i j (x ⊗⇘i⇙ y) = Σ i j x ⊗⇘(i + j)⇙ Σ i j y"
  by (induct j, simp, metis assms local.face_compat_var local.iDst local.icat.sscatml.r0_absorb symcomp_type_var1)

lemma symcomp_comp2: 
  assumes "k < i"
  and "fFx i x"
  and "fFx i y"
  and "DD k x y"
  shows "Σ i j (x ⊗⇘k⇙ y) = Σ i j x ⊗⇘k⇙ Σ i j y"
proof (induct j)
  case 0
  show ?case
    by simp
next
  case (Suc j)
  have "Σ i (Suc j) (x⊗⇘k⇙y) = σ (i + j) ((Σ i j x) ⊗⇘k⇙ (Σ i j y))"
    by (simp add: Suc)
  also have "… = σ (i + j) (Σ i j x) ⊗⇘k⇙ σ (i + j) (Σ i j y)"
    apply (rule sym_func3)
    using assms(1) assms(2) assms(3) symcomp_type_var apply presburger+
    using assms local.iDst local.locality symcomp_face2 by presburger
  finally show ?case
    by simp
qed

lemma symcomp_comp3: 
  assumes "i + j < k"
  and "fFx i x"
  and "fFx i y"
  and "DD k x y"
  shows "Σ i j (x ⊗⇘k⇙ y) = Σ i j x ⊗⇘k⇙ Σ i j y" using ‹k > i + j›
proof (induct j)
  case 0
  show ?case
    by simp
next
  case (Suc j)
  have "Σ i (Suc j) (x⊗⇘k⇙y) = σ (i + j) ((Σ i j x) ⊗⇘k⇙ (Σ i j y))"
    using Suc.hyps Suc.prems by force
  also have "… = σ (i + j) (Σ i j x) ⊗⇘k⇙ σ (i + j) (Σ i j y)"
    apply (rule sym_func3)
    using Suc.prems apply linarith+
    using assms(2) assms(3) symcomp_type_var apply presburger+
    using Suc.prems assms(2) assms(3) assms(4) local.icid.ts_msg.st_locality_locality symcomp_face2 by simp
  finally show ?case
    by simp
qed

lemma fix_comp:
  assumes "i ≠ j"
  and "fFx i x"
  and "fFx i y"
  and "DD j x y"
  shows "fFx i (x ⊗⇘j⇙ y)"
  using face_func assms by simp

lemma symcomp_comp4: 
  assumes "i < k"
  and "k ≤ i + j"
  and "fFx i x"
  and "fFx i y"
  and "DD k x y"
  shows "Σ i j (x ⊗⇘k⇙ y) = Σ i j x ⊗⇘(k - 1)⇙ Σ i j y" 
  using ‹k ≤ i + j› ‹fFx i x› ‹fFx i y› ‹DD k x y›
proof (induct j arbitrary: x y)
  case 0
  thus ?case
    using assms(1) by linarith
next
  case (Suc j)
  have a: "fFx i (x ⊗⇘k⇙ y)"
    using Suc.prems(2) Suc.prems(3) Suc.prems(4) assms(1) fix_comp by force
  have b: "fFx (k - 1) (Σ i (k - 1 - i) x)"
    using Suc.prems(2) assms(1) less_imp_Suc_add symcomp_type_var by fastforce
  have c: "fFx (k - 1) (Σ i (k - 1 - i) y)"
    using Suc.prems(3) assms(1) less_imp_Suc_add symcomp_type_var by fastforce
  have d: "DD k (Σ i (k - 1 - i) x) (Σ i (k - 1 - i) y)"
    by (metis Suc.prems(2) Suc.prems(3) Suc.prems(4) add_diff_cancel_left' assms(1) lessI less_imp_Suc_add local.iDst local.locality plus_1_eq_Suc symcomp_face2)
  have "Σ i (Suc j) (x ⊗⇘k⇙ y) = Σ k (i + j + 1 - k) (σ (k - 1) (Σ i (k - 1 - i) (x ⊗⇘k⇙ y)))"
    by (smt (verit) Suc.prems(1) Suc_eq_plus1 a add_Suc_right add_le_imp_le_diff assms(1) decomp_symcomp3 diff_diff_left le_add_diff_inverse2 less_eq_Suc_le plus_1_eq_Suc)
  also have "… = Σ k (i + j + 1 - k) (σ (k - 1) (Σ i (k - 1 - i) x ⊗⇘k⇙ Σ i (k - 1 - i) y))"
    using Suc.prems(2) Suc.prems(3) Suc.prems(4) assms(1) symcomp_comp3 by force
  also have "… = Σ k (i + j + 1 - k) (σ (k - 1) (Σ i (k - 1 - i) x ⊗⇘((k - 1) + 1)⇙ Σ i (k - 1 - i) y))"
    using assms(1) by auto
  also have "… = Σ k (i + j + 1 - k) (σ (k - 1) (Σ i (k - 1 - i) x) ⊗⇘(k - 1)⇙ σ (k - 1) (Σ i (k - 1 - i) y))"
    using assms(1) b c d less_iff_Suc_add sym_func2 by fastforce
  also have "… = Σ k (i + j + 1 - k) (σ (k - 1) (Σ i (k - 1 - i) x)) ⊗⇘(k - 1)⇙ Σ k (i + j + 1 - k) (σ (k - 1) (Σ i (k - 1 - i) y))"
    apply (rule symcomp_comp2)
    using assms(1) b sym_face3 apply fastforce+
    apply (metis assms(1) c le_add1 le_add_diff_inverse2 less_imp_Suc_add plus_1_eq_Suc sym_face3)
    by (metis assms(1) b c d le_add1 le_add_diff_inverse2 less_imp_Suc_add plus_1_eq_Suc sym_func2_DD)
  also have "… = Σ k (i + j + 1 - k) (Σ i (k - i) x) ⊗⇘(k - 1)⇙ Σ k (i + j + 1 - k) (Σ i (k - i) y)"
    using assms(1) less_imp_Suc_add by fastforce
  also have "… = (Σ i (j + 1) x) ⊗⇘(k - 1)⇙ Σ k (i + j + 1 - k) (Σ i (k - i) y)"
    by (smt (verit, ccfv_SIG) Nat.diff_diff_eq Suc.prems(1) Suc.prems(2) add.comm_neutral add_left_mono assms(1) decomp_symcomp1 diff_add_inverse diff_le_mono group_cancel.add2 linordered_semidom_class.add_diff_inverse order_less_imp_le order_less_imp_not_less plus_1_eq_Suc zero_less_Suc)
  also have "… = (Σ i (j + 1) x) ⊗⇘(k - 1)⇙ (Σ i (j + 1) y)"
    by (smt (verit, ccfv_SIG) Nat.add_0_right Nat.diff_diff_eq Suc.prems(1) Suc.prems(3) add_Suc add_Suc_shift add_diff_inverse_nat add_mono_thms_linordered_semiring(2) assms(1) decomp_symcomp1 diff_add_inverse diff_le_mono nless_le order.asym plus_1_eq_Suc trans_less_add2 zero_less_one)
  finally show ?case
    by simp
qed

lemma symcomp_comp: 
  assumes "fFx i x"
  and "fFx i y"
  and "DD k x y"
  shows "Σ i j (x ⊗⇘k⇙ y) = (if k = i then Σ i j x ⊗⇘(i + j)⇙ Σ i j y
                                else (if (i < k ∧ k ≤ i + j) then Σ i j x ⊗⇘(k - 1)⇙ Σ i j y
                                  else Σ i j x ⊗⇘k⇙ Σ i j y))"
  by (metis assms linorder_not_le not_less_iff_gr_or_eq symcomp_comp1 symcomp_comp2 symcomp_comp3 symcomp_comp4)

lemma inv_symcomp_comp1: 
  assumes "fFx (i + j) x"
  and "fFx (i + j) y"
  and "DD (i + j) x y"
  shows "Θ i j (x ⊗⇘(i + j)⇙ y) = Θ i j x ⊗⇘i⇙ Θ i j y"
  by (metis assms inv_symcomp_type_var local.fFx_prop local.iDst local.icat.sscatml.l0_absorb)

lemma inv_symcomp_comp2:
  assumes "k < i"
  and "fFx (i + j) x"
  and "fFx (i + j) y"
  and "DD k x y"
  shows "Θ i j (x ⊗⇘k⇙ y) = Θ i j x ⊗⇘k⇙ Θ i j y"
proof-
  have a: "DD k (Θ i j x) (Θ i j y)"
    using assms inv_symcomp_face2 local.iDst local.locality by presburger
  have "x ⊗⇘k⇙ y = Σ i j (Θ i j x) ⊗⇘k⇙ Σ i j (Θ i j y)"
    by (simp add: assms(2) assms(3) symcomp_inv_symcomp)
  hence "x ⊗⇘k⇙ y = Σ i j ((Θ i j x) ⊗⇘k⇙ (Θ i j y))"
    using a assms(1) assms(2) assms(3) inv_symcomp_type_var symcomp_comp2 by presburger
  thus ?thesis
    using a assms(1) assms(2) assms(3) fix_comp inv_symcomp_face3 inv_symcomp_symcomp by simp
qed

lemma inv_symcomp_comp3:
  assumes "i + j < k"
  and "fFx (i + j) x"
  and "fFx (i + j) y"
  and "DD k x y"
  shows "Θ i j (x ⊗⇘k⇙ y) = Θ i j x ⊗⇘k⇙ Θ i j y"
proof-
  have h: "DD k (Θ i j x) (Θ i j y)"
    using assms inv_symcomp_face2 local.iDst local.locality by presburger
  have "x ⊗⇘k⇙ y = Σ i j (Θ i j x) ⊗⇘k⇙ Σ i j (Θ i j y)"
    by (simp add: assms(2) assms(3) symcomp_inv_symcomp)
  hence "x ⊗⇘k⇙ y = Σ i j ((Θ i j x) ⊗⇘k⇙ (Θ i j y))"
    using assms(1) assms(2) assms(3) h inv_symcomp_face3 symcomp_comp3 by simp
  thus ?thesis
    using assms(1) assms(2) assms(3) fix_comp h inv_symcomp_face3 inv_symcomp_symcomp by simp
qed

lemma inv_symcomp_comp4:
  assumes "i ≤ k"
  and "k < i + j"
  and "fFx (i + j) x"
  and "fFx (i + j) y"
  and "DD k x y"
  shows "Θ i j (x ⊗⇘k⇙ y) = Θ i j x ⊗⇘(k + 1)⇙ Θ i j y"
proof-
  have h: "DD (k + 1) (Θ i j x) (Θ i j y)"
    using assms(1) assms(2) assms(3) assms(4) assms(5) inv_symcomp_face1 local.icat.sts_msg.st_local by auto
  have "x ⊗⇘k⇙ y = Σ i j (Θ i j x) ⊗⇘k⇙ Σ i j (Θ i j y)"
    by (simp add: assms(3) assms(4) symcomp_inv_symcomp)
  hence "x ⊗⇘k⇙ y = Σ i j ((Θ i j x) ⊗⇘(k + 1)⇙ (Θ i j y))"
   apply (subst symcomp_comp4)
    using assms h inv_symcomp_type_var by auto
  thus ?thesis
    by (metis Suc_eq_plus1 Suc_n_not_le_n assms(1) assms(3) assms(4) fix_comp h inv_symcomp_face3 inv_symcomp_symcomp)
qed

end

end