Theory CubicalCategoriesConnections

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

section‹Cubical Categories with Connections›

theory CubicalCategoriesConnections
  imports CubicalCategories

begin

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

class connection_ops = 
  fixes connection :: "nat ⇒ bool ⇒ 'a ⇒ 'a" ("Γ")

abbreviation (in connection_ops) "ΓΓ i α ≡ image (Γ i α)"

text ‹We define a class for cubical $\omega$-categories with connections.›

class cubical_omega_category_connections = cubical_omega_category + connection_ops +
  assumes conn_face1: "fFx j x ⟹ ∂ j α (Γ j α x) = x"
  and conn_face2: "fFx j x ⟹ ∂ (j + 1) α (Γ j α x) = σ j x"
  and conn_face3: "i ≠ j ⟹ i ≠ j + 1 ⟹ fFx j x ⟹ ∂ i α (Γ j β x) = Γ j β (∂ i α x)"
  and conn_corner1: "fFx i x ⟹ fFx i y ⟹ DD (i + 1) x y ⟹ Γ i tt (x ⊗⇘(i + 1)⇙ y) = (Γ i tt x ⊗⇘(i + 1)⇙ σ i x) ⊗⇘i⇙ (x ⊗⇘(i + 1)⇙ Γ i tt y)" 
  and conn_corner2: "fFx i x ⟹ fFx i y ⟹ DD (i + 1) x y ⟹ Γ i ff (x ⊗⇘(i + 1)⇙ y) = (Γ i ff x ⊗⇘(i + 1)⇙ y) ⊗⇘i⇙ (σ i y ⊗⇘(i + 1)⇙ Γ i ff y)"
  and conn_corner3: "j ≠ i ∧ j ≠ i + 1 ⟹ fFx i x ⟹ fFx i y ⟹ DD j x y ⟹ Γ i α (x ⊗⇘j⇙ y) = Γ i α x ⊗⇘j⇙ Γ i α y"
  and conn_fix: "fFx i x ⟹ fFx (i + 1) x ⟹ Γ i α x = x"
  and conn_zigzag1: "fFx i x ⟹ Γ i tt x ⊗⇘(i + 1)⇙ Γ i ff x = x"
  and conn_zigzag2: "fFx i x ⟹ Γ i tt x ⊗⇘i⇙ Γ i ff x = σ i x"
  and conn_conn_braid: "diffSup i j 2 ⟹ fFx j x ⟹ fFx i x ⟹ Γ i α (Γ j β x) = Γ j β (Γ i α x)"
  and conn_shift: "fFx i x ⟹ fFx (i + 1) x ⟹ σ (i + 1) (σ i (Γ (i + 1) α x)) = Γ i α (σ (i + 1) x)"

begin 

lemma conn_face4: "fFx j x ⟹ ∂ j α (Γ j (¬α) x) = ∂ (j + 1) α x"
  by (smt (z3) local.conn_face1 local.conn_zigzag2 local.face_comm_var local.locality local.pcomp_lface local.pcomp_uface local.sym_face1 local.sym_fix_var1)

lemma conn_face1_lift: "FFx j X ⟹ ∂∂ j α (ΓΓ j α X) = X"
  by (auto simp add: image_iff local.conn_face1)

lemma conn_face4_lift: "FFx j X ⟹ ∂∂ j α (ΓΓ j (¬α) X) = ∂∂ (j + 1) α X"
  apply safe
  apply (simp add: local.conn_face4)
  by (metis image_eqI local.conn_face4)

lemma conn_face2_lift: "FFx j X ⟹ ∂∂ (j + 1) α (ΓΓ j α X) = σσ j X"
  by (smt (z3) comp_apply image_comp image_cong local.conn_face2)

lemma conn_face3_lift: "i ≠ j ⟹ i ≠ j + 1 ⟹ FFx j X ⟹ ∂∂ i α (ΓΓ j β X) = ΓΓ j β (∂∂ i α X)"
  by (smt (z3) image_cong image_image local.conn_face3)

lemma conn_fix_lift: "FFx i X ⟹ FFx (i + 1) X ⟹ ΓΓ i α X = X"
  by (simp add: local.conn_fix)

lemma conn_conn_braid_lift: 
  assumes "diffSup i j 2" 
  and "FFx j X" 
  and "FFx i X"
  shows "ΓΓ i α (ΓΓ j β X) = ΓΓ j β (ΓΓ i α X)"
  by (smt (z3) assms image_cong image_image local.conn_conn_braid)

lemma conn_sym_braid: 
  assumes "diffSup i j 2"
  and "fFx i x"
  and "fFx j x"
  shows "Γ i α (σ j x) = σ j (Γ i α x)"
  by (smt (z3) assms add_diff_cancel_left' cancel_comm_monoid_add_class.diff_cancel diff_is_0_eq' icat.st_local le_add1 local.conn_conn_braid local.conn_corner3 local.conn_face1 local.conn_face3 local.conn_zigzag2 numeral_le_one_iff rel_simps(28) semiring_norm(69))

