Theory ICatoids

(*
Title: Indexed Catoids
Authors: Tanguy Massacrier, Georg Struth
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section‹Indexed Catoids›

theory ICatoids
  imports Catoids.Catoid

begin

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

no_notation src (‹σ›)

notation True (‹tt›) 
notation False (‹ff›)

abbreviation Fix :: "('a ⇒ 'a) ⇒ 'a set" where
  "Fix f ≡ {x. f x = x}"

text ‹First we lift locality to powersets.›

lemma (in local_catoid) locality_lifting: "(X ⋆ Y ≠ {}) = (Tgt X ∩ Src Y ≠ {})"
proof-
  have "(X ⋆ Y ≠ {}) = (∃x y. x ∈ X ∧ y ∈ Y ∧ x ⊙ y ≠ {})"
    by (metis (mono_tags, lifting) all_not_in_conv conv_exp2)
  also have "… = (∃x y. x ∈ X ∧ y ∈ Y ∧ tgt x = src y)"
    using local.st_local by auto
  also have "… = (Tgt X ∩ Src Y ≠ {})"
    by blast
  finally show ?thesis.
qed

text ‹The following lemma about functional catoids is useful in proofs.›

lemma (in functional_catoid) pcomp_def_var4: "Δ x y ⟹ x ⊙ y = {x ⊗ y}"
  using local.pcomp_def_var3 by blast


subsection ‹Indexed catoids and categories›

class face_map_op = 
  fixes fmap :: "nat ⇒ bool ⇒ 'a ⇒ 'a" (‹∂›) 

begin

abbreviation Face :: "nat ⇒ bool ⇒ 'a set ⇒ 'a set" (‹∂∂›) where
  "∂∂ i α ≡ image (∂ i α)"

abbreviation face_fix :: "nat ⇒ 'a set" where
  "face_fix i ≡ Fix (∂ i ff)"

abbreviation "fFx i x ≡ (∂ i ff x = x)"

abbreviation "FFx i X ≡ (∀x ∈ X. fFx i x)"

end

class icomp_op =
  fixes icomp :: "'a ⇒ nat ⇒ 'a ⇒ 'a set" (‹_⊙⇘_⇙_›[70,70,70]70)

class imultisemigroup = icomp_op +
  assumes iassoc: "(⋃v ∈ y ⊙⇘i⇙ z. x ⊙⇘i⇙ v) = (⋃v ∈ x ⊙⇘i⇙ y. v ⊙⇘i⇙ z)"

begin

sublocale ims: multisemigroup "λx y. x ⊙⇘i⇙ y"
  by unfold_locales (simp add: local.iassoc)

abbreviation "DD ≡ ims.Δ"

abbreviation iconv :: "'a set ⇒ nat ⇒ 'a set ⇒ 'a set" (‹_⋆⇘_⇙_›[70,70,70]70) where
  "X ⋆⇘i⇙ Y ≡ ims.conv i X Y"

end

class icatoid = imultisemigroup + face_map_op +
  assumes iDst: "DD i x y ⟹ ∂ i tt x = ∂ i ff y"
  and is_absorb [simp]: "(∂ i ff x) ⊙⇘i⇙ x = {x}"
  and it_absorb [simp]: "x ⊙⇘i⇙ (∂ i tt x) = {x}"

begin

text ‹Every indexed catoid is a catoid. ›

sublocale icid: catoid "λx y. x ⊙⇘i⇙ y" "∂ i ff" "∂ i tt"
  by unfold_locales (simp_all add: iDst)

lemma lFace_Src: "∂∂ i ff = icid.Src i"
  by simp

lemma uFace_Tgt: "∂∂ i tt = icid.Tgt i"
  by simp

lemma face_fix_sfix: "face_fix = icid.sfix"
  by force

lemma face_fix_tfix: "face_fix = icid.tfix"
  using icid.stopp.stfix_set by presburger

lemma face_fix_prop [simp]: "x ∈ face_fix i = (∂ i α x = x)"
  by (smt (verit, del_insts) icid.stopp.st_fix mem_Collect_eq)

lemma fFx_prop: "fFx i x = (∂ i α x = x)"
  by (metis icid.st_eq1 icid.st_eq2)

end

class icategory = icatoid +
  assumes locality: "∂ i tt x = ∂ i ff y ⟹ DD i x y"
  and functionality: "z ∈ x ⊙⇘i⇙ y ⟹ z' ∈ x ⊙⇘i⇙ y ⟹ z = z'"

begin 

text ‹Every indexed category is a (single-set) category.›

sublocale icat: single_set_category "λx y. x ⊙⇘i⇙ y" "∂ i ff" "∂ i tt"
  apply unfold_locales
    apply (simp add: local.functionality)
   apply (metis dual_order.eq_iff icid.src_local_cond icid.st_locality_locality local.locality)
  by (metis icid.st_locality_locality local.iDst local.locality order_refl)

abbreviation ipcomp :: "'a ⇒ nat ⇒ 'a ⇒ 'a" (‹_⊗⇘_⇙_›[70,70,70]70) where
  "x ⊗⇘i⇙ y ≡ icat.pcomp i x y"

lemma iconv_prop: "X ⋆⇘i⇙ Y = {x ⊗⇘i⇙y |x y. x ∈ X ∧ y ∈ Y ∧ DD i x y}"
  by (rule antisym) (clarsimp simp: ims.conv_def, metis local.icat.pcomp_def_var)+

abbreviation "dim_bound k x ≡ (∀i. k ≤ i ⟶ fFx i x)"

abbreviation "fin_dim x ≡ (∃k. dim_bound k x)"

end

end