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
relationship/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
Category with one object
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
associative, with a unit element; not necessarily commutative
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