lemma conn_zigzag1_var [simp]: "Γ i tt (∂ i α x) ⊙⇘(i + 1)⇙ Γ i ff (∂ i α x) = {∂ i α x}"
proof (cases "DD (i + 1) (Γ i tt (∂ i α x)) (Γ i ff (∂ i α x))")
  case True
  hence "Γ i tt (∂ i α x) ⊙⇘(i + 1)⇙ Γ i ff (∂ i α x) = {Γ i tt (∂ i α x) ⊗⇘(i + 1)⇙ Γ i ff (∂ i α x)}"
    by (metis True local.icat.pcomp_def_var4)
  also have "… = {∂ i α x}"
    using local.conn_zigzag1 by simp
  finally show ?thesis.
next
  case False
  thus ?thesis
    using local.conn_face2 local.locality by simp 
qed

lemma conn_zigzag1_lift:
  assumes "FFx i X"
  shows "ΓΓ i tt X ⋆⇘(i + 1)⇙ ΓΓ i ff X = X"
proof-
  have "ΓΓ i tt X ⋆⇘(i + 1)⇙ ΓΓ i ff X = {Γ i tt x ⊗⇘(i + 1)⇙ Γ i ff y | x y. x ∈ X ∧ y ∈ X ∧ DD (i + 1) (Γ i tt x) (Γ i ff y)}"
    unfolding local.iconv_prop by force
  also have "… = {Γ i tt x ⊗⇘(i + 1)⇙ Γ i ff y | x y. x ∈ X ∧ y ∈ X ∧ ∂ (i + 1) tt (Γ i tt x) = ∂ (i + 1) ff (Γ i ff y)}"
    using icat.st_local by presburger
  also have "… = {Γ i tt x ⊗⇘(i + 1)⇙ Γ i ff y | x y. x ∈ X ∧ y ∈ X ∧ σ i x = σ i y}"
    by (metis (no_types, lifting) assms local.conn_face2)
  also have "… = {Γ i tt x ⊗⇘(i + 1)⇙ Γ i ff x | x. x ∈ X}"
    using assms local.sym_inj_var by blast
  also have "… = {Γ i tt (∂ i tt x) ⊗⇘(i + 1)⇙ Γ i ff (∂ i tt x) | x. x ∈ X}"
    by (metis (full_types) assms icid.ts_compat)
  also have "… = {∂ i tt x | x. x ∈ X}"
    using local.conn_zigzag1 local.face_compat_var by presburger
  also have "… = X"
    by (smt (verit, del_insts) Collect_cong Collect_mem_eq assms local.icid.stopp.st_fix)
  finally show ?thesis.
qed

lemma conn_zigzag2_var: "Γ i tt (∂ i α x) ⊙⇘i⇙ Γ i ff (∂ i α x) = {σ i (∂ i α x)}"
proof (cases "DD i (Γ i tt (∂ i α x)) (Γ i ff (∂ i α x))")
  case True
  hence "Γ i tt (∂ i α x) ⊙⇘i⇙ Γ i ff (∂ i α x) = {Γ i tt (∂ i α x) ⊗⇘i⇙ Γ i ff (∂ i α x)}"
    by (metis True local.icat.pcomp_def_var4)
  also have "… = {σ i (∂ i α x)}"
    using local.conn_zigzag2 by simp
  finally show ?thesis.
next
  case False
  thus ?thesis
    by (simp add: local.conn_face1 local.locality)
qed

lemma conn_zigzag2_lift:
  assumes "FFx i X"
  shows "ΓΓ i tt X ⋆⇘i⇙ ΓΓ i ff X = σσ i X"
proof-
  have "ΓΓ i tt X ⋆⇘i⇙ ΓΓ i ff X = {Γ i tt x ⊗⇘i⇙ Γ i ff y | x y. x ∈ X ∧ y ∈ X ∧ DD i (Γ i tt x) (Γ i ff y)}"
    unfolding local.iconv_prop by force
  also have "… = {Γ i tt x ⊗⇘i⇙ Γ i ff y | x y. x ∈ X ∧ y ∈ X ∧ ∂ i tt (Γ i tt x) = ∂ i ff (Γ i ff y)}"
    using icat.st_local by presburger
  also have "… = {Γ i tt x ⊗⇘i⇙ Γ i ff x | x. x ∈ X}"
    by (metis (full_types) assms local.conn_face1)
  also have "… = {Γ i tt (∂ i tt x) ⊗⇘i⇙ Γ i ff (∂ i tt x) | x. x ∈ X}"
    by (metis (full_types) assms icid.ts_compat)
  also have "… = {σ i x | x. x ∈ X}"
    by (metis assms icid.ts_compat local.conn_zigzag2)
  also have "… = σσ i X"
    by force
  finally show ?thesis.
qed

lemma conn_sym_braid_lift: "diffSup i j 2 ⟹ FFx i X ⟹ FFx j X ⟹ ΓΓ i α (σσ j X) = σσ j (ΓΓ i α X)"
  by (smt (z3) image_cong image_image local.conn_sym_braid)

lemma conn_corner1_DD:
  assumes "fFx i x"
  and "fFx i y"
  and "DD (i + 1) x y"
  shows "DD i (Γ i tt x ⊗⇘(i + 1)⇙ σ i x) (x ⊗⇘(i + 1)⇙ Γ i tt y)"
