Theory Strict_Omega_Category

theory Strict_Omega_Category
imports Globular_Set

begin

section ‹Strict $\omega$-categories›

text ‹
  First, we define a locale ‹pre_strict_omega_category› that holds the data of a strict
  $\omega$-category without the associativity, unity and exchange axioms
  \cite[Def 1.4.8 (a) - (b)]{Leinster2004}. We do this in order to set up convenient notation
  before we state the remaining axioms.
›

locale pre_strict_omega_category = globular_set +
  fixes comp :: "nat ⇒ nat ⇒ 'a ⇒ 'a ⇒ 'a"
    and i :: "nat ⇒ 'a ⇒ 'a"
  assumes comp_fun: "is_composable_pair m n x' x ⟹ comp m n x' x ∈ X m"
    and i_fun: "i n ∈ X n → X (Suc n)"
    and s_comp_Suc: "is_composable_pair (Suc m) m x' x ⟹ s m (comp (Suc m) m x' x) = s m x"
    and t_comp_Suc: "is_composable_pair (Suc m) m x' x ⟹ t m (comp (Suc m) m x' x) = t m x'"
    and s_comp: "⟦is_composable_pair (Suc m) n x' x; n < m⟧ ⟹
          s m (comp (Suc m) n x' x) = comp m n (s m x') (s m x)"
    and t_comp: "⟦is_composable_pair (Suc m) n x' x; n < m⟧ ⟹
          t m (comp (Suc m) n x' x) = comp m n (t m x') (s m x)"
    and s_i: "x ∈ X n ⟹ s n (i n x) = x"
    and t_i: "x ∈ X n ⟹ t n (i n x) = x"
begin

text ‹Similar to the generalised source and target maps in ‹globular_set›, we defined a generalised
identity map. The first argument gives the dimension of the resulting identity cell, while the
second gives the dimension of the input cell.›

fun i' :: "nat ⇒ nat ⇒ 'a ⇒ 'a" where
"i' 0 0 = id" |
"i' 0 (Suc n) = undefined" |
"i' (Suc m) n = (if Suc m < n then undefined
  else if Suc m = n then id
  else i m ∘ i' m n)"

lemma i'_n_n [simp]: "i' n n = id"
  by (metis i'.elims i'.simps(1) less_irrefl_nat)

lemma i'_Suc_n_n [simp]: "i' (Suc n) n = i n"
  by simp

lemma i'_Suc [simp]: "n ≤ m ⟹ i' (Suc m) n = i m ∘ i' m n"
  by fastforce

lemma i'_Suc': "n < m ⟹ i' m n = i' m (Suc n) ∘ i n"
proof (induction m arbitrary: n)
  case 0
  then show ?case by blast
next
  case (Suc m)
  then show ?case by force
qed

lemma i'_fun: "n ≤ m ⟹ i' m n ∈ X n → X m"
proof (induction m arbitrary: n)
  case 0
  then show ?case by fastforce
next
  case (Suc m)
  thus ?case proof (cases "n = Suc m")
    case True
    then show ?thesis by auto
  next
    case False
    hence "n ≤ m" using `n ≤ Suc m` by force
    thus ?thesis using Suc.IH i_fun by auto
  qed
qed
  
end

text ‹Now we may define a strict $\omega$-category including the composition, unity and exchange
  axioms \cite[Def 1.4.8 (c) - (f)]{Leinster2004}.›

locale strict_omega_category = pre_strict_omega_category +
  assumes comp_assoc: "⟦is_composable_pair m n x' x; is_composable_pair m n x'' x'⟧ ⟹ 
            comp m n (comp m n x'' x') x = comp m n x'' (comp m n x' x)"
    and i_comp: "⟦n < m; x ∈ X m⟧ ⟹ comp m n (i' m n (t' m n x)) x = x"
    and comp_i: "⟦n < m; x ∈ X m⟧ ⟹ comp m n x (i' m n (s' m n x)) = x"
    and bin_interchange: "⟦q < p; p < m;
          is_composable_pair m p y' y; is_composable_pair m p x' x;
          is_composable_pair m q y' x'; is_composable_pair m q y x⟧ ⟹
          comp m q (comp m p y' y) (comp m p x' x) = comp m p (comp m q y' x') (comp m q y x)"
    and null_interchange: "⟦q < p; is_composable_pair p q x' x⟧ ⟹
          comp (Suc p) q (i p x') (i p x) = i p (comp p q x' x)"

locale strict_omega_functor = globular_map + 
  source: strict_omega_category X s⇩X t⇩X comp⇩X i⇩X + 
  target: strict_omega_category Y s⇩Y t⇩Y comp⇩Y i⇩Y 
  for comp⇩X i⇩X comp⇩Y i⇩Y +
  assumes commute_with_comp: "is_composable_pair m n x' x ⟹
      φ m (comp⇩X m n x' x) = comp⇩Y m n (φ m x') (φ m x)"
    and commute_with_id: "x ∈ X n ⟹ φ (Suc n) (i⇩X n x) = i⇩Y n (φ n x)"

end