# 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