From Cakes, custard and category theory by Eugenia Cheng:
Category theory emphasises the context in which we’re thinking about things, rather than just the things themselves.
Category theory seeks to highlight the context you’re thinking about at that moment, to emphasise its importance and raise our awareness of it. The way it does it [..] is by emphasising relationships between things rather than just their intrinsic characteristics.
Consists of
f: A → B means:
dom f is A (aka source)cod f is B (aka target)C(A, B) is the collection of all arrows with
A as domain and B as codomain.
f ∈ C(A, B) means the same thing as
f : A → B.○.
f and g which has
cod f = dom g.g ○ f : dom f → cod gh ○ (g ○ f) = (h ○ g) ○ fobjects = formulas
arrows = proofs
objects = types of a functional programming language
Just functions?? Or are functions just a kind of morphisms??
a in a categoryaka monic.
An arrow f:B→C is monic if for any two arrows
g:A→B and h:A→B in the category,
f∘h = g∘h then g = h.
I guess we can say
∀(g h:A→B), (f∘g = f∘h) -> (g = h)
aka epic.
Sounds like a 'reversed' form of monomorphism..
An arrow f:A→B is epic if for any two arrows
g:B→C and h:B→C of the category,
g∘f = h∘f means g = h.
≤ₚ
Order preserving function. (Sort of like covariance in type theory??)
(M,⋅,e) A set M equipped with:
⋅ : (M, M) → M such that
⋅ is a relation from pairs of elements in
M to elements in M)f from a monoid to another.f : M -> M'
where M and M' are monoids.
(M, ⋅, e) and (M', ⋅', e')
Properties:
α
F ==> G
This means that α is a natural transformation of F to G.
An object 1 of a category C is a terminal object if from any object q∈C, there exists a unique morphism from q to 1.
A relationship between two functors.
F: C ⇆ D : U
'Sort of' means that the categories C and D
are 'kinda related'.
Then the functors F and U are said to be adjoint functors.
'a monoid in the category of endofunctors'. ʷ
Free monoad: Monad with no additional constraints
Monads aka triples: (T, η, μ)
A functor T and two natural transformations: η and μ
T: C -> C
η: A -> T A
μ: T² A -> T A
η μ
T A ----->---- T² A ----->---- T A
| | |
| | |
id v v μ v id
| | |
| | |
+----->----- T A -----<------+
Essentially, monad is a functor that comes with some additional rules (that supports some additional structure ⁸):
The flattening function μ is called join in Haskell.
-- Like μ
join :: Monad m => m (m a) -> m a
-- Like η
return :: Monad m => a -> M a| Category | Objects | Arrows |
|---|---|---|
| Set | Sets | Total functions |
| Pfn | Sets | Partial functions |
| Poset | Posets | monotone functions |
| Mon | Monoids | monoid homomorphism |
| Vect | Vector spaces | Linear transforms |
| Top | Toplogical spaces | Continuous functions |
| Grp | Groups | Group homomorphisms |
Diagrams in categories. Propreties of the category satisfied => the diagram commutes.
f'
X →-→-→-→-→-→-→-→-→-→- Z
↓ ↓
g'↓ ↓ g
↓ ↓
W →-→-→-→-→-→-→-→-→-→- Y
f
If this diagram commutes, it means that f∘g' = g∘f'.
Many computer science people prefer to say f;g instead
of g∘f (ie, by sort of reversing the order of
functions).
Another example:
succ-int
int →-→-→-→-→-→-→-→-→- int
↓ ↓
↓ ↓
toreal ↓ ↓ toreal
↓ ↓
↓ ↓
real →-→-→-→-→-→-→-→-→- real
succ-real
This says that
toreal(succ-int(int)) ≡ succ-real(toreal(int)).
When a functional language is described as a category, commutative diagrams can be used to assert the validity of program transformations in which the order of operations is permuted.
Products within a category. ie, with objects of the same category.
C
+-←-←-←-←-+-→-→-→-→-+
↓ ⇣ ↓
↓ ⇣ ↓
f ↓ ⇣ ⟨f,g⟩ ↓ g
↓ ⇣ ↓
↓ ⇣ ↓
A-←-←-←-A x B-→-→-→-B
π₁ π₂
(dashed arrows are assertions. Properties that should hold when the rest of the connections in the commutative diagram holds).
ie,
If
then
Written as one of these
Coproduct of two objects A and B is (A+B) along with two arrows ι₁ and ι₂.
If
then
ι₁ ι₂
A-→-→-→ A + B ←-←-← B
↓ ⇣ ↓
↓ ⇣ ↓
f ↓ ⇣ [f,g] ↓ g
↓ ⇣ ↓
↓ ⇣ ↓
+-→-→-→-→ C ←-←-←-←-+
Set theory instance of coproduct is disjoint-union.
It's like a union, where it's still possible to know which element came from which set.
(Kind of reminds one of a wedding with a prenuptial agreement.)
Eg:
A = {1,2,3}
B = {2,3,4}
A + B = {(1,A), (2,A), (3,A), (2,B), (3,B), (4,B)}
Forgetful functor:
Example:
U: Monoid -> Set
which sends:
(M,⋅,e) to M(M,⋅,e) → (M',⋅,e) to
M → M'hom(X,y): The set of all morphisms from object X to
object Y (where X and Y are objects in the same category)
X to object
Y in a category C.f ∈ hom(X,Y), f:X → YCorresponds to simply typed lambda calculus.
Given a monad (T, η, μ) on a category C,
T-algebra consists of objects of C acted upon by
T.
A T-algebra (x,h) where:
x ∈ Ch is an arrow T x -> x (structure map
of the T-algebra)(Remember, T is an endofunctor of type
C -> C where C is the category.)
T-algebras form a category known as Eilenberg-Moore
category (Cᵀ).
A relationship between two functors. In which case the two functors are known as adjoint functors (left adjoint and right adjoint).
Example for two categories C and D,
F: D -> C
G: C -> D
| Homotopy theory | Category theory | |
|---|---|---|
| Type | Spaces | Higher dimensional groupoids |
| Category | Object | Morphism |
|---|---|---|
| Set | Sets | Functions |
| Top | Topological spaces | Continuous functions |
| Group | Set | Group homomorphism |
| Poset | Set | Order preserving maps |
f: X → Y is an isomorphism if
there exists a morphism g: Y → X such that:
A functor F: C → D consists of:
F c ∈ D(f: c → c') ∈ C, there is a morphism
(F f: F c → F c') ∈ D