3.1 Examples of categories, orders, monoids

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

There is an arrow between any two objects

Thin Category #card #bidirectional

Every Hom-set is an empty set or a singleton set

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

1

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

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

1

any two functions are composable

corresponds to weak typing