1.1 Motivation and Philosophy
1.2 What is a category?
2.1 Functions, epimorphisms
2.2 Monomorphisms, simple types
Injective and surjective = bijection
Bijection
injective and surjective
reversible
3.1 Examples of categories, orders, monoids
Category with no objects
Initial object in Category of Categories
Category with one object
Terminal object in Category of Categories
Hom-set #card #bidirectional
the set of arrows between two objects in a category
this is a traditional set from Set Theory
Arrows, morphisms can be thought of as relations, like $$\leq$$
Orders
Pre-order #card #bidirectional
0 or 1 arrows (relations) between any two objects
Can have a loop
In a way, the most basic category
Partial order #card #bidirectional
Pre-order but with no cycles
Same as a directed acyclic graph
Total Order
There is an arrow between any two objects
Thin Category #card #bidirectional
Every Hom-set is an empty set or a singleton set
isomorphism -> Pre-order
If there is an arrow between two objects, those objects have a relation
Defines a relation
Thick Categories #card #bidirectional
Hom-set can have multiple arrows
If there is an arrow between two objects those objects have a relation
Every arrow between two points can be considered a different “proof” of a relation between those two points
Defines a proof-relevant relation
Becomes relevant in Homotopy Type Theory
Monoid #card #bidirectional
Can have many morphisms
Known as a sort of “pre-group” in Group Theory
Monoid in Set Theory #card #bidirectional
defined as a set of elements
some operation for that set
can take in multiple elements from the set and return one from the set
has to be defined for all elements of the set
one element is the Unit element
Commutative and Associative
Examples
multiplication, Unit element = 1
string concatenation, Unit element = "" (empty string)
appending lists
Monoid in Set Theory == Monoid in Category Theory
Typing
Types in Category of Types #card #bidirectional
corresponds to strong typing in programming
to compose two functions, the result of the first function has to be the same type as the input of the second function
Types in a Monoid #card #bidirectional
any two functions are composable
corresponds to weak typing
3.2 Kleisli Category
4.1 Terminal object and Initial object
4.2 Products
5.1 Coproducts and sum types
5.2 Algebraic data types
6.1 Functor
6.2 Functor in programming
7.1 Functoriality, bifunctors
7.2 Monoidal categories, Functoriality of ADTs, Profunctors
8.1 Function objects, exponentials
8.2 Type algebra, Curry-Howard-Lambek Isomorphism
9.1 Natural transformations
9.2 bicategories
10.1 Monads
10.2 Monoid in the category of endofunctors
from Bartosz Milewski Category Theory Lectures
exploring Universal Constructions
void = initial object = in SET Category, empty set = in logic, proving “false”
initial object = for every point in a category there is one and only one arrow from the initial object to the point
identity exists, void -> void
nothing can return void
anything that takes in a void can return any type, void -> a
unit = terminal object = () = in SET Category, set with one element = in logic, proving “true”
terminal object = from every point in a category, there is one and only one arrow to the terminal object
two terminal objects are always have a uniquely ismorphic = only one way to isomorph between the two
you can return a unit from anything, a -> ()
can use unit to define the element of a set, one :: () -> int, two :: () -> int
as many unit -> t functions exist as elements in the type t
unit -> t
instead of talking about elements in category theory, we can talk about the function from unit
bool = in SET Category, set with two elements
TODO how are groups, rings, fields defined as a category?