# Theory Globular_Set

theory Globular_Set

imports "HOL-Library.FuncSet"

begin

section ‹Background material on extensional functions›

lemma PiE_imp_Pi: "f ∈ A →⇩E B ⟹ f ∈ A → B" by fast

lemma PiE_iff': "f ∈ A →⇩E B = (f ∈ A → B ∧ f ∈ extensional A)"

abbreviation composing ("_ ∘ _ ↓ _" [60,0,60]59)
where "g ∘ f ↓ D ≡ compose D g f"

lemma compose_PiE: "f ∈ A → B ⟹ g ∈ B → C ⟹ g ∘ f ↓ A ∈ A →⇩E C"
by (metis funcset_compose compose_extensional PiE_iff')

lemma compose_eq_iff: "(g ∘ f ↓ A = k ∘ h ↓ A) = (∀x ∈ A. g (f x) = k (h x))"
proof (safe)
fix x assume "g ∘ f ↓ A = k ∘ h ↓ A" "x ∈ A"
then show "g (f x) = k (h x)" by (metis compose_eq)
next
assume "∀x ∈ A. g (f x) = k (h x)"
hence "⋀x. x ∈ A ⟹ (g ∘ f ↓ A) x = (k ∘ h ↓ A) x" by (metis compose_eq)
then show "g ∘ f ↓ A = k ∘ h ↓ A" by (metis extensionalityI compose_extensional)
qed

lemma compose_eq_if: "(⋀x. x ∈ A ⟹ g (f x) = k (h x)) ⟹ g ∘ f ↓ A = k ∘ h ↓ A"
using compose_eq_iff by blast

lemma compose_compose_eq_iff2: "(h ∘ (g ∘ f ↓ A) ↓ A = h' ∘ (g' ∘ f' ↓ A) ↓ A) =
(∀x ∈ A. h (g (f x)) = h' (g' (f' x)))"

lemma compose_compose_eq_iff1: assumes "f ∈ A → B" "f' ∈ A → B"
shows "((h ∘ g ↓ B) ∘ f ↓ A = (h' ∘ g' ↓ B) ∘ f' ↓ A) = (∀x ∈ A. h (g (f x)) = h' (g' (f' x)))"
proof -
have "(h ∘ g ↓ B) ∘ f ↓ A = h ∘ (g ∘ f ↓ A) ↓ A" by (metis assms(1) compose_assoc)
moreover have "(h' ∘ g' ↓ B) ∘ f' ↓ A = h' ∘ (g' ∘ f' ↓ A) ↓ A" by (metis assms(2) compose_assoc)
ultimately have h: "((h ∘ g ↓ B) ∘ f ↓ A = (h' ∘ g' ↓ B) ∘ f' ↓ A) =
(h ∘ (g ∘ f ↓ A) ↓ A = h' ∘ (g' ∘ f' ↓ A) ↓ A)" by presburger
then show ?thesis by (simp only: h compose_compose_eq_iff2)
qed

lemma compose_compose_eq_if1: "⟦f ∈ A → B; f' ∈ A → B; ∀x ∈ A. h (g (f x)) = h' (g' (f' x))⟧ ⟹
(h ∘ g ↓ B) ∘ f ↓ A = (h' ∘ g' ↓ B) ∘ f' ↓ A"
using compose_compose_eq_iff1 by blast

lemma compose_compose_eq_if2: "∀x ∈ A. h (g (f x)) = h' (g' (f' x)) ⟹
h ∘ (g ∘ f ↓ A) ↓ A = h' ∘ (g' ∘ f' ↓ A) ↓ A"
using compose_compose_eq_iff2 by blast

lemma compose_restrict_eq1: "f ∈ A → B ⟹  restrict g B ∘ f ↓ A = g ∘ f ↓ A"
by (smt (verit) PiE compose_eq_iff restrict_apply')

lemma compose_restrict_eq2: "g ∘ (restrict f A) ↓ A = g ∘ f ↓ A"
by (metis (mono_tags, lifting) compose_eq_if restrict_apply')

lemma compose_Id_eq_restrict: "g ∘ (λx ∈ A. x) ↓ A = restrict g A"
by (smt (verit) compose_restrict_eq1 compose_def restrict_apply' restrict_ext)

section ‹Globular sets›

subsection ‹Globular sets›

text ‹
We define a locale ‹globular_set› that encodes the cell data of a strict $\omega$-category
\cite[Def 1.4.5]{Leinster2004}. The elements of ‹X n› are the ‹n›-cells, and the maps ‹s›
and ‹t› give the source and target of a cell, respectively.
›

locale globular_set =
fixes X :: "nat ⇒ 'a set" and s :: "nat ⇒ 'a ⇒ 'a" and t :: "nat ⇒ 'a ⇒ 'a"
assumes s_fun: "s n ∈ X (Suc n) → X n"
and   t_fun: "t n ∈ X (Suc n) → X n"
and  s_comp: "x ∈ X (Suc (Suc n)) ⟹ s n (t (Suc n) x) = s n (s (Suc n) x)"
and  t_comp: "x ∈ X (Suc (Suc n)) ⟹ t n (s (Suc n) x) = t n (t (Suc n) x)"
begin

lemma s_comp': "s n ∘ t (Suc n) ↓ X (Suc (Suc n)) = s n ∘ s (Suc n) ↓ X (Suc (Suc n))"
by (metis (full_types) compose_eq_if s_comp)

lemma t_comp': "t n ∘ s (Suc n) ↓ X (Suc (Suc n)) = t n ∘ t (Suc n) ↓ X (Suc (Suc n))"
by (metis (full_types) compose_eq_if t_comp)

text ‹These are the generalised source and target maps. The arguments are the dimension of the
input and output, respectively. They allow notation similar to ‹s⇧m⇧-⇧p› in \cite{Leinster2004}.›

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

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

lemma s'_n_n [simp]: "s' n n = id"
by (cases n, simp_all)

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

lemma s'_Suc_Suc_n_n [simp]: "s' (Suc (Suc n)) n = s n ∘ s (Suc n)"
by simp

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

lemma s'_Suc': "n < m ⟹ s' m n = s n ∘ s' m (Suc n)"
proof (induction m arbitrary: n)
case 0
then show ?case by blast
next
case (Suc m)
hence "n ≤ m" by fastforce
show ?case proof (cases "n = m", simp)
assume "n ≠ m"
then show "s' (Suc m) n = s n ∘ s' (Suc m) (Suc n)" using Suc by fastforce
qed
qed

lemma t'_n_n [simp]: "t' n n = id"
by (cases n, simp_all)

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

lemma t'_Suc_Suc_n_n [simp]: "t' (Suc (Suc n)) n = t n ∘ t (Suc n)"
by simp

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

lemma t'_Suc': "n < m ⟹ t' m n = t n ∘ t' m (Suc n)"
proof (induction m arbitrary: n)
case 0
then show ?case by blast
next
case (Suc m)
hence "n ≤ m" by fastforce
show ?case proof (cases "n = m", simp)
assume "n ≠ m"
then show "t' (Suc m) n = t n ∘ t' (Suc m) (Suc n)" using Suc by fastforce
qed
qed

lemma s'_fun: "n ≤ m ⟹ s' m n ∈ X m → X n"
proof (induction m arbitrary: n)
case 0
thus ?case by force
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 s_fun s'_Suc by auto
qed
qed

lemma t'_fun: "n ≤ m ⟹ t' m n ∈ X m → X n"
proof (induction m arbitrary: n)
case 0
thus ?case by force
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 t_fun t'_Suc by auto
qed
qed

lemma s'_comp: "⟦ n < m; x ∈ X m ⟧ ⟹ s n (t' m (Suc n) x) = s' m n x"
proof (induction "m - n" arbitrary: n)
case 0
then show ?case by force
next
case IH: (Suc k)
show ?case proof (cases k)
case 0
with IH(2) have "m = Suc n" by fastforce
then show ?thesis using s'_Suc' by auto
next
case (Suc k')
with ‹Suc k = m - n› have hle: "Suc (Suc n) ≤ m" by simp
hence "Suc n < m" by force
hence "Suc (Suc n) ≤ m" by fastforce
have "s n (t' m (Suc n) x)
= s n (t (Suc n) (t' m (Suc (Suc n)) x))" using t'_Suc' ‹Suc n < m› by simp
also have "… = s n (s (Suc n) (t' m (Suc (Suc n)) x))"
using t'_fun ‹Suc (Suc n) ≤ m› s_comp IH(4) by blast
also have "… = s n (s' m (Suc n) x)"
using IH Suc_diff_Suc Suc_inject ‹Suc n < m› by presburger
finally show ?thesis using ‹n < m› s'_Suc' by simp
qed
qed

lemma t'_comp: "⟦ n < m; x ∈ X m ⟧ ⟹ t n (s' m (Suc n) x) = t' m n x"
proof (induction "m - n" arbitrary: n)
case 0
then show ?case by force
next
case IH: (Suc k)
show ?case proof (cases k)
case 0
with IH(2) have "m = Suc n" by fastforce
then show ?thesis using IH.prems(1) by auto
next
case (Suc k')
with ‹Suc k = m - n› have hle: "Suc (Suc n) ≤ m" by simp
hence "Suc n < m" by force
hence "Suc (Suc n) ≤ m" by fastforce
have "t n (s' m (Suc n) x)
= t n (s (Suc n) (s' m (Suc (Suc n)) x))" using s'_Suc' ‹Suc n < m› by simp
also have "… = t n (t (Suc n) (s' m (Suc (Suc n)) x))"
using s'_fun ‹Suc (Suc n) ≤ m› t_comp IH(4) by blast
also have "… = t n (t' m (Suc n) x)"
using IH Suc_diff_Suc Suc_inject ‹Suc n < m› by presburger
finally show ?thesis using ‹n < m› t'_Suc' by simp
qed
qed

text ‹The following predicates and sets are needed to define composition in an $\omega$-category.›

definition is_parallel_pair :: "nat ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool" where
"is_parallel_pair m n x y ≡ n ≤ m ∧ x ∈ X m ∧ y ∈ X m ∧ s' m n x = s' m n y ∧ t' m n x = t' m n y"

text ‹\cite[p. 44]{Leinster2004}›
definition is_composable_pair :: "nat ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool" where
"is_composable_pair m n y x ≡ n < m ∧ y ∈ X m ∧ x ∈ X m ∧ t' m n x = s' m n y"

definition composable_pairs :: "nat ⇒ nat ⇒ ('a × 'a) set" where
"composable_pairs m n = {(y, x). is_composable_pair m n y x}"

lemma composable_pairs_empty: "m ≤ n ⟹ composable_pairs m n = {}"
using is_composable_pair_def composable_pairs_def by simp

end

subsection ‹Maps between globular sets›

text ‹We define maps between globular sets to be natural transformations of the corresponding
functors \cite[Def 1.4.5]{Leinster2004}.›

locale globular_map = source: globular_set X s⇩X t⇩X + target: globular_set Y s⇩Y t⇩Y
for X s⇩X t⇩X Y s⇩Y t⇩Y +
fixes φ :: "nat ⇒ 'a ⇒ 'b"
assumes map_fun: "φ m ∈ X m → Y m"
and   is_natural_wrt_s: "x ∈ X (Suc m) ⟹ φ m (s⇩X m x) = s⇩Y m (φ (Suc m) x)"
and   is_natural_wrt_t: "x ∈ X (Suc m) ⟹ φ m (t⇩X m x) = t⇩Y m (φ (Suc m) x)"
begin

lemma is_natural_wrt_s': "⟦ n ≤ m; x ∈ X m ⟧ ⟹ φ n (source.s' m n x) = target.s' m n (φ m x)"
proof (induction "m - n" arbitrary: n)
case 0
hence "m = n" by simp
then show ?case by fastforce
next
case (Suc k)
hence "n < m" by force
hence "Suc n ≤ m" by auto
have "φ n (source.s' m n x) = φ n (s⇩X n (source.s' m (Suc n) x))"
using source.s'_Suc' ‹n < m› by simp
also have "… = s⇩Y n (φ (Suc n) (source.s' m (Suc n) x))"
using source.s'_fun ‹Suc n ≤ m› Suc(1) Suc(4) is_natural_wrt_s by blast
also have "… = s⇩Y n (target.s' m (Suc n) (φ m x))"
using Suc ‹Suc n ≤ m› Suc_diff_Suc Suc_inject ‹n < m› by presburger
finally show ?case using target.s'_Suc' ‹n < m› by simp
qed

lemma is_natural_wrt_t': "⟦ n ≤ m; x ∈ X m ⟧ ⟹ φ n (source.t' m n x) = target.t' m n (φ m x)"
proof (induction "m - n" arbitrary: n)
case 0
hence "m = n" by simp
then show ?case by fastforce
next
case (Suc k)
hence "n < m" by force
hence "Suc n ≤ m" by auto
have "φ n (source.t' m n x) = φ n (t⇩X n (source.t' m (Suc n) x))"
using source.t'_Suc' ‹n < m› by simp
also have "… = t⇩Y n (φ (Suc n) (source.t' m (Suc n) x))"
using source.t'_fun ‹Suc n ≤ m› Suc(1) Suc(4) is_natural_wrt_t by blast
also have "… = t⇩Y n (target.t' m (Suc n) (φ m x))"
using Suc ‹Suc n ≤ m› Suc_diff_Suc Suc_inject ‹n < m› by presburger
finally show ?case using target.t'_Suc' ‹n < m› by simp
qed

end

text ‹The composition of two globular maps is itself a globular map. This intermediate
locale gathers the data needed for such a statement.›
locale two_globular_maps = fst: globular_map X s⇩X t⇩X Y s⇩Y t⇩Y φ + snd: globular_map Y s⇩Y t⇩Y Z s⇩Z t⇩Z ψ
for X s⇩X t⇩X Y s⇩Y t⇩Y Z s⇩Z t⇩Z φ ψ

sublocale two_globular_maps ⊆ comp: globular_map X s⇩X t⇩X Z s⇩Z t⇩Z "λm. ψ m ∘ φ m"
proof (unfold_locales)
fix m
show "ψ m ∘ φ m ∈ X m → Z m" using fst.map_fun snd.map_fun by fastforce
next
fix x m assume "x ∈ X (Suc m)"
then show "(ψ m ∘ φ m) (s⇩X m x) = s⇩Z m ((ψ (Suc m) ∘ φ (Suc m)) x)"
using fst.is_natural_wrt_s snd.is_natural_wrt_s comp_apply fst.map_fun by fastforce
next
fix x m assume "x ∈ X (Suc m)"
then show "(ψ m ∘ φ m) (t⇩X m x) = t⇩Z m ((ψ (Suc m) ∘ φ (Suc m)) x)"
using fst.is_natural_wrt_t snd.is_natural_wrt_t comp_apply fst.map_fun by fastforce
qed

sublocale two_globular_maps ⊆ compose: globular_map X s⇩X t⇩X Z s⇩Z t⇩Z "λm. ψ m ∘ φ m ↓ X m"
proof (unfold_locales)
fix m
show "ψ m ∘ φ m ↓ X m ∈ X m → Z m" using funcset_compose fst.map_fun snd.map_fun by fast
next
fix x m assume "x ∈ X (Suc m)"
then show "(ψ m ∘ φ m ↓ X m) (s⇩X m x) = s⇩Z m ((ψ (Suc m) ∘ φ (Suc m) ↓ X (Suc m)) x)"
by (metis PiE fst.is_natural_wrt_s snd.is_natural_wrt_s fst.map_fun compose_eq fst.source.s_fun)
next
fix x m assume "x ∈ X (Suc m)"
then show "(ψ m ∘ φ m ↓ X m) (t⇩X m x) = t⇩Z m ((ψ (Suc m) ∘ φ (Suc m) ↓ X (Suc m)) x)"
by (metis PiE fst.is_natural_wrt_t snd.is_natural_wrt_t fst.map_fun compose_eq fst.source.t_fun)
qed

subsection ‹The terminal globular set›

text ‹The terminal globular set, with a unique m-cell for each m \cite[p. 264]{Leinster2004}.›

interpretation final_glob: globular_set "λm. {()}" "λm. id" "λm. id"
by (unfold_locales, auto)

context globular_set
begin

text ‹\cite[p. 272]{Leinster2004}›

interpretation map_to_final_glob: globular_map X s t
"λm. {()}" "λm. id" "λm. id"
"λm. (λx. ())"
by (unfold_locales, simp_all)

end

end