Category theory

https://arxiv.org/pdf/1803.05316 https://www.logicmatters.net/2020/01/09/programming-with-categories/ https://github.com/pcapriotti/agda-categories/blob/master/category/category/core.agda

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.

Something basic

General

Limit of a functor

Category

Consists of

Example: Set

  • objects = sets
  • arrows = (total) functions between sets
  • identity arrows = identity functions

Example: Categorical logic

  • objects = formulas

  • arrows = proofs

  • objects = types of a functional programming language

More examples

  • Category 0: has no objects and no arrows.
    • Identity and associativity laws vacuously satisfied.

Morphism

Just functions?? Or are functions just a kind of morphisms??

Monomorphisms

aka 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)

Epimorphisms

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.

Partial ordering

≤ₚ

Monotone function

Order preserving function. (Sort of like covariance in type theory??)

Monoid

(M,⋅,e) A set M equipped with:

TL;DR: has associative operation with identity element

Monoid homomorphism

  • A function f from a monoid to another.
  • Homomorphism => properties preserved.

f : M -> M'

where M and M' are monoids.

(M, ⋅, e) and (M', ⋅', e')

Properties:

  • f(e) = e'
  • f(x⋅y) = f(x)⋅'f(y)

Natural transformation

   α
F ==> G

This means that α is a natural transformation of F to G.

Natural isomorphism

Terminal object (1)

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.

Adjunction

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.

Monad

'a monoid in the category of endofunctors'. ʷ

Free monad: Monad with no additional constraints

Monads aka triples: (T, η, μ)

        η               μ
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

Internal vs external binary operation

Horizontal vs vertical composition

Vertical composition.

Consider the 2-category Cat.

Whiskering

Another name for horizontal composition in a 2-category ??

n-category

Category of categories at n levels.

2-category

Category of categories.

  • Example is Cat
    • objects: categories
    • morphisms: functors
    • functors: natural transformations

k-morphism

A table

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

Diagram

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.

Product

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

Coproduct

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 ←-←-←-←-+

Disjoint-union ʷ

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)}

Functor

Forgetful functor:

Example:

U: Monoid -> Set

which sends:

String diagrams

Hom-set

Closed Cartesian Category (CCC)

Corresponds to simply typed lambda calculus.

T-algebra ʷ

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:

(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ᵀ).

Adjunction

For example, for two categories C and D,

L: C -> D
R: D -> C

Extension

New terms

Some 'standard' categories

References

Category theory vs Homotopy theory

Homotopy theory Category theory
Type Spaces Higher dimensional groupoids

Reboot

Category theory in context

Category Object Morphism
Set Sets Functions
Top Topological spaces Continuous functions
Group Set Group homomorphism
Poset Set Order preserving maps

A functor F: C → D consists of:

Awodhey

Rel is a category

  • Object: sets

  • Arrows: relations

  • Identity: aRa = {(a,a) | a ∈ A}

  • Composition:

    • R: A -> B
    • S: B -> C
    • S∘R: A -> C = {∃b∈B, aRb ∧ bSc | a∈A, c∈C}

  • Associativity of composition

    • H∘(G∘F) = (H∘G)∘F

Continuing..

It's the arrows that really matter!

Functor

  • F:C->D gives a 'picture' of C in D

Some categories

  • Product category
  • Dual or opposite category of another category
    • Objects = same, but arrow direction reversed
  • Arrow category
  • Co-slice category

Slice category (𝐂/C)

Slice category 𝐂/C of a category 𝐂 over an object C

  • Objects = arrows of 𝐂 whose codomain is in C.
  • (f:X -> C) (f': X' -> C) ∈ Arrow(𝐂), (g: X -> X') ∈ Arrow(𝐂/C),

C = base object

f : X  -> C
f': X' -> C
a : X  -> X'

f'∘a = f

Free monoid

Universal mapping property (UMP)

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.

  • DBT: I guess that's because there is only one such monoid? Due to UMP?

Notations:

  • |N| is the set underlying the monoid N.
  • A*: Free monoid on a set A

Given:

  • a function from a set A to a monoid M(A): i: A -> |M(A)|
    • DBT: is A the generating set
  • a monoid N
  • a function f: 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?

PS1

Background

Hom-set of a category: set of morphisms between two given objects of the category:

  • Hom(X, Y)

A functor does this:

  • F: C -> D
  • F: HomC(X, Y) -> HomD(F(X), F(Y)), where X,Y∈C

Faithful functor (injective):

  • Functor that is injective on hom-sets (ie, 1-to-1)
  • No morphism2 is mapped onto from multiple morphism1-s.

Full functor (surjective):

  • Functor that is surjective on hom-sets (ie, onto)

Fully faithful functor = bijective

1

  • Example of a category and functor from CS or math:

Categories:

  • STLC (Church or Curry)
    • Arrows = functions
      • Identity = identity function
      • When you take the arrow, function is applied
    • Objects = terms
  • UTLC
  • Functor with domain as STLC = type erasure to get UTLC from STLC
  • Functor with codomain as STLC = from category of sml to STLC

—

Is ℕ and ℤ isomorphic ???? No, I guess. But why?

3

Every monoid is like an untyped program.

  • skip = identity
  • sequence = operation

Resources

Glossary