-
Notifications
You must be signed in to change notification settings - Fork 0
TheCatsters Metric Spaces Enriched Categories
- Growing abstraction - generalize metric space to Enriched category
| metric space | generalization |
|---|---|
| d(a,b) + d(b,c) >= d(a,c) | Hom(a,b) x Hom(b,c) -*-> Hom(a,c) |
| 0 >= d(a,a) | {42} --id--> Hom(a,a) |
Given
- C is a category
- we have a collection of objects Ob(C)
- for all a,b ∈ Ob(C) we have homset Hom(a,b) ∈ Ob(Set)
- for all a,b,c ∈ Ob(C) exists Hom(a,b) x Hom(b,c) -*-> Hom(a,c)
- for all a ∈ Ob(C) exists {*} -id-> Hom(a,a) such that
- associativity condition
- unit condition where -id-> and -*-> are morphisms in set
We can generalize Set to monoidal category (V, ⊗, 1):
Given C is a V-category (category enriched with monoidal category (V, ⊗, 1))
- we have a collection of objects Ob(C)
- for all a,b ∈ Ob(C) we have homset Hom(a,b) ∈ Ob(V)
- for all a,b,c ∈ Ob(C) exists composition: Hom(a,b) ⊗ Hom(b,c) -*-> Hom(a,c)
- for all a ∈ Ob(C) exists 1 -id-> Hom(a,a) such that
- associativity condition
- unit condition
-id-> and -*-> are morphisms in V
Examples:
- when V is category of vector spaces we get linear category - Ob(V) are vector spaces, Hom(a,b) ⊗ Hom(b,c) is bilinear map
- when V is category of abelian groups we get additive category
- when V is category where objects are non negative numbers or infinity ∈ [0,∞] morphisms are Hom(a,b) is one element when a >= b and empty set otherwise and V is monoidal category (R+,+,0) we get generalized metric space
Metric space generalized in sense of Lawvere
Given C is a R+ category (category enriched with monoidal category (R,+,0))
- we have a collection of objects Ob(C)
- for all a,b ∈ Ob(C) we have homset Hom(a,b) ∈ [0,∞]
- for all a,b,c ∈ Ob(C) exists composition: Hom(a,b) + Hom(b,c) >= Hom(a,c)
- for all a ∈ Ob(C) exists 0 >= Hom(a,a) (since Hom(a,a) >=0 so 0 == Hom(a,a) ) such that (vacuously true)
- associativity condition
- unit condition
Examples
- we have villages as objects and Hom(a,b) is time needed to get between village a and b
- cost of travel from town a to b
Generalization because:
- it is not symmetric (route in the mountains) d(a,b) != d(b,a)
- it is possible that d(a,b) = 0 when a != b
- allows for ∞ distance
V-Functor Let C and D be categories enriched with V and F is a functor F: C -> D
- a set of maps F: Ob(C)-> Ob(D)
- for every a,b ∈ C we have morphism (in D) F: Hom(a,b) -> Hom(F(a),F(b)) that commute with composition
Example
- when V is R+ we have Hom(a,b) >= Hom(F(a),F(b)) so it is a map that is not expanding
TODO Enriched natural transformations
- A tale of two functors or: How I learned to stop worrying and love data and control, tweag.io (blog post)
summary:
Functor works on data types (do not preserve linear types - use function multiple times to map list).
Functor applies an effect to a value (preserver linear types - apply function to every element of the list once).
Enriched category definition is definition of category where we replace Homset with object from some category. (In general, in CT we replace Sets with Categories.)
All symmetric monoidal closed categories are enriched in themselves.
An enriched functor is a functor that respects the enrichment.
The category of types and functions is symmetric monoidal closed. So it is enriched in itself.
In the category of types and functions, enriched functor and functor are the same.
The linear function uses its argument only once.
The category of types and linear functions is symmetric monoidal closed. So it is enriched in itself.
Some functors are enriched, others are not like: A => (A,A).
TODO prerequisites: strength of functor, strength of monad,
-
Enriched Categories - Bartosz Milewski, Bartosz Milewski's Programming Cafe (blog post)
-
Profunctor optics, a categorical update - Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Roman arxiv (pdf)
-
Metric spaces, generalized logic and closed categories - F. W. Lawvere TAC reprint (pdf)
-
Mike Stay, Lucius Gregory Meredith
TODO prerequisites: monads, Lawvere theory, 2-Category, λ-calculus, universal algebra