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.
=>): Map between two functorsF: X -> Y and G: X -> YF: X -> YF is limFlimF is an object in Y such that:
limF has a morphism to F x ??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)TL;DR: has associative operation with identity element
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 monad: 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 aVertical composition.
Consider the 2-category Cat.
Another name for horizontal composition in a 2-category ??
Category of categories at n levels.
Category of categories.
Cat
Cat (category of categories or 2-category), 2-morphisms are natural transformations between functors| 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 → Yhom(X,Y) may also be written as [X, Y]Corresponds 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ᵀ).
For example, for two categories C and D,
L: C -> D
R: D -> C
| 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') ∈ DObject: sets
Arrows: relations
Identity: aRa = {(a,a) | a ∈ A}
Composition:
Associativity of composition
It's the arrows that really matter!
Functor
Some categories
Slice category 𝐂/C of a category 𝐂 over an object C
C = base object
f : X -> C
f': X' -> C
a : X -> X'
f'∘a = f
A monoid M(A) is generated from a set A.
Wikipedia: A monoid is free if it is isomorphic to the free monoid on some set.
Notations:
|N| is the set underlying the monoid N.A*: Free monoid on a set AGiven:
i: A -> |M(A)|
A the generating setNf: A -> |N|then there is a unique monoid homomorphism f̅: M(A) -> N such that:
|f̅|∘i : A -> |N|DBT: 'monoid is a category with only one object'. How?
Hom-set of a category: set of morphisms between two given objects of the category:
A functor does this:
Faithful functor (injective):
Full functor (surjective):
Fully faithful functor = bijective
Categories:
—
Is ℕ and ℤ isomorphic ???? No, I guess. But why?
Every monoid is like an untyped program.
Groupoid = category where every morphism is an isomorphism
Forgetful functor: functor that drops some properties of the domain category
Sub-category: Restrict to some objects and morphism of parent category while still remaining a category
Order theory terms
Scott domain ???
Concrete category: One that can be defined in terms of sets and functions over sets.
Cayley representation of a group/category
Dual of a category C: Same objects as C, but direction of arrows is reversed
Atomic boolean algebra: ???
Complete boolean algebra: ???
Universal algebra: Study of algebras themselves. Not just instances of algebras.
Pointed set: Set together with an element that set called the base point.
Base map: Map functions that map between pointed sets
Small category: Collection of objects is a set, collection of arrows is a set
Cat: category of small categories
Locally small category
Hom(X, Y) = {f ∈ ℂ | f: X → Y} is a setA rule of thumb??
Baez, J. and Stay, M., 2011. Physics, topology, logic and computation: a Rosetta Stone (pp. 95-172). Springer Berlin Heidelberg.