Theory CubicalOmegaZeroCategoriesConnections

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

section‹Cubical $(\omega,0)$-Categories with Connections›

theory CubicalOmegaZeroCategoriesConnections
  imports CubicalCategoriesConnections

begin

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

text ‹First we define shell-invertibility.›

abbreviation (in cubical_omega_category_connections) "ri_inv i x y ≡ (DD i x y ∧ DD i y x ∧ x ⊗⇘i⇙ y = ∂ i ff x ∧ y ⊗⇘i⇙ x = ∂ i tt x)"

abbreviation (in cubical_omega_category_connections) "ri_inv_shell k i x ≡ (∀j α. j + 1 ≤ k ∧ j ≠ i ⟶ (∃y. ri_inv i (∂ j α x) y))"

text ‹Next we define the class of cubical $(\omega,0)$-categories with connections.›

class cubical_omega_zero_category_connections = cubical_omega_category_connections +
  assumes ri_inv: "k ≥ 1 ⟹ i ≤ k - 1 ⟹ dim_bound k x ⟹ ri_inv_shell k i x ⟹ ∃y. ri_inv i x y"

begin

text ‹Finally, to show our axiomatisation at work we prove Proposition 2.4.7 from our companion paper, namely that every
cell in an $(\omega,0)$-category is ri-invertible for each natural number i. This requires some background theory engineering.›

lemma ri_inv_fix:
  assumes "fFx i x"
  shows "∃y. ri_inv i x y"
  by (metis assms icat.st_local local.face_compat_var local.icat.sscatml.l0_absorb)

lemma ri_inv2:
  assumes "k ≥ 1"
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
  shows "∃y. ri_inv i x y"
  proof (cases "i ≤ k - 1")
  case True
  thus ?thesis
    using assms local.ri_inv by simp
next
  case False
  hence "fFx i x"
    using assms(2) by fastforce
  thus ?thesis
    using ri_inv_fix by simp
qed

lemma ri_inv3: 
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
  shows "∃y. ri_inv i x y"
proof (cases "k = 0")
  case True
  thus ?thesis
    using assms(1) less_eq_nat.simps(1) ri_inv_fix by simp
next
  case False
  hence "k ≥ 1"
    by simp
  thus ?thesis
    using assms ri_inv2 by simp
qed

lemma ri_unique: "(∃y. ri_inv i x y) = (∃!y. ri_inv i x y)"
  by (metis local.icat.pcomp_assoc local.icat.sscatml.assoc_defined local.icat.sscatml.l0_absorb local.icat.sts_msg.st_local local.pcomp_uface)

lemma ri_unique_var: "ri_inv i x y ⟹ ri_inv i x z ⟹ y = z"
  using ri_unique by fastforce

definition "ri i x = (THE y. ri_inv i x y)"

lemma ri_inv_ri: "ri_inv i x y ⟹ (y = ri i x)"
proof-
  assume a: "ri_inv i x y"
  hence "∃!y. ri_inv i x y"
    using ri_unique by blast
  thus "y = ri i x"
    unfolding ri_def 
    by (smt (verit, ccfv_threshold) a the_equality)
qed