proof-
  have h1: "DD (i + 1) (Γ i tt x) (σ i x)"
    using assms(1) local.conn_face2 local.locality local.sym_type_var by simp
  have h2: "DD (i + 1) x (Γ i tt y)"
    by (metis assms(2) assms(3) conn_zigzag1_var icat.st_local icid.src_comp_aux singleton_iff)
  have h3: "∂ i tt (Γ i tt x ⊗⇘(i + 1)⇙ σ i x) = x"
    by (metis assms(1) local.conn_face1 local.conn_face2 local.icat.sscatml.r0_absorb)
  have "∂ i ff (x ⊗⇘(i + 1)⇙ Γ i tt y) = ∂ i ff x ⊗⇘(i + 1)⇙ ∂ i ff (Γ i tt y)"
    using h2 local.face_func by simp
  hence h4: "∂ i ff (x ⊗⇘(i + 1)⇙ Γ i tt y) = x ⊗⇘(i + 1)⇙ ∂ (i + 1) ff y"
    by (metis (full_types) assms(1) assms(2) local.conn_face4)
  have "∂ i tt (Γ i tt x ⊗⇘(i + 1)⇙ σ i x) = ∂ i tt (Γ i tt x) ⊗⇘(i + 1)⇙ ∂ i tt (σ i x)"
    using h1 local.face_func by simp
  also have "… = x ⊗⇘(i + 1)⇙ ∂ (i + 1) tt x"
    using calculation h3 by simp
  thus ?thesis
    using assms(3) h3 h4 local.icat.sts_msg.st_local by simp
qed

lemma conn_corner1_var: "ΓΓ i tt (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = (Γ i tt (∂ i α x) ⊙⇘(i + 1)⇙ σ i (∂ i α x)) ⋆⇘i⇙ (∂ i α x ⊙⇘(i + 1)⇙ Γ i tt (∂ i β y))"
proof (cases "DD (i + 1) (∂ i α x) (∂ i β y)")
  case True
  have h1: "DD (i + 1) (Γ i tt (∂ i α x)) (σ i (∂ i α x))"
    by (metis local.conn_face2 local.face_compat_var local.locality)
  have h2: "DD (i + 1) (∂ i α x) (Γ i tt (∂ i β y))"
    by (metis True icid.src_comp_aux insertCI local.conn_zigzag1_var local.iDst local.locality)
  have h3: "DD i (Γ i tt (∂ i α x) ⊗⇘(i + 1)⇙ σ i (∂ i α x)) (∂ i α x ⊗⇘(i + 1)⇙ Γ i tt (∂ i β y))"
    using True local.conn_corner1_DD local.face_compat_var by simp
  have "ΓΓ i tt (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = ΓΓ i tt {∂ i α x ⊗⇘(i + 1)⇙ ∂ i β y}"
    using True local.icat.pcomp_def_var4 by simp
  also have "… = {(Γ i tt (∂ i α x) ⊗⇘(i + 1)⇙ σ i (∂ i α x)) ⊗⇘i⇙ (∂ i α x ⊗⇘(i + 1)⇙ Γ i tt (∂ i β y))}"
    using True local.conn_corner1 local.face_compat_var by simp
  also have "… = {Γ i tt (∂ i α x) ⊗⇘(i + 1)⇙ σ i (∂ i α x)} ⋆⇘i⇙ {∂ i α x ⊗⇘(i + 1)⇙ Γ i tt (∂ i β y)}"
    using h3 local.icat.pcomp_def_var4 local.icid.stopp.conv_atom by simp
  also have "… = (Γ i tt (∂ i α x) ⊙⇘(i + 1)⇙ σ i (∂ i α x)) ⋆⇘i⇙ (∂ i α x ⊙⇘(i + 1)⇙ Γ i tt (∂ i β y))"
    using h1 h2 local.icat.pcomp_def_var4 by simp
  finally show ?thesis.
next
  case False
  thus ?thesis
    by (smt (z3) Union_empty empty_is_image icat.st_local icid.ts_compat local.conn_face4 local.face_comm_var local.icid.stopp.ts_compat multimagma.conv_distl)
qed

lemma conn_corner1_lift_aux: "fFx i x ⟹ ∂ (i + 1) ff (Γ i tt x) = ∂ (i + 1) ff x"
  by (metis conn_zigzag1_var empty_not_insert equals0I icid.src_comp_aux singletonD)

lemma conn_corner1_lift:
  assumes "FFx i X"
  and "FFx i Y"
  shows "ΓΓ i tt (X ⋆⇘(i + 1)⇙ Y) = (ΓΓ i tt X ⋆⇘(i + 1)⇙ σσ i X) ⋆⇘i⇙ (X ⋆⇘(i + 1)⇙ ΓΓ i tt Y)"
