Theory RTSEnrichedCategory
section "RTS-Enriched Categories"
text ‹
The category ‹❙R❙T❙S› is cartesian closed, hence monoidal closed.
This implies that each hom-set of ‹❙R❙T❙S› itself carries the structure of an RTS,
so that ‹❙R❙T❙S› becomes a category ``enriched in itself''.
In this section we show that RTS-categories are essentially the same thing as
categories enriched in ‹❙R❙T❙S›, and that the RTS-category ‹❙R❙T❙S⇧†› is equivalent to
the RTS-category determined by ‹❙R❙T❙S› regarded as a category enriched in itself.
Thus, the complete structure of the RTS-category ‹❙R❙T❙S⇧†› is already determined by
its ordinary subcategory ‹❙R❙T❙S›.
›
theory RTSEnrichedCategory
imports RTSCatx RTSCat EnrichedCategoryBasics.CartesianClosedMonoidalCategory
EnrichedCategoryBasics.EnrichedCategory
begin
context rtscat
begin
sublocale CMC: cartesian_monoidal_category comp Prod α ι
using extends_to_cartesian_monoidal_category⇩E⇩C⇩C by blast
text ‹
The tensor for @{locale elementary_cartesian_closed_monoidal_category} is given by the
binary functor ‹Prod›. This functor is defined in uncurried form, which is consistent
with its nature as a functor defined on a product category. However, the tensor
@{term CMC.tensor} defined in @{locale monoidal_category} is a curried version.
There might be a way to streamline this, if the various monoidal category locales were
changed so that the binary functor used to specify the tensor were given in curried form,
but I have not yet attempted to do this. For now, we have two versions of tensor,
which we need to show are equal to each other.
›
lemma tensor_agreement:
assumes "arr f" and "arr g"
shows "CMC.tensor f g = f ⊗ g"
by simp
text ‹
The situation with tupling and ``duplicators'' is similar.
›
lemma tuple_agreement:
assumes "span f g"
shows "CMC.tuple f g = ⟨f, g⟩"
proof (intro pr_joint_monic [of "cod f" "cod g" "CMC.tuple f g" "⟨f, g⟩"])
show "ide (cod f)" and "ide (cod g)"
using assms by auto
show "seq 𝔭⇩0[cod f, cod g] (CMC.tuple f g)"
by (metis (no_types, lifting) CMC.ECC.seq_pr_tuple ‹ide (cod f)›
‹ide (cod g)› assms pr_agreement(1))
show "𝔭⇩0[cod f, cod g] ⋅ CMC.tuple f g = 𝔭⇩0[cod f, cod g] ⋅ ⟨f, g⟩"
using assms pr_agreement(1-2)
by (metis (no_types, lifting) CMC.ECC.pr_tuple(2) ‹ide (cod f)›
‹ide(cod g)› pr_tuple(2))
show "𝔭⇩1[cod f, cod g] ⋅ CMC.tuple f g = 𝔭⇩1[cod f, cod g] ⋅ ⟨f, g⟩"
using assms pr_agreement(1-2)
by (metis (no_types, lifting) CMC.ECC.pr_tuple(1) ‹ide (cod f)›
‹ide (cod g)› pr_tuple(1))
qed
lemma dup_agreement:
assumes "arr f"
shows "CMC.dup f = dup f"
using assms tuple_agreement by simp
sublocale elementary_cartesian_closed_monoidal_category
comp Prod α ι exp eval curry
using extends_to_elementary_cartesian_closed_monoidal_category⇩E⇩C⇩C⇩C
by blast
text ‹
We have a need for the following expansion of associators in terms of tensor and
projections. This is actually the definition of the associators given
in @{locale category_with_binary_products}, but it could (and perhaps should) be proved
as a consequence of the locale assumptions in @{locale elementary_cartesian_category}.
Here we already have the fact ‹assoc_agreement› which expresses that the definition
of associators given in @{locale category_with_binary_products} agrees with the version
derived from the locale parameters in @{locale cartesian_monoidal_category},
and ‹prod_eq_tensor›, which expresses that the tensor equals the cartesian product.
So we can just use these facts, together with the definition from
@{locale elementary_cartesian_category}, to avoid a longer proof.
›
lemma assoc_expansion:
assumes "ide a" and "ide b" and "ide c"
shows "CMC.assoc a b c =
⟨𝔭⇩1[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], ⟨𝔭⇩0[a, b] ⋅ 𝔭⇩1[a ⊗ b, c], 𝔭⇩0[a ⊗ b, c]⟩ ⟩"
using assms assoc_def assoc_agreement by simp
lemma extends_to_enriched_category:
shows "enriched_category comp Prod α ι
(Collect ide) exp ECMC.Id ECMC.Comp"
using ECMC.is_enriched_in_itself by blast
end
locale rts_enriched_category =
universe arr_type +
RTS: rtscat arr_type +
enriched_category RTS.comp RTS.Prod RTS.α RTS.ι Obj Hom Id Comp
for arr_type :: "'A itself"
and Obj :: "'O set"
and Hom :: "'O ⇒ 'O ⇒ 'A rtscatx.arr"
and Id :: "'O ⇒ 'A rtscatx.arr"
and Comp :: "'O ⇒ 'O ⇒ 'O ⇒ 'A rtscatx.arr"
begin
abbreviation HOM⇩E⇩C
where "HOM⇩E⇩C a b ≡ RTS.Rts (Hom a b)"
end
locale hom_rts =
rts_enriched_category +
fixes a :: 'b
and b :: 'b
assumes a: "a ∈ Obj"
and b: "b ∈ Obj"
begin
sublocale extensional_rts ‹HOM⇩E⇩C a b›
using a b by force
sublocale small_rts ‹HOM⇩E⇩C a b›
using a b by force
end
locale rts_enriched_functor =
RTS: rtscat arr_type +
A: rts_enriched_category arr_type Obj⇩A Hom⇩A Id⇩A Comp⇩A +
B: rts_enriched_category arr_type Obj⇩B Hom⇩B Id⇩B Comp⇩B +
enriched_functor RTS.comp RTS.Prod RTS.α RTS.ι
for arr_type :: "'A itself"
begin
lemma is_local_simulation:
assumes "a ∈ Obj⇩A" and "b ∈ Obj⇩A"
shows "simulation (A.HOM⇩E⇩C a b) (B.HOM⇩E⇩C (F⇩o a) (F⇩o b))
(RTS.Map (F⇩a a b))"
using assms preserves_Hom [of a b] RTS.arrD [of "F⇩a a b"] by auto
end
locale fully_faithful_rts_enriched_functor =
rts_enriched_functor +
fully_faithful_enriched_functor RTS.comp RTS.Prod RTS.α RTS.ι
section "RTS-Enriched Categories induce RTS-Categories"
text‹
Here we show that every RTS-enriched category determines a corresponding RTS-category.
This is done by combining the RTS's underlying the homs of the RTS-enriched category,
forming a global RTS that provides the vertical structure of the RTS-category.
The composition operation of the RTS-enriched category is used to obtain the
horizontal structure.
›
locale rts_category_of_enriched_category =
universe arr_type +
RTS: rtscat arr_type +
rts_enriched_category arr_type Obj Hom Id Comp
for arr_type :: "'A itself"
and Obj :: "'O set"
and Hom :: "'O ⇒ 'O ⇒ 'A rtscatx.arr"
and Id :: "'O ⇒ 'A rtscatx.arr"
and Comp :: "'O ⇒ 'O ⇒ 'O ⇒ 'A rtscatx.arr"
begin
notation RTS.in_hom ("«_ : _ → _»")
notation RTS.prod (infixr "⊗" 51)
notation RTS.one ("𝟭")
notation RTS.assoc ("𝖺[_, _, _]")
notation RTS.lunit ("𝗅[_]")
notation RTS.runit ("𝗋[_]")
text‹
Here we define the ``global RTS'', obtained as the disjoint union of all the
hom-RTS's. Note that types 'O and 'A are fixed in the current context:
type 'O is the type of ``objects'' of the given RTS-enriched category,
and type 'A is the type of the universe that underlies the base category ‹RTS›.
›