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)"
  by (simp add: PiE_iff Pi_iff)

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)))"
  by (simp add: compose_eq compose_eq_iff)

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