proof-
  have h1: "∀y ∈ Y. ∂ (i + 1) ff (Γ i tt y) = ∂ (i + 1) ff y"
    by (metis assms(2) conn_zigzag1_var local.icid.ts_msg.tgt_comp_aux singletonI)
  have h2 :"∀xa ∈ X. DD (i + 1) (Γ i tt xa) (σ i xa) ⟶ ∂ i tt (Γ i tt xa ⊗⇘(i + 1)⇙ σ i xa) = ∂ i tt (Γ i tt xa) ⊗⇘(i + 1)⇙ ∂ i tt (σ i xa)"
    by (simp add: local.face_func)
  have h3 :"∀xc ∈ X. ∀y ∈ Y. DD (i + 1) xc (Γ i tt y) ⟶ ∂ i ff (xc ⊗⇘(i + 1)⇙ Γ i tt y) = ∂ i ff xc ⊗⇘(i + 1)⇙ ∂ i ff (Γ i tt y)"
    by (simp add: local.face_func)
  have h4: "∀xa ∈ X. ∂ i tt (Γ i tt xa) ⊗⇘(i + 1)⇙ ∂ i tt (σ i xa) = xa ⊗⇘(i + 1)⇙ ∂ i tt (∂ (i + 1) tt xa)"
    by (smt (z3) assms(1) local.conn_face1 local.fFx_prop local.face_comm_var local.sym_face1_var1 local.sym_fix_var1)
  have h5: "∀xc ∈ X. ∀y ∈ Y. ∂ i ff xc ⊗⇘(i + 1)⇙ ∂ i ff (Γ i tt y) = xc ⊗⇘(i + 1)⇙ ∂ (i + 1) ff y"
    by (metis (full_types) assms(1) assms(2) local.conn_face4)
  have h6: "∀xc ∈ X. ∀y ∈ Y. DD (i + 1) xc (∂ (i + 1) ff y) ⟶ xc ⊗⇘(i + 1)⇙ ∂ (i + 1) ff y = xc"
    by (metis local.face_compat_var local.icat.sscatml.r0_absorb local.icid.stopp.Dst)
  have h7: "∀xa ∈ X. xa ⊗⇘(i + 1)⇙ ∂ i tt (∂ (i + 1) tt xa) = xa"
    by (metis assms(1) local.face_comm_var local.face_compat_var local.icat.sscatml.r0_absorb)
  have h8: "∀x ∈ X. ∀y ∈ Y. DD (i + 1) x y ⟶ (Γ i tt x ⊗⇘(i + 1)⇙ σ i x) ⊗⇘i⇙ (x ⊗⇘(i + 1)⇙ Γ i tt y) = Γ i tt (x ⊗⇘(i + 1)⇙ y)"
    using assms(1) assms(2) local.conn_corner1 by auto
  have "(ΓΓ i tt X ⋆⇘(i + 1)⇙ σσ i X) ⋆⇘i⇙ (X ⋆⇘(i + 1)⇙ ΓΓ i tt Y) = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xb) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xb xc y. xa ∈ X ∧ xb ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ DD (i + 1) (Γ i tt xa) (σ i xb) ∧ DD (i + 1) xc (Γ i tt y) ∧ DD i (Γ i tt xa ⊗⇘(i + 1)⇙ σ i xb) (xc ⊗⇘(i + 1)⇙ Γ i tt y)}"
    unfolding local.iconv_prop by blast
  also have "… = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xb) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xb xc y. xa ∈ X ∧ xb ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ ∂ (i + 1) tt (Γ i tt xa) = ∂ (i + 1) ff (σ i xb) ∧ ∂ (i + 1) tt xc = ∂ (i + 1) ff (Γ i tt y) ∧ ∂ i tt (Γ i tt xa ⊗⇘(i + 1)⇙ σ i xb) = ∂ i ff (xc ⊗⇘(i + 1)⇙ Γ i tt y)}"
    using icat.st_local by presburger
  also have "… = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xb) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xb xc y. xa ∈ X ∧ xb ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ xa = xb ∧ ∂ (i + 1) tt xc = ∂ (i + 1) ff (Γ i tt y) ∧ ∂ i tt (Γ i tt xa ⊗⇘(i + 1)⇙ σ i xb) = ∂ i ff (xc ⊗⇘(i + 1)⇙ Γ i tt y)}"
    by (smt (verit) Collect_cong assms(1) local.conn_face2 local.sym_type_var)
  also have "… = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xa) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xc y. xa ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ ∂ (i + 1) tt xc = ∂ (i + 1) ff y ∧ ∂ i tt (Γ i tt xa ⊗⇘(i + 1)⇙ σ i xa) = ∂ i ff (xc ⊗⇘(i + 1)⇙ Γ i tt y)}"
    by (smt (verit, best) Collect_cong assms(1) h1 local.conn_face3 local.locality local.sym_type_var)
  also have "… = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xa) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xc y. xa ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ ∂ (i + 1) tt xc = ∂ (i + 1) ff y ∧ ∂ i tt (Γ i tt xa) ⊗⇘(i + 1)⇙ ∂ i tt (σ i xa) = ∂ i ff xc ⊗⇘(i + 1)⇙ ∂ i ff (Γ i tt y)}"
    by (smt (verit, del_insts) h2 h3 Collect_cong assms(1) h1 icat.st_local local.conn_face2 local.sym_type_var)
  also have "… = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xa) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xc y. xa ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ ∂ (i + 1) tt xc = ∂ (i + 1) ff y ∧ xa ⊗⇘(i + 1)⇙ ∂ i tt (∂ (i + 1) tt xa) = xc ⊗⇘(i + 1)⇙ ∂ (i + 1) ff y}"
    by (smt (verit, del_insts) h4 h5 Collect_cong)
  also have "… = {(Γ i tt xa ⊗⇘(i + 1)⇙ σ i xa) ⊗⇘i⇙ (xc ⊗⇘(i + 1)⇙ Γ i tt y) | xa xc y. xa ∈ X ∧ xc ∈ X ∧ y ∈ Y ∧ ∂ (i + 1) tt xc = ∂ (i + 1) ff y ∧ xa = xc}"
    by (smt (z3) h6 h7 Collect_cong assms(2) icid.st_eq1 local.face_comm_var)
  also have "… = {Γ i tt (x ⊗⇘(i + 1)⇙ y) | x y. x ∈ X ∧ y ∈ Y ∧ DD (i + 1) x y}"
    by (smt (verit, ccfv_threshold) h8 Collect_cong icat.st_local)
  also have "… = ΓΓ i tt (X ⋆⇘(i + 1)⇙ Y)"
    unfolding local.iconv_prop by force
  finally show ?thesis
    by simp