lemma ri_def_prop:
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
shows "DD i x (ri i x) ∧ DD i (ri i x) x ∧ x ⊗⇘i⇙ (ri i x) = ∂ i ff x ∧ (ri i x) ⊗⇘i⇙ x = ∂ i tt x"
proof-
  have "∃y. ri_inv i x y"
    using assms ri_inv3 by blast
  hence "∃!y. DD i x y ∧ DD i y x ∧ x ⊗⇘i⇙ y = ∂ i ff x ∧ y ⊗⇘i⇙ x = ∂ i tt x"
    by (simp add: ri_unique)
  hence "DD i x (ri i x) ∧ DD i (ri i x) x ∧ x ⊗⇘i⇙ (ri i x) = ∂ i ff x ∧ (ri i x) ⊗⇘i⇙ x = ∂ i tt x"
    unfolding ri_def by (smt (verit, del_insts) theI')
  thus ?thesis
    by simp
qed

lemma ri_right:
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
  shows "x ⊗⇘i⇙ ri i x = ∂ i ff x"
  using assms ri_def_prop by simp

lemma ri_right_set:
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
  shows "x ⊙⇘i⇙ ri i x = {∂ i ff x}"
  using assms local.icat.pcomp_def_var3 ri_def_prop by blast

lemma ri_left:
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
  shows "ri i x ⊗⇘i⇙ x = ∂ i tt x"
  using assms ri_def_prop by simp

lemma ri_left_set:
  assumes "dim_bound k x"
  and "ri_inv_shell k i x"
  shows "ri i x ⊙⇘i⇙ x = {∂ i tt x}"
  using assms local.icat.pcomp_def_var3 ri_def_prop by blast

lemma dim_face: "dim_bound k x ⟹ dim_bound k (∂ i α x)"
  by (metis local.double_fix_prop local.face_comm_var)

lemma dim_ri_inv:
  assumes "dim_bound k x"
  and "ri_inv i x y"
  shows "dim_bound k y"
proof-
  {fix l α
  assume ha: "l ≥ k"
  have h1: "DD i x (∂ l α y)"
    by (smt (verit, ccfv_threshold) assms ha icat.st_local icid.s_absorb_var3 local.pcomp_face_func_DD)
  have h2: "DD i (∂ l α y) x"
    by (metis (full_types) assms ha icid.ts_compat local.iDst local.locality local.pcomp_face_func_DD)
  have "∂ l α (x ⊗⇘i⇙ y) = ∂ l α x ⊗⇘i⇙ ∂ l α y"
    by (metis ha assms(1) assms(2) local.fFx_prop local.face_func local.icat.sscatml.r0_absorb local.pcomp_uface)
  hence h3: "∂ l α (x ⊗⇘i⇙ y) = x ⊗⇘i⇙ ∂ l α y"
    by (metis assms(1) ha local.face_compat_var)
  have "∂ l α (y ⊗⇘i⇙ x) = ∂ l α y ⊗⇘i⇙ ∂ l α x"
    by (metis ha assms(1) assms(2) local.fFx_prop local.face_func local.icat.sscatml.r0_absorb local.pcomp_uface)
  hence "∂ l α (y ⊗⇘i⇙ x) = ∂ l α y ⊗⇘i⇙ x"
    by (metis assms(1) ha local.face_compat_var)
  hence "ri_inv i x (∂ l α y)"
    by (smt (z3) assms(1) assms(2) h1 h2 h3 ha icid.ts_compat local.face_comm_var)
  hence "∂ l α y = y"
    using ri_unique_var assms(2) by blast}
  thus ?thesis
    by simp
qed

lemma every_dim_k_ri_inv:
  assumes "dim_bound k x"
  shows "∀i. ∃y. ri_inv i x y" using ‹dim_bound k x›
proof (induct k arbitrary: x)
  case 0
  thus ?case 
    using ri_inv_fix by simp
next
  case (Suc k)
  {fix i
    have "∃y. ri_inv i x y"
    proof (cases "Suc k ≤ i")
      case True 
      thus ?thesis
        using Suc.prems ri_inv_fix by simp
    next
      case False
      {fix j α
        assume h: "j ≤ k ∧ j ≠ i"
        hence a: "dim_bound k (Σ j (k - j) (∂ j α x))"
          by (smt (z3) Suc.prems antisym_conv2 le_add_diff_inverse local.face_comm_var local.face_compat_var local.symcomp_face2 local.symcomp_type_var nle_le not_less_eq_eq)
        have "∃y. ri_inv i (∂ j α x) y"
        proof (cases "j < i")
          case True
          obtain y where b: "ri_inv (i - 1) (Σ j (k - j) (∂ j α x)) y"
            using Suc.hyps a by force
          have c: "dim_bound k y"
            apply (rule dim_ri_inv[where x = "Σ j (k - j) (∂ j α x)"])
            using a b by simp_all 
          hence d: "DD i (∂ j α x) (Θ j (k - j) y)"
            by (smt (verit) False True a b h icid.ts_compat le_add_diff_inverse local.iDst local.icid.stopp.ts_compat local.inv_symcomp_face1 local.inv_symcomp_symcomp local.locality nle_le not_less_eq_eq)
          hence e: "DD i (Θ j (k - j) y) (∂ j α x)"
            by (smt (verit) False True b c dual_order.refl h icid.ts_compat le_add_diff_inverse local.iDst local.icid.stopp.ts_compat local.inv_symcomp_face1 local.inv_symcomp_symcomp local.locality local.symcomp_type_var not_less_eq_eq)
          have f: "∂ j α x ⊗⇘i⇙ Θ j (k - j) y = Θ j (k - j) (Σ j (k - j) (∂ j α x) ⊗⇘(i - 1)⇙ y)"
            apply (subst inv_symcomp_comp4)
            using True local.symcomp_type_var1 c False One_nat_def b local.face_compat_var local.inv_symcomp_symcomp a by auto
          have "Θ j (k - j) y ⊗⇘i⇙ ∂ j α x = Θ j (k - j) (y ⊗⇘(i - 1)⇙ Σ j (k - j) (∂ j α x))"
            apply (subst inv_symcomp_comp4)
            using True local.symcomp_type_var1 b c False local.face_compat_var local.inv_symcomp_symcomp a by simp_all
          thus ?thesis
            by (metis False True b c d dual_order.refl e f h le_add_diff_inverse local.icid.stopp.Dst local.inv_symcomp_face1 not_less_eq_eq)
        next
          case False
          obtain y where b: "ri_inv i (Σ j (k - j) (∂ j α x)) y"
            using Suc.hyps a by presburger
          have c: "dim_bound k y"
            apply (rule dim_ri_inv[where x = "Σ j (k - j) (∂ j α x)"])
            using a b by simp_all
          hence d: "DD i (∂ j α x) (Θ j (k - j) y)"
            by (smt (verit) False a b dual_order.refl h icid.ts_compat le_add_diff_inverse linorder_neqE_nat local.iDst local.icid.stopp.ts_compat local.inv_symcomp_face2 local.inv_symcomp_symcomp local.locality)
          hence e: "DD i (Θ j (k - j) y) (∂ j α x)"
            by (smt (z3) False add.commute b c dual_order.refl h le_add_diff_inverse2 linorder_neqE_nat local.face_comm_var local.face_compat_var local.iDst local.inv_symcomp_face2 local.inv_symcomp_symcomp local.locality local.symcomp_face2)
          have f: "∂ j α x ⊗⇘i⇙ Θ j (k - j) y = Θ j (k - j) (Σ j (k - j) (∂ j α x) ⊗⇘i⇙ y)"
            apply (subst inv_symcomp_comp2)
            using False h nat_neq_iff local.symcomp_type_var1 b c a local.face_compat_var local.inv_symcomp_symcomp by simp_all
          have "Θ j (k - j) y ⊗⇘i⇙ ∂ j α x = Θ j (k - j) (y ⊗⇘i⇙ Σ j (k - j) (∂ j α x))"
            apply (subst inv_symcomp_comp2)
            using False h a b c local.inv_symcomp_symcomp by simp_all
          thus ?thesis
            by (metis False antisym_conv3 b d e f h local.face_compat_var local.inv_symcomp_face2 local.inv_symcomp_symcomp local.symcomp_type_var1)
        qed}
      thus ?thesis
        apply (intro ri_inv[where k = "k + 1"])
        using False Suc.prems by simp_all
    qed}
  thus ?case
    by simp
qed

text ‹We can now show that every cell is ri-invertible in every direction i.›

lemma every_ri_inv: "∃y. ri_inv i x y"
  using every_dim_k_ri_inv local.fin_fix by blast

end

end