qed

lemma conn_corner2_DD:
  assumes "fFx i x"
  and "fFx i y"
  and "DD (i + 1) x y"
  shows "DD i (Γ i ff x ⊗⇘(i + 1)⇙ y) (σ i y ⊗⇘(i + 1)⇙ Γ i ff y)"
proof-
  have h1: "DD (i + 1) (Γ i ff x) y"
    by (metis assms(1) assms(3) conn_zigzag1_var insertCI local.iDst local.icid.ts_msg.src_comp_aux local.locality)
  have h2: "∂ i ff (σ i y ⊗⇘(i + 1)⇙ Γ i ff y) = ∂ i ff (σ i y) ⊗⇘(i + 1)⇙ ∂ i ff (Γ i ff y)"
    using assms(2) local.conn_face2 local.face_func local.locality local.sym_face3_simp by auto
  have "∂ i tt (Γ i ff x ⊗⇘(i + 1)⇙ y) = ∂ i tt (Γ i ff x) ⊗⇘(i + 1)⇙ ∂ i tt y"
    using h1 local.face_func by simp
  hence h4: "∂ i tt (Γ i ff x ⊗⇘(i + 1)⇙ y) = ∂ (i + 1) tt x ⊗⇘(i + 1)⇙ y"
    by (metis (full_types) assms(1) assms(2) icid.st_eq1 local.conn_face4)
  thus ?thesis
    by (metis h2 assms(2) assms(3) local.conn_face1 local.conn_face2 local.face_comm_var local.icid.stopp.Dst local.locality)
qed

lemma conn_corner2_var: "ΓΓ i ff (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = (Γ i ff (∂ i α x) ⊙⇘(i + 1)⇙ ∂ i β y) ⋆⇘i⇙ (σ i (∂ i β y) ⊙⇘(i + 1)⇙ Γ i ff (∂ i β y))"
proof (cases "DD (i + 1) (∂ i α x) (∂ i β y)")
  case True
  have h1: "DD (i + 1) (Γ i ff (∂ i α x)) (∂ i β y)"
    by (metis True insertCI local.conn_zigzag1_var local.iDst local.icid.ts_msg.src_comp_aux local.locality)
  have h2: "DD (i + 1) (σ i (∂ i β y)) (Γ i ff (∂ i β y))"
    by (metis local.conn_face2 local.face_compat_var local.locality)
  have h3: "DD i (Γ i ff (∂ i α x) ⊗⇘(i + 1)⇙ ∂ i β y) (σ i (∂ i β y) ⊗⇘(i + 1)⇙ Γ i ff (∂ i β y))"
    using True local.conn_corner2_DD by simp
  have "ΓΓ i ff (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = {Γ i ff (∂ i α x ⊗⇘(i + 1)⇙ ∂ i β y)}"
    by (metis (full_types) True local.icat.pcomp_def_var4 image_empty image_insert) 
  also have "… = {(Γ i ff (∂ i α x) ⊗⇘(i + 1)⇙ (∂ i β y)) ⊗⇘i⇙ (σ i (∂ i β y) ⊗⇘(i + 1)⇙ Γ i ff (∂ i β y))}"
    using True conn_corner2 local.face_compat_var by simp
 also have "… = {Γ i ff (∂ i α x) ⊗⇘(i + 1)⇙ (∂ i β y)} ⋆⇘i⇙ {σ i (∂ i β y) ⊗⇘(i + 1)⇙ Γ i ff (∂ i β y)}"
   using h3 local.icat.pcomp_def_var4 local.icid.stopp.conv_atom by simp
  also have "… = (Γ i ff (∂ i α x) ⊙⇘(i + 1)⇙ (∂ i β y)) ⋆⇘i⇙ {σ i (∂ i β y) ⊗⇘(i + 1)⇙ Γ i ff (∂ i β y)}"
    by (metis h1 local.icat.functionality_lem_var local.icat.pcomp_def local.icat.sscatml.r0_absorb local.it_absorb)
  also have "… = (Γ i ff (∂ i α x) ⊙⇘(i + 1)⇙ (∂ i β y)) ⋆⇘i⇙ (σ i (∂ i β y) ⊙⇘(i + 1)⇙ Γ i ff (∂ i β y))"
    using h2 local.icat.pcomp_def_var4 by simp
  finally show ?thesis.
next
  case False
  thus ?thesis
    by (metis UN_empty add_eq_self_zero empty_is_image local.conn_face1 local.face_compat_var local.pcomp_face_func_DD multimagma.conv_def nat_neq_iff zero_less_one)
qed

lemma conn_corner2_lift:
  assumes "FFx i X"
  and "FFx i Y"
  shows "ΓΓ i ff (X ⋆⇘(i + 1)⇙ Y) = (ΓΓ i ff X ⋆⇘(i + 1)⇙ Y) ⋆⇘i⇙ (σσ i Y ⋆⇘(i + 1)⇙ ΓΓ i ff Y)"
proof-
  have h1 :"∀x ∈ X. ∀ya ∈ Y. ∂ (i + 1) tt x = ∂ (i + 1) ff ya ⟶ ∂ i tt (Γ i ff x ⊗⇘(i + 1)⇙ ya) = ∂ i tt (Γ i ff x) ⊗⇘(i + 1)⇙ ∂ i tt ya"
    by (metis local.face_func add.commute add_diff_cancel_right' assms(1) bot_nat_0.extremum_unique cancel_comm_monoid_add_class.diff_cancel conn_zigzag1_var empty_not_insert ex_in_conv icat.st_local local.icid.ts_msg.src_comp_aux not_one_le_zero singletonD)
  have h2 :"∀yb ∈ Y. DD (i + 1) (σ i yb) (Γ i ff yb) ⟶ ∂ i ff (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb) = ∂ i ff (σ i yb) ⊗⇘(i + 1)⇙ ∂ i ff (Γ i ff yb)"
    by (simp add: local.face_func)
  have h3: "∀x ∈ X. ∀y ∈ Y. DD (i + 1) x y ⟶ (Γ i ff x ⊗⇘(i + 1)⇙ y) ⊗⇘i⇙ (σ i y ⊗⇘(i + 1)⇙ Γ i ff y) = Γ i ff (x ⊗⇘(i + 1)⇙ y)"
    using assms local.conn_corner2 by simp
  have h4: "∀x ∈ X. ∀ya ∈ Y. (∂ (i + 1) tt (Γ i ff x) = ∂ (i + 1) ff ya) = (∂ (i + 1) tt x = ∂ (i + 1) ff ya)"
    by (metis assms(1) conn_zigzag1_var local.icid.ts_msg.src_comp_aux singletonI)
  have h5: "∀yb ∈ Y. ∀yc ∈ Y. (∂ (i + 1) tt (σ i yb) = ∂ (i + 1) ff (Γ i ff yc)) = (yb = yc)"
    by (metis assms(2) local.conn_face2 local.inv_sym_sym local.sym_face3_simp)
  have h6: "∀x ∈ X. ∀ya ∈ Y. ∀yb ∈ Y. (x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ ∂ (i + 1) tt x = ∂ (i + 1) ff ya ∧ ∂ i tt (Γ i ff x ⊗⇘(i + 1)⇙ ya) = ∂ i ff (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb)) = (x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ ∂ (i + 1) tt x = ∂ (i + 1) ff ya ∧ ∂ i tt (Γ i ff x) ⊗⇘(i + 1)⇙ ∂ i tt ya = ∂ i ff (σ i yb) ⊗⇘(i + 1)⇙ ∂ i ff (Γ i ff yb))"
    using h1 h2 h5 icat.st_local by force
  have "(ΓΓ i ff X ⋆⇘(i + 1)⇙ Y) ⋆⇘i⇙ (σσ i Y ⋆⇘(i + 1)⇙ ΓΓ i ff Y) = {(Γ i ff x ⊗⇘(i + 1)⇙ ya) ⊗⇘i⇙ (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yc) | x ya yb yc. x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ yc ∈ Y ∧ DD (i + 1) (Γ i ff x) ya ∧ DD (i + 1) (σ i yb) (Γ i ff yc) ∧ DD i (Γ i ff x ⊗⇘(i + 1)⇙ ya) (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yc)}"
    unfolding local.iconv_prop by fastforce
  also have "… = {(Γ i ff x ⊗⇘(i + 1)⇙ ya) ⊗⇘i⇙ (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yc) | x ya yb yc. x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ yc ∈ Y ∧ ∂ (i + 1) tt (Γ i ff x) = ∂ (i + 1) ff ya ∧ ∂ (i + 1) tt (σ i yb) = ∂ (i + 1) ff (Γ i ff yc) ∧ ∂ i tt (Γ i ff x ⊗⇘(i + 1)⇙ ya) = ∂ i ff (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yc)}"
    using icat.st_local by simp
  also have "… = {(Γ i ff x ⊗⇘(i + 1)⇙ ya) ⊗⇘i⇙ (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb) | x ya yb. x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ ∂ (i + 1) tt x = ∂ (i + 1) ff ya ∧ ∂ i tt (Γ i ff x ⊗⇘(i + 1)⇙ ya) = ∂ i ff (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb)}"
    using h4 h5 by (smt (verit, del_insts) Collect_cong)
  also have "… = {(Γ i ff x ⊗⇘(i + 1)⇙ ya) ⊗⇘i⇙ (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb) | x ya yb. x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ ∂ (i + 1) tt x = ∂ (i + 1) ff ya ∧ ∂ i tt (Γ i ff x) ⊗⇘(i + 1)⇙ ∂ i tt ya = ∂ i ff (σ i yb) ⊗⇘(i + 1)⇙ ∂ i ff (Γ i ff yb)}"
    using h6 by fastforce
  also have "… = {(Γ i ff x ⊗⇘(i + 1)⇙ ya) ⊗⇘i⇙ (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb) | x ya yb. x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ ∂ (i + 1) tt x = ∂ (i + 1) ff ya ∧ ∂ (i + 1) tt x ⊗⇘(i + 1)⇙ ya = ∂ (i + 1) ff yb ⊗⇘(i + 1)⇙ yb}"
    by (smt (z3) Collect_cong assms(1) assms(2) icid.st_eq1 local.conn_face1 local.conn_face4 local.conn_face2 local.face_comm_var)
  also have "… = {(Γ i ff x ⊗⇘(i + 1)⇙ ya) ⊗⇘i⇙ (σ i yb ⊗⇘(i + 1)⇙ Γ i ff yb) | x ya yb. x ∈ X ∧ ya ∈ Y ∧ yb ∈ Y ∧ ∂ (i + 1) tt x = ∂ (i + 1) ff ya ∧ ya = yb}"
    by force
  also have "… = {Γ i ff (x ⊗⇘(i + 1)⇙ y) | x y. x ∈ X ∧ y ∈ Y ∧ DD (i + 1) x y}"
    by (smt (verit, ccfv_threshold) h3 Collect_cong icat.st_local)
  also have "… = ΓΓ i ff (X ⋆⇘(i + 1)⇙ Y)"
    unfolding local.iconv_prop by force
  finally show ?thesis
    by simp
qed

lemma conn_corner3_var: 
  assumes "j ≠ i ∧ j ≠ i + 1"
  shows "ΓΓ i α (∂ i β x ⊙⇘j⇙ ∂ i γ y) = Γ i α (∂ i β x) ⊙⇘j⇙ Γ i α (∂ i γ y)"
  by (smt (z3) assms empty_is_image image_insert local.conn_corner3 local.conn_face1 local.conn_face3 local.face_compat_var local.iDst local.icat.pcomp_def_var4 local.locality local.pcomp_face_func_DD)

lemma conn_corner3_lift:
  assumes "j ≠ i"
  and "j ≠ i + 1"
  and "FFx i X"
  and "FFx i Y"
  shows "ΓΓ i α (X ⋆⇘j⇙ Y) = ΓΓ i α X ⋆⇘j⇙ ΓΓ i α Y"
proof-
  have h: "∀x ∈ X. ∀y ∈ Y. DD j (Γ i α x) (Γ i α y) = DD j x y"
    by (metis assms icat.st_local local.conn_face1 local.conn_face3 local.face_comm_var)
  have "ΓΓ i α X ⋆⇘j⇙ ΓΓ i α Y = {Γ i α x ⊗⇘j⇙ Γ i α y | x y. x ∈ X ∧ y ∈ Y ∧ DD j (Γ i α x) (Γ i α y)}"
    unfolding local.iconv_prop by force
  also have "… = {Γ i α x ⊗⇘j⇙ Γ i α y | x y. x ∈ X ∧ y ∈ Y ∧ DD j x y}"
    using h by force
  also have "… = {Γ i α (x ⊗⇘j⇙ y) | x y. x ∈ X ∧ y ∈ Y ∧ DD j x y}"
    using conn_corner3 assms by fastforce
  also have "… = ΓΓ i α (X ⋆⇘j⇙ Y)"
    unfolding local.iconv_prop by force
  finally show ?thesis
    by simp
qed

lemma conn_face5 [simp]: "∂ (j + 1) α (Γ j (¬α) (∂ j γ x)) = ∂ (j + 1) α (∂ j γ x)"
  by (smt (verit, ccfv_SIG) icid.s_absorb_var local.conn_corner1_lift_aux local.conn_zigzag1_var local.face_compat_var local.icid.ts_msg.src_comp_cond local.is_absorb singleton_insert_inj_eq')

lemma conn_inv_sym_braid:
  assumes "diffSup i j 2"
  shows "Γ i α (θ j (∂ i β (∂ (j + 1) γ x))) = θ j (Γ i α (∂ i β (∂ (j + 1) γ x)))"
  by (smt (z3) add_diff_cancel_left' assms diff_add_0 diff_is_0_eq' local.conn_face3 local.conn_sym_braid local.face_comm_var local.face_compat_var local.inv_sym_face2 local.inv_sym_sym_var1 local.inv_sym_type_var local.sym_inv_sym nat_1_add_1 nle_le rel_simps(28))

lemma conn_corner4: "ΓΓ i tt (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = (Γ i tt (∂ i α x) ⊙⇘i⇙ ∂ i α x) ⋆⇘(i + 1)⇙ (σ i (∂ i α x) ⊙⇘i⇙ Γ i tt (∂ i β y))"
proof (cases "DD (i + 1) (∂ i α x) (∂ i β y)")
  case True
  have h1: "∂∂ (i+1) tt (Γ i tt (∂ i α x) ⊙⇘i⇙ ∂ i α x) = {σ i (∂ i α x)}"
    by (metis image_empty image_insert local.conn_face1 local.conn_face2 local.face_compat_var local.it_absorb)
  have "∂ (i+1) tt (∂ i α x) = ∂ (i+1) ff (∂ i β y)"
    using True local.iDst by simp
  hence h2: "∂∂ (i+1) ff (σ i (∂ i α x) ⊙⇘i⇙ Γ i tt (∂ i β y)) = {σ i (∂ i α x)}"
    by (smt (z3) add_eq_self_zero conn_face4 conn_face5 icat.st_local image_is_empty local.comp_face_func local.conn_face2 local.face_comm_var local.face_compat_var local.it_absorb subset_singletonD zero_neq_one)
  hence "∂∂ (i+1) tt (Γ i tt (∂ i α x) ⊙⇘i⇙ ∂ i α x) ∩ ∂∂ (i+1) ff (σ i (∂ i α x) ⊙⇘i⇙ Γ i tt (∂ i β y)) ≠ {}"
    using h1 by simp
  thus ?thesis
    by (smt (z3) True add_cancel_right_right dual_order.eq_iff empty_is_image h1 h2 icat.locality_lifting local.conn_corner1_var local.icat.pcomp_def_var4 local.interchange_var multimagma.conv_atom not_one_le_zero)
next
  case False
  thus ?thesis
    by (smt (z3) Union_empty add_eq_self_zero dual_order.eq_iff icat.st_local image_empty local.conn_face4 local.conn_face2 local.face_comm_var local.face_compat_var multimagma.conv_distl not_one_le_zero)
qed

lemma conn_corner5: "ΓΓ i ff (∂ i α x ⊙⇘(i + 1)⇙ ∂ i β y) = (Γ i ff (∂ i α x) ⊙⇘i⇙ σ i (∂ i β y)) ⋆⇘(i + 1)⇙ (∂ i β y ⊙⇘i⇙ Γ i ff (∂ i β y))"
proof (cases "DD (i + 1) (∂ i α x) (∂ i β y)")
  case True
  have h1: "∂∂ (i+1) ff (∂ i β y ⊙⇘i⇙ Γ i ff (∂ i β y)) = {σ i (∂ i β y)}"
    by (metis image_empty image_insert local.conn_face1 local.conn_face2 local.face_compat_var local.is_absorb)
  have "∂ (i+1) tt (∂ i α x) = ∂ (i+1) ff (∂ i β y)"
    using True local.iDst by simp
  hence h2: "∂∂ (i+1) tt (Γ i ff (∂ i α x) ⊙⇘i⇙ σ i (∂ i β y)) = {σ i (∂ i β y)}"
    by (smt (z3) conn_face4 conn_face5 h1 icat.st_local image_insert image_is_empty local.comp_face_func local.conn_face2 local.face_comm_var local.face_compat_var local.icat.functionality_lem_var local.it_absorb subset_singletonD)
  hence "∂∂ (i+1) ff (∂ i β y ⊙⇘i⇙ Γ i ff (∂ i β y)) ∩ ∂∂ (i+1) tt (Γ i ff (∂ i α x) ⊙⇘i⇙ σ i (∂ i β y)) ≠ {}"
    using h1 by simp
  thus ?thesis
    by (smt (z3) True add_cancel_right_right dual_order.eq_iff empty_is_image h1 h2 icat.locality_lifting local.conn_corner2_var local.icat.functionality_lem_var local.interchange_var multimagma.conv_atom not_one_le_zero)
next
  case False
  thus ?thesis
    by (smt (z3) UN_empty add_cancel_right_right dual_order.eq_iff image_empty local.conn_face2 local.face_compat_var local.pcomp_face_func_DD local.sym_func2_DD local.sym_type_var multimagma.conv_def not_one_le_zero)
qed

lemma conn_corner3_alt: "j ≠ i ⟹  j ≠ i + 1 ⟹ ΓΓ i α (∂ i β x ⊙⇘j⇙ ∂ i γ y) = Γ i α (∂ i β x) ⊙⇘j⇙ Γ i α (∂ i γ y)"
  by (simp add: local.conn_corner3_var)

lemma conn_shift2:
  assumes "fFx i x"
  and "fFx (i + 2) x"
shows "θ i (θ (i + 1) (Γ i α x)) = Γ (i + 1) α (θ (i + 1) x)"

proof-
  have "Γ i α x = σ (i + 1) (σ i (Γ (i + 1) α (θ (i + 1) x)))"
    using assms local.conn_shift local.inv_sym_face2 local.inv_sym_face3_simp local.sym_inv_sym by simp
  thus ?thesis
    using assms local.conn_face3 local.inv_sym_face2 local.inv_sym_sym local.inv_sym_type_var local.sym_type_var by simp
qed

end

end