Category Theory for Programmers: Notes

ct_notes.txt

CATEGORY THEORY FOR PROGRAMMERS

Category Theory 1.1: Motivation and Philosophy 
https://www.youtube.com/watch?v=I8LbkfSSR58&index=1&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Composability, Abstraction, Reusability

Category Theory is a higher-level language.
Not a practical, executable language.

CT unifies over Mathematics
Curry-Howard-Lambek correspondence
* Logic <-> TypeTheory <-> CT
https://wiki.haskell.org/Curry-Howard-Lambek_correspondence
The Curry-Howard-Lambek correspondence is a three way isomorphism between types (in programming languages), 
propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps 
programs (functions in Haskell) to (constructive) proofs in logic (and vice versa).


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 1.2: What is a category? 
https://www.youtube.com/watch?v=p54Hd7AmVFU&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=2

Abstraction: Get rid of the details; things that are different at lower level 
             may be identical at higher levels of abstraction
Composition: Combine small parts to build larger structures
Identity:

(Homotopy type Theory: What things are identical? What are isomorphic?) 

CT encompasses Composition and Identity

Definition: Category
    A bunch of objects and morphisms (arrow)

Definition: Object
    A primitive of CT. It has no properties!
    "Names for the ends of arrows"
    
Definition: Morphism (a.k.a. Arrow)
    Goes from one object to another
    
Definition: Composition
    If there is an arrow A -> B and an arrow B -> C then there is an arrow A -> C
    A -> C is the `composition` of A -> B and B -> C
    Composition is *associative*: h . (g . f) = (h . g) . f

Definition: Identity
    For every object, there is an Identity arrow A -> A
    If f is an arrow A -> B and id_B is the Identity arrow of B, then
    id_B . f = f           Left Identity
    likewise g . id_A = g  Right Identity
    
In Programming:
    Objects are Types
    Morphisms are Functions

What are Types? Sets of values
What are Functions? Functions on Sets of values


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 2.1: Functions, epimorphisms 
https://www.youtube.com/watch?v=O2lZkr-aAqk&index=3&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_
    
Semantics:
Operational = How expressions/statements can be transformed
Denominational = Map expressions into another domain, e.g. mathematics

Partial functions = functions that are not defined for all arguments of its type
Total functions = are defined for all arguments of its type
In programming, a function is "pure" if you can memoize it.

How can we use functions in our category "set" which contains (sets, function)
* Functions have direction -- unlike a Relation
* Function may be many-to-one or one-to-one, but never one-to-many.
* domain: Set of inputs
* codomain: Set of all possible outputs
* image: Set of actual outputs (may be a subset of the codomain)

Is the function invertible? Usually it is *not*.
a function f :: a -> b *does not imply* there is a function g :: b -> a

if g . f = id then f and g are invertible; this implies f . g = id

An invertible function is called an isomorphism. This is the definition in any category.
Notice that the definition is in CT terms, i.e. composition and identity.

Why are most functions not isomorphic?
* A function may collapse elements of the codomain (e.g. isEven maps numbers to T|F) : ABSTRACTION
* A function's image is a strict subset of the codomain. : MODELING

A function that is not invertible increases entropy.

injective function: every x maps to a unique y
surjective function: every y is mapped to by an x. forall y . exists x s.t. y = f x

An isomorphism is both injective and surjective. That is the set/Latin.

In CT:

monomorphism = injective
epimorphism = surjective

Epimorphism (CT definition)
* f is an epimorphism from a -> b if for every other object C in the whole category, 
  and every pair of morphisms b -> c (e.g. g1 and g2) if g1 . f == g2 . f => g1 == g2
This definition works for any category. In Set context, it is a surjection.
Proven with "post-composition" (add category C after)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 2.2: Monomorphisms, simple types 
https://www.youtube.com/watch?v=NcT7CGPICzo&index=4&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Monomorphism 

Start with something *not* a monomorphism. 
e.g. a non-injective function that maps two different xs into the same y.

forall c . forall g1,g2 :: c -> a if f . g1 == f . g2 => g1 == g2

Epimorphism and monmomorphism is defined for every category

----

Simple sets

In Haskell: 
* Empty Set corresponds to Void type
* Singleton Set is () (Unit type)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 3.1: Examples of categories, orders, monoids 
https://www.youtube.com/watch?v=aZjhqkD6k6w&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=5

Simplest possible category: zero objects, zero morphisms
Then: 1 object, Id Arrow

In general, we can start with a graph. (n.b.: Not every graph is a category!)
You can add arrows to any graph until it *is* a category.
1. Identity: For every node, add Id Arrow
2. Composition: For every pair of arrows a -> b, b -> c, add arrow a -> c
3. Associativity also must be satisfied

Free Construction of a category (from a graph). Unconstrained except by properties above.

Orders:
A category where arrows are *not* functions
An arrow represents a relation, viz. <=
in this context a -> b means a <= b

Preorder:
A relation that satisfies the minimum of conditions
* Composable. If a < b && b < c then a < c
* Associative. 
* Identity. a <= a duh. Reflexivity.
* There may or may not be an arrow betwee two objects.
* May not have multiple arrows from one object to another. (In Total Order there is an arrow between any two arrows.)
* Thin Category corresponds to a Preorder, and Preorder corresponds to a This category.

Note that a Thin Category is both an epimorphism and a monomorphism. But it is not invertible.

Most general category: A Preorder that is *thick*. Multiple arrows a -> b. 
Each arrow represents a different proof of the relation.
A "proof-relevant relation"


Hom-set: 
A set of arrows C(a, b) (or C(a, a))
If C is a category containing objects A and B then Hom(A,B) is the collection of all morphisms from A to B:
Hom(A,B) = {f∈C | f: A -> B }
where: A = Dom(f) and B = Cod(f)

Partial Order:
No loops!
If there is an arrow a -> b, then there is not an arrow b -> a
Corresponds to a directed acyclic graph.
Some objects are not comparable

Partial Order is also not invertible -- by defintion, you cannot have both a -> b and b -> a


Total Order:
There is an arrow between any two objects

Back to single-object category. 
The single object may have several arrows. 
Composable: Obviously. Trivially.

That is a Monoid! A single object and however many arrows you want.

Monoid is known from Algebra & Set theory: 
A set of elements and a (total) binary operator.
* One element in the set is "unit" (a.k.a. identity element, or "empty")
    exists e . forall a : e `op` a == a `op` e == a
* Associativity. 
*   (a `op` b) `op` c == a `op` (b `op` c)
     
Examples: Natural numbers with (+, 0)
          Natural numbers with (*, 1)
          Strings         with (concat, "") (n.b. this is not symmetric!)
          Lists           with (concat, []) (n.b. this is not symmetric!)

Hom-set of Monoid is M(m, m), i.e. set of arrows m -> m

Monoid can be seen as the basis of multiplication -- M(m, m) implies other 
arrows may be produced as the product/composition of m -> m

In a monoid, any two functions are composable! 
Corresponds to "weakly typed" language, i.e. there is only one type


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 3.2: Kleisli category 
https://www.youtube.com/watch?v=i9CU4CuHADQ&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=6&spfreload=1

Consider subset relation. Is this Order? Preorder?
* Identity: Every set is a subset of itself (reflexivity)
* Composability: if a `subset` b and b `subset` c then a `subset` c

OK, so it is at least a Preorder.

* There are no loops -- if a `subset` b and b `subset` a then a == b
So it is a Partial Order.

Not a Total Order: There may be disjoint subsets, e.g.

Kleisli Category
Suppose we have a lib of functions.
Business comes up with a new requirement: Every function must have an audit trail.
Task: Go and rewrite the lib to satisfy this requirement.

Naive solution: Global String log

Later ...
Business requires this to work in a multithreaded environment. ummm ....

Now what?

Starts by redifining simple functions to return pair of ('a returnValue * string logText)
Build a compose function:

compose (a -> b) -> (b -> c) -> (a -> c) // this looks familiar. 

Have to extend that for pairs:

compose (a -> (b, p1)) -> (b -> (c, p2)) -> (a -> (c, p1 + p2))

Hmmm. Is there a category here? 
* Composition: Check. That is the point
* Associativity: Yes, regular function composition and string concatenation are both associative.
* Identity: (a, "") -> (a, "")

Hey! That's a monoid!
This is a category with types as objects and functions a -> (b, String) as morphisms.

This is the Kleisli category. a -> (b, x) is a Kleisli arrow.

These arrows are composable because this embellishment is a monad. watch out.
Don't fear the Monads. Just a special way of composing functions.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 4.1: Terminal and initial objects 
https://www.youtube.com/watch?v=zer1aFgj4aU&index=7&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Recap Kleisli Category
* Start with category C
* trying to build Kleisli category K
* For every object a in C, there is an object a in K
* The *arrows* are not the same. For every arrow a -> m b in C, there is an arrow a -> b in K
* Therefore, Identity in K is a -> m a in C (looks like flatMap ...)
  And that m a has to be `unit` with respect to the composition in K
* K must also be associative
* So K has Identity, Composability, and Associativity.
* uh-oh, that's a monad

-----
Back to Set theory vs. Catageory "Set"

Set Theory:   "Sets are things that have elements that we can use to define things."
Set category: "We have arrows between objects. We don't know about sets or elements. We know composition."

Rediscover/redfine things in terms of arrows under composition. 

Method for doing this rediscovery: Universal Construction.
* Define a pattern (pattern: some combination of objects and arrows)
* Find everything that matches this pattern
* Order the matches
* The top match is it

Example 1: Singleton set
* A singleton set has an arrow from every other object in the category: a -> ()
   ... including a function from Void -> () (but you can't call it)
   This doesn't give us much; almost all sets have this property
     (except non-empty set to empty set)
* The difference is that there is a *unique* arrow from any set to the singleton set.
* `unit` is a "Terminal object". All arrows converge on it.
* A terminal object is an object in a category s.t.
    1. forall a . exists f :: a -> ()
    2. forall f :: a -> (), g :: a -> () => f == g

    Terminal object example: Order
    * The arrows in N e.g. represent <=
    * There is no "largest" n in N
    * hence, there is no terminal object in this category over N
    
Example 2: Empty set
* Can be defined in terms of outgoing arrows.
* Void -> a (`absurd`)
* "You cannot prove that I don't have this function"
* Initial object: Has a unique outbound arrow to every other object (incl. itself, i.e. Identity)

When a category has an Initial or Terminal object, then ...
* Any path to a Terminal object can be shrunk to a unique arrow
* Likewise in the opposite direction for Initial object

Arrows can be shown to be equal, by comparing their ends
What does it mean for objects to be "equal"? Dunno!
We can say they are isomorphic (or not)  f::a -> b and g::b -> a, and composition = Identity

Terminal object is unique up to an isomorphism
(if you have two terminal objects, then they describe a unique isomorphism)

Proof
Suppose we have two Terminal objects a and b
By definition there is a unique arrow from every object
Therefore there are unique arrows f::a -> b and g::b -> a
let h = Identity of a (similarly for Id b)
By definition, h must be unique
note that g . f = Id a and f . g = Id b (this defines the isomorphism)
Therefore, this is a unique isomorphism -- there cannot be any other arrows because a and b are terminal.

Example Universal Construction
1. Pick a pattern.
   - A single object.
2. Find all the matched
   - All objects in the category
3. Order them (maybe partial)
   - a is better than b if there is a unique arrow b -> a
4. What is the best fit? 
   - The object b at the top of the arrows, viz. the terminal object

Note you can find the initial object by inverting the sense of the comparison


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 4.2: Products 
https://www.youtube.com/watch?v=Bsdl_NKbNnU&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=8

One more note on terminal objects: What about outgoing arrows from terminal object?
There usually are outgoing arrows.

Reversing the arrows of the Construction reveals a deeper truth:
Every construction implies another construction with the arrows reversed

For every category, you can create another category with the arrows reversed.

Category C = f :: a -> b => C^{op} = f^{op} :: b -> a
             g :: b -> c             g^{op} :: c -> b
             g . f                   g^{op} . f^{op}

so (g . f)^{op} = g^{op} . f^{op}

It's Composable. 
And since Id^{op} = Id, we have the "op" category.

Cartesian Product

Set definition: forall x in X, y in Y => (x, y)
Category definition (in terms of arrows/functions): 
* Projection: for every Cartesion Product A x B, there are two arrows fst and snd
* All we know is we have an object, and an arrows going from it to a and another going to b

Now let's rank/order patterns that match

                    c'
                   /|\
               p' / | \ q'
                 /  |m \
                v   v   v
                a<--c-->b
                  p   q


Compare candidates c and c'. 
* c has arrows p and q to a and b, resp.
* c' has arrows p' and q' to a and b, resp.
* (p' p', q, and q' are "projections")
* c is better than c' if there is a unique morphism (arrow) m from c' to c
* p . m = p'
* q . m = q'
* The factors of p' are p and m
* The factors of q' are q and m
* p' and q' share a common factor, so we can factor it out and get c


Let c = (Int, Bool)
Let c' = Int

The morphism m is  :: Int -> (Int, Bool)
                   :: x   -> (x, Bool)

Let c = (Int, Bool)
Let c' = (Int, Int, Bool)
p' :: (Int, Int, Bool) -> Integer
p' x _ _ = x
q' :: (Int, Int, Bool) -> Bool
q' _ _ b = b

The morphism m is :: (x, y, b) -> (x, b)


Define Product with arrows & objects (Categorical Product)
A product of two objects a and b is a third object c with arrows p :: c -> a and q :: c -> b
For any other c' (p' :: c' -> a and q' :: c' -> b) there is a unique morphism m :: c' -> c
that factorizes the two projections (p' = p . m and q' = q . m)

c is the product of a * b


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 5.1: Coproducts, sum types 
https://www.youtube.com/watch?v=LkIRsNj9T-8&index=9&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_


Coproduct: Dual of the Product; take the Product and reverse the arrows. a.k.a "Injection"

           i   j
         a-->c<--b
         \   |   /
       i' \  |m / j'
           \ | /
            vvv
             c'

Observe that:
j' = m . j 
i' = m . i

Note that the order of the composition is reversed as well.

How do I use it?
Product is Cartesian Product, Tuples, Pairs. What is a Coproduct?

Like union of two disjoint sets

Or you could "tag" elements from a and b in c and get a Discriminated Union, a.k.a. Tagged Union, Variant, Sum type.
Used to hold a value that may take on several different, but fixed types.

Example: 
Boolean = True | False : Tagged Union. A value is one or the other.

Contrast with
Tuple = (Int, Bool) : Product type. 

Another Example: Enum is a Tagged type

Another Example: 
data Either a b = Left a | Right b

takes two types (a and b) and can be constructed two ways (as above). 
n.b. Left/Right correspond to i/j in the Coproduct diagram.

Product types + Sum types are the foundation of the type system.

Why are they called Product & Sum?
* Product is like Cartesian pairs;
* Sum is like ... addition?


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 5.2: Algebraic data types 
https://www.youtube.com/watch?v=w1WMykh7AxA&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=10

Multiplication:
* Monoid: associative, closed binary operation, unit element

How does this translate to types?

Associativity:
((a, b), c) /= (a, (b, c)) NOT THE SAME

However, all the info is there, so you can define a function e.g.:
assoc ((a, b), c) = (a, (b, c))
Product types are associative in this sense

n.b. that since they are associative up to isomorphism, these are essentially the same:
((a, b), c) == (a, (b, c)) == (a, b, c)

Unit element: Unit Type
Again: (a, ()) NOT THE SAME AS a, but isomorphic with these helpers:
munit (a, ()) = a   {- munit = fst -}
munit_inv x = (x, ())

Product types are isomorphic to multiplication

Product types are "symmetric up to isomorphism" :
(a, b) is isomorphic to (b, a) : 

swap :: (a, b) -> (b, a)
swap p = (snd p, fst p)

So... Sum Types
Also monoidal:
Symmetric up to isomorphism, e.g. Either a b ~ Either b a
Associative up to isomorphism, e.g. data Triple a b c = Left a | Middle b | Right c
    Ordering does not matter!
Unit of Sum: Void type => Either a Void ~ a
                                 a + 0 == a

Combine Sum & Product types

a * 0 = 0
(a, Void) ~ Void

Distributive:
a * (b + c) = a * b + a * c

Also true (up to isomorphism), e.g.:
(a, Either b c) ~ Either (a, b) (a, c) 

Product & Sum together forms a Semiring (a.k.a. Rig, a "Ring without the 'n'")
For a true ring we need an inverse operation.

Some isomorphisms:

Bool : True | False        ~ 2 = 1 + 1
Maybe a : Nothing | Just a ~ 1 + a
          also Either () a           

Algerbraic equations

l(a) = 1 + a * l(a)

l(a) - a * l(a) = 1
l(a)(1 - a)     = 1
l(a)            = 1/(1 - a)
                = n=0->infinity sum a^n = 1 + a + a*a + a*a*a + ...
                = data List a = Nil | Cons a (List a)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 6.1: Functors 
https://www.youtube.com/watch?v=FyoQjkwsy7o&index=11&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Functor is a mapping from one category to another
How do we define mapping between categories?
Map objects (e.g. sets in a small category) => Functions
   - But functions are mapping between sets, and sets have no *structure*
   - We want to find a way to map while preserving structure
   - Discrete Category: No arrows except Id. Corresponds to a Set (objects are elements 
     in the Set); models "structurlessness".
   - Any category that is not Discrete has structure, i.e. other arrows
   - Therefore: We need to be able to map the arrows as well!

            F
   a ----------------> F a
   |                    |
 f |                    | F f  (mapping the morphism f)
   |                    | 
   v                    v
   b ----------------> F a

 Hom-set:             Hom-set
 C(a, b)             D(F a, F b)

So we need a function that maps objects
       and a function that maps Hom-sets
To preserve structure, we must preserve composition as well
e.g. If we have a morphism g :: b -> c, we can also add an arrow g . f :: a -> c
     We must then have F g :: F b -> F c and F g . F f :: F a -> F c
     And: F (g . f) == F g . F f
     And: F Id_a == Id_{F a}

And that is a Functor.
A mapping of objects and morphisms that preserves composition.
Any morphism in the source category must have an associated arrow in the target category.

Faithful Functor: Injective on hom-sets
Full Functor: Surjective on hom-sets
n.b.: Objects are not part of the definition of Faithful/Full. Objects may be squeezed 
      and still be Faithful or Full.

Constant Functor: Maps all objects into one, and all morphisms into Id (e.g. \delta c)
Endofunctor: A mapping of objects/morphisms into the same category

What does this have to do with programming?

Objects   => Types
Morphisms => Functions

Mapping of types: Type Constructor (Parameritzed Data Type, Generic Type, Template Type, etc.)
                  Maybe a: maps a -> Maybe a
Mapping of functions: 

            F
   a ----------------> Maybe a
   |                    |
 f |                    | fmap f  (mapping the morphism f)
   |                    | 
   v                    v
   b ----------------> Maybe a

Transforms (a -> b) into the lifted context
fmap :: (a -> b) -> (Maybe a -> Maybe b)
fmap f Nothing  = Nothing
fmap f (Just x) = Just (f x)

Theorems for Free: read this paper later
From the type of a polymorphic function we can derive a theorem that it satisfies. 
Every function of the same type satisfies the same theorem. This provides a free 
source of useful theorems, courtesy of Reynolds' abstraction theorem for the 
polymorphic lambda calculus. 
http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html
http://homepages.inf.ed.ac.uk/wadler/papers/free/free.dvi


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 6.2: Functors in programming 
https://www.youtube.com/watch?v=EO86S2EZssc&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=12&spfreload=1

Is Maybe a lawful functor?
[x] Maps types (objects)
[x] Maps functions (morphisms)
[?] Preserves composition
[?] Preserves identity

Type system cannot encode preservation of composition/identity.
But, we may still be able to prove Maybe preserves structure.

Equational Reasoning: inline & refactor to show semantics are the same

1. Claim: 
   fmap id = id
   Proof:
   fmap id Nothing  = Nothing 
                    = id Nothing
   fmap id (Just x) = Just (id x) 
                    = Just x
   id (Just x)      = Just x

2. Claim: 
   fmap (g . f) = (fmap g) . (fmap f)
   This follows from parametric polymorphism & proof of id law. "Theorem for Free"

* Usually when you define a functor with ADTs, it will satisfy these laws (in Haskell)

How do we define a functor in general in Haskell?

Lifting: f gets "lifted" into Maybe context

          fmap f 
 Maybe a --------> Maybe b
       ^           ^
       |           |
       |           |
       |           |
       a --------> b
            f

ad hoc polymorphism: Typeclasses
* Define a family of types that share a common interface (OO anyone?)
* Example:
    class Eq a where 
      (==) :: a -> a -> Bool
  "There is an operator `==` that takes two 'elements' of type a and produce a Boolean."
  This is just a signature -- different types can implement for their needs
  n.b. Eq is parameterized by type "a"

Functor is not parameterized by types, it is a type *constructor*. e.g., Maybe takes a type, produces a type.
  class Functor f where 
    fmap :: (a -> b) -> (f a -> f b) -- this sig tells the compiler that `f` acts on types
    
More functor examples!

  data List a = Nil | Cons a (List a)
  1. List is a type constructor (List of Int, List of Bool, etc.)
  2. Is it a functor? define an instance of functor:
    instance Functor List where
      fmap :: (a -> b) -> List a -> List b
      fmap f Nil              = Nil
      fmap f (Cons head tail) = Cons (f head) (fmap f tail)
      -- fmap = map

  type Reader r a = r -> a
                  = (->) r a

  fmap :: (a -> b) -> (f a -> f b)
          (a -> b) -> (r -> a) -> (r -> b)
  fmap f g = f . g
           = (.) f g
  fmap = (.)          -- fmap for Reader/Function is composition. Neat.

What is the general intuition behind Functor?
* A functor acting on a type encapsulates the value of the type. Sort of.
* Analogous to a "container"
* How is Reader a container?
  - A function (Bool -> *) can be described as a container of two values
  - A function (Int -> *) can be described as a container of a sequence of values
* Distinction between DataType/Function is weak
  - e.g. infinite list [1..] is implemented as a function
  - e.g. data types are implemented as thunks
  - conclusion: There is no real distinction between Data Type and Function


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 7.1: Functoriality, bifunctors
https://www.youtube.com/watch?v=pUQ0mmbIdxs&index=13&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Composing Functors G . F

            F                     G
   a ----------------> F a ----------------> G (F a)
   |                    |                    |
 f |                    | F f                | G (F f)
   |                    |                    |
   v                    v                    v
   b ----------------> F a ----------------> G (F b)

   

Functor Identity (map everything to itself)

F . Id = F
Id . F = F

Functors define a category "Cat" where Functors are the morphisms and categories are the objects

Example of composition of functors, Maybe and List:

safeTail :: [a] -> Maybe [a]
safeTail []     = Nothing
safeTail (x:xs) = Just xs

Maybe List is also a functor. Define fmap:

fmap (fmap f) ms
(fmap . fmap) f ms

fmap for each level of composition.

Claim:
Algebraic Data Structures are automatically Functorial.
i.e. Product & Sum types

Is a Product (a, b) a Functor?

(a, b) == (,) a b

If we fix a, we get a functor in b. It is a type constructor in b.
Then a function is applied to the b.

(e, a) -------> (e, b)
  ^               ^
  |               |  
  |               |
  a ------------> b
  
  fmap f (e, x) = (e, x) -> (e, f x)

The pair is a "container" for the second object. You could also flip 
and use the same reasoning.

Is it a functor in both a and b at the same time? Yes.
We can define a functor that works on a pair of categories, i.e. a product of two categories.

Define a product of two categories: 
In small categories, objects form sets.
Take objects from C and D and form CxD = (c, d)
Morphisms pair in the same way. Hom-sets are sets, so you can take the Cartesian Product.
Composition: (f', g') . (f, g) = (f' . f, g' . g)
Identity:  (id_a, id_b) = id_{(a, b)}

It's just a category. So we can define a functor from CxD -> E (some category E)

Bifunctor: A functor from CxD -> E. A functor from the Product category.
           A mapping from two types into a type.
           Two functions are lifted at the same time.

Haskell Example:

class Bifunctor b where
  bimap :: (a -> a') (b -> b') -> f a b -> f a' b'
  
"A Product is a Bifunctor"

So... What about Sum? Is that functorial?

* Use the same bifunctor id. 
* Either a b is a bifunctor. Takes two types, returns a single type.

Category with a bifunctor is called Monoidal. That meeans there is a unit as well.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 7.2: Monoidal Categories, Functoriality of ADTs, Profunctors
https://www.youtube.com/watch?v=wtIKd8AhJOc&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=14

Monoidal Categories
* What does it mean to "multiply" two objects? 
  - Categorical Product
  - Associativity
  - Unit
* in Haskell we have Unit type; in CT this corresponds to Terminal Object
  Claim:
  a * () = a
  () * a = a
  
  Proof: 
  Candidiate
  
        a
    id / \  unit
      v   v
      a   ()
      
  add object b with projection p :: b -> a and unit_b :: b -> ()
  Is there a unique morphism from b -> a?
  observe id . p = p
  So we have the same object (a).
  QED

So: If you have a Categorical Product for every pair of objects and Terminal object 
    for the category, then you have monoidal structure for objects, i.e. a
    Monoidal Category.

Tensor Product: A monoidal category has a Tensor Product and a unit. (., 1)

----
Const Functor
Takes any type a, and maps it into a single object c (a.k.a. \delta c)

  data Const c a = Const c

`a` disappears. Is this a functor?

  instance Functor (Const c)  -- note that `Const c` requires a type argument (`a`)
    -- fmap :: (a -> b) -> Const c a -> Const c b
    fmap f (Const c) = Const c

Identity Functor

  data Identity a = Identity a
  
  instance Functor (Identity a)
    fmap f (Identity a) = Identity (f a)


Maybe redux

  data Maybe a = Nothing | Just a

this is equivalenet to saying:
  
  Either () (Identity a)
  -- or
  Either (Const () a) (Identity a)

Since we can produce Maybe by composing Functors, it is a Functor. QED.

extension to Haskell:
{-# LANGUAGE DeriveFunctor #-}

e.g.
data MyF = ..... deriving Functor

If you data type parametrically polymorphic, there can be only one `fmap`. Theorem for free.

Function
"arrow" is a type constructor of two arguments:

  (->) a b = a -> b

(see Reader functor above. Function is Functorial in the second argument.)
  newtype Reader c a = Reader (c -> a)
  -- recall `fmap` for Reader = (.), i.e. composition.


  data Op c a = Op (a -> c)
    fmap :: (a -> b) -> Op c a   -> Op c b
  = fmap :: (a -> b) -> (a -> b) -> (b -> c) 
            problem
             here
             
  arrow from a -> b prevents composing to get b -> c
  We can invert the arrows in the Co-category ...
  
  This should be called Cofunctor! But it's NOT! It's called "Contravariant."
  
  class Contravariant f where
    contramap :: (b -> a) -> (f a -> f b)
    
Back to (->) as a "Functor thingie"

  (->) a b goes from C^{op} x C -> C
  Take a pair of morphisms, but the first one is flipped.
  This is called a Profunctor. 
  
  classProfunctor p where
    dimap :: (a' -> a) -> (b -> b') -> (p a b) -> (p a' b')

first morphism is "flipped" (C^{op}).

Define `dimap` for (->)
  dimap :: (a' -> a) -> (b -> b') -> (p a b) -> (p a' b')
               f           g         h::a->b     a'->b'
  dimap = g . h . f

(->) is the simplest Profunctor.
  
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 8.1: Function objects, exponentials 
https://www.youtube.com/watch?v=REqRzMI26Nw&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=15

Function types (finally)
When a and b are sets:
* Hom-set is a set, so there is a set a -> b that corresponds to the hom-set between objects a and b.
* the homset is also an object in the category.

* In an arbitrary category, we have the Hom-set as an external thing. 
* What we want is an *internal* Hom-set. 
* In many categories it is possible to define such a Hom-set.

We can use Universal Construction to construct a Function object.

First we must have a Category with Product.
Model Function as a Pair, Function z and Argument a, that returns result b.
So we have a Cartesian Product of z x a like so:

  +-+ +-----+ 
  | | |     | eval
  |z| |z * a|-----> b
  | | |     | 
  +-+ +-----+
      +-----+
      |  a  |
      +-----+
      
Now, do the Universal Construction thing. Imagine another candidate z'. 
There is a Product z' * a, and a morphism g :: (z', a) -> b

Now we need to factor through g and eliminate g'. 
Add an arrow h from z' to z. But we also need an arrow from (z', a) and (z, a) 
so we can factor out g'.

Remember: Product is a *Bifunctor*: Takes two morphisms and produces a third morphisms.
So the first morphism is h :: z' -> z, and the second morphism is Identity (a -> a).
That maps (z', a) into (z, a).
Now we have a path from (z', a) to b through g.
g' = g . (h * id)
Therefore, (z, a) is the better candidate.
QED

In the diagram, you can think of g' as a Function of two arguments.
Observe that a function of two arguments is equivalent to a function 
of one argument that returns a function of one argument (down the `h` arrow).
Currying is built into this Universal construction.

h :: z -> (a -> b)
g :: (z, a) -> b

curry f = \a -> \b -> f (a, b)
translates a function from a pair into a function of one argument to a new function

uncurry f = \(a, b) -> f a b
translates a curried function into a function that takes a pair of arguments.

In Haskell: 
* Function Arrows associate to the right.
* Function application (call) associates to the left

In category theory, this is NOT called a function: It is call an "exponential".
a -> b ~ b^a
Argument on top, result in the base.

Example: Bool -> Int is a pair of Integers (one for False, one for True)
         All possible Bool -> Functions is all possible (Int, Int) pairs.
         This is the same as Int * Int, or Int^2 or Int^{Bool}

As long as the types are finite sets, the number of functions (a -> b) = b^a

Cartesian Closed Categories (CCC):
Products for every pair of objects.
"Closed" means it has exponentials as well, i.e. for every (a, b) there is a^b
And it has a Terminal Object. Like the zeroth power of an object.

If it has initial object as well, then it is a Bi-Cartesian Closed Category (BCCC)

With exponentials, we can do more algebra ... yay?

            a^0       = 1
            a^{Void}  = ()
  absurd :: Void -> a = ()

:. Exponential works for types with a^0

  1^a  = 1
  a -> ()
  
  a^1 = a
  () -> a ~ a


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 8.2: Type algebra, Curry-Howard-Lambek isomorphism 
https://www.youtube.com/watch?v=iXZR1v3YN-8&index=16&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

  a^{b + c} = a^b * a^c
  Either b c -> a ~ (b -> a), (c -> a)

  (a^b)^c = a^{b * c}
  c -> b -> a ~ (c, b) -> a -- currying
  
  (a * b)^c a^c * b^c
  c -> (a, b) ~ (c -> a, c -> b)
  -- IOW one function that produces a pair can be replaced by two function that produce each element of the pair.
  
-----
Programming, Type theory, Category theory, etc.: The same stuff keeps coming up. Why is that?
* Curry-Howard isomorphism: Propositions as Types. 
  One-to-One correspondence from type theory/programming/lambda calculus to logic.

  Proposition corresponds to Type.
  Proposition is True | False
  Type is Inhabited | Uninhabited
  
  If we can construct an element of a Type, we have "proven the proposition".
   
              Logic         Type     
              -----         -----
              True          Unit
              False         Void
conjunction   AND           (a, b)
disjunction   OR            Either a b  (or Sum type data S = X | Y)
implication   a => b        a -> b         
modus ponens  (a => b) ^ a  function application

Lambek added a third correspondence to objects in a CCC.
https://wiki.haskell.org/Curry-Howard-Lambek_correspondence
The Curry-Howard-Lambek correspondence is a three way isomorphism between types (in programming languages), propositions (in logic) and objects of a Cartesian closed category. Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs in logic (and vice versa).


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 9.1: Natural transformations 
https://www.youtube.com/watch?v=2LJC-XD5Ffo&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=17

Natural Transformations

One of the (3) foundations of CT
* Definition of Category: 
  - Objects, Morphisms, Composition, Identity. All about structure.
* Defintion of Functor: 
  - Mappings between categories that preserve structure.
  - Embed/Mopdel a category inside another category
* Definition of Natural Transformations:
  - Mappings between functors, preserving structure.

Definition (expanded)
Two categories, C and D.
Functor F maps object a in C to object (F a) in D
Functor G maps object a in C to object (G a) in D
We need a mapping in D between (F a) and (G a), i.e. F a -> G a
- But -- D already has mappings.
- We don't want to just arbitrarily add one
- But we should be able to pick one from the hom-set (F a -> G a)
For every object in C, find two object imagess in D, and choose a morphism in D between those images
These morphisms are called a "Component". (A Component is a morphism)
- e.g. \alpha_a :: F a -> G a 
- Observe that although `a` is in C, the Component F a -> F g is in D.

All the Components taken together form a family of morphisms, and that is the Natural Transformation. 
Except we need to talk about structure of C being preserved in D (i.e. morphisms in C)

Take objec b in C and map into F b and G b
- So we have a Component \alpha_b :: F a -> F b
- what about morphism f :: a -> b in C? That will be mapped by Functor F to F f and by G to G f.

What is the relationship between F f G f? Are they "similar"?
An NT does not have to exist at all. There are such categories.
There must be a relation between the four arrows: \alpha_a, \alpha_b, F f, G f.
Observe that G f . (F a -> F b) = G b = (F b -> G b) . F f = G b
                    \alpha_a             \alpha_b
This equality is the "Naturality Condition" and the graph of it is the "Naturality Square"

                F f
        F a ------------> F b
         |                 |
\alpha_a |                 | \alpha_b
         |                 |
         v                 v
        G a ------------> G b
                G f

Another Definition:
* NT maps objects to morphisms.
* NT maps morphisms to commuting diagrams viz the "Naturality Square"

In mathematics, and especially in category theory, a commutative diagram is a diagram of 
objects (also known as vertices) and morphisms (also known as arrows or edges) such that 
all directed paths in the diagram with the same start and endpoints lead to the same result 
by composition. 

NT gives us a higher-level language in CT for discussing commuting diagrams.
We can replace talk of commuting diagrams with 
"There is a NT between functors." That implies the naturality squares.

An invertible NT is called a "Natural Isomorphism"
All of the morphisms in the Naturality Square will have arrows in the other direction as well.

What is an NT in Programming?
* A family of functions parameterized by a type
* Hence a NT in programming context is a polymorphic function
  - e.g. alpha :: forall a . F a -> G a
    This is defined for all types `a`. 
    (use "explicit forall" extension in Haskell)

There is a subtle difference: 
* In Haskell we are assuming parametric polymorphism, i.e. can only define one formula *for all types*
* This is much stronger than categorical definition.

Why?
Consider Naturality Square.
\alpha_b . fmap_F f =  fmap_G f . \alpha_a

First fmap is for Functor f, second one is for Functor G.
In Haskell, specifying the Functor instance is unnecessary. You get it for free.

Example: List Functor and Maybe Functor

safeHead :: [a] -> Maybe a
safeHead []    = Nothing
safeHead (x:_) = Just x

safeHead works for every Type `a`. 
It is parametrically polymorphic.
Claim: safeHead is automatically "Natural"

Proof:
    Empty List case:
    1. fmap f []       = []
       safeHead []     = Nothing
    2. safeHead []     = Nothing
       fmap f Nothing  = Nothing

    Non-empty list case
    1. fmap f x:xs     = f x : (fmap f xs)
       safeHead (x:xs) = Just x
    2. safeHead (x:xs) = Just x
       fmap f (Just x) = Just (f x)

Practical benefit? CT provides opportunity for optimization. 
e.g. safeHead first then fmap is cheaper than fmap then safeHead
     compiler may be optimized to use these categorical transformations.

NT never modifies the contents of the container.
Instead it repackages into a different container.
There is *no way* to modify the contents because the content is *polymorphic*
OTOH, Functor preserves the container but may modify its contents.

Naturality Condition means that it does not matter whether you 
repackage first and then fmap, or fmap first and then repackage.

Examples:

  a -> [a]
  is a NT because `a` is equivalent to `Identity a`, so this is a mapping of 
  Identity functor into List functor.

  length :: [a] -> Int
  Mapping a List Functor to a Const Functor.
  
In general if you have a function from ADT -> ADT, it is a NT
* Not all, though: There are mixed functors, e.g. contravariant in one argument, and covariant in the other
  that do not satisfy Naturality.

Back to Kleisli arrows:
  
  a -> m b
  return :: a -> m a
  
  return is defined as a NT. (Same as Identity a -> [a], as shown above)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 9.2: bicategories 
https://www.youtube.com/watch?v=wrpxBXXgLCI&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_&index=18

Generalizing Category Theory.
uh-oh: "Deep math."

Every time you are mapping ask yourself: Do they compose?
What would it mean to compose NTs?

  NT \alpha :: F -> G 
  NT \beta  :: G -> H

     C                                  D
                     F  
          +---------------------------> F a
         /                              |  
        /                               | \alpha_a
       /                                v
     a ------------------------------> G a
       \                                | 
        \                               | \beta_a
         \                              V
          +--------------------------> H a
         
\alpha_a and \beta_a are morphisms. They compose (obv). So you can compose \beta . \alpha.
Is the composition \beta . \alpha a NT?
To determin that we would need to verify that:
* there is an object b in C with an arrow f :: a -> b
* then we have F b, G b, H b, and morphisms F f, G f, H f
* Verify Naturality Condition:
  H a . (\beta_a . \alpha_a) = f a . (\beta_b . \alpha_b)
  That forms the composed Naturality Square, with corners F a, F b, H b, H a
  
     F a ------> F b
      |           | 
      |           | 
     G a - - - > G b
      |           |
      v           v
     H a ------> H b 
  
 Is there Identity?
 An Identity NT is the family of morphisms from F a to itself.
 
 Is it associative?
 In Components, it is. 
 
 Functors between categories [C, D] form a category where Functors are objects and NT are morphisms.
 Can be written D^C
 
 Back to Cat:
 * Objects are Categories
 * Morphisms are Functors
 
                     F 
            +-------------------+
           /         ||          \
          /          ||           \
         C           ||            D  
          \          ||           /
           \         \/          /
            +-------------------+
                     G
                     
In Cat there are Functors between categories, and NTs between Functors.

This is called a 
2-category.
* in Cat, the Hom-Set is a set of Functors
* Note that the Hom-set between two categores is itself a category
* Therefore the Hom-set is also an element in Cat
* [C, D] = D^C
* Conclusion: Cat is CCC

To construct a category with Hom-objects (instead of Hom-sets):
* Hom-objects must be from a Monoidal category, using monoidal operator for composition
* This called an "Enriched category"

back to 2-category
* There are two axes of composition. 
  1. From object -> object (horizontal)
  2. From Functor -> Functor (vertical)
* Consider two compositions of the horizontal type: G . F and G' . F'
  - How do we construct a NT from those functors?
    The functors fan out:
    1. Start with object a with Functors F a and F' a. There is an NT \alpha_a :: F a -> F' a
    2. At F a and F' a the split again:
       F a  goes via G  to (G . F) a
       F a  goes via G' to (G' . F) a
       F' a goes via G  to (G . F') a
       F' a goes via G' to (G' . F') a
    3. We can lift/transport \alpha_a to (G . F)  a -> (G . F') a
       We can lift/transport \alpha_a to (G' . F) a -> (G' . F') a
    4. We have \beta_a (G . F)  a -> (G' . F) a
       We have \beta_a (G . F')  a -> (G' . F') a
    5. We get our composition G . F -> G' . F' either by:
       G' \alpha_a . \beta_a
       \beta . G' \alpha_a
    6. There is out Naturality Square. The diagram shows it better than I just wrote it, but would be a nightmare to try and do ACII style   

Wait -- it gets worse:
Interchange law: Add \alpha' and beta' and draw arrows until your eyes bleed

OK back to the show.

If you have morphisms between morphisms, you can have isomorphisms between morphisms.
Let's forget about "equality". 
Let's just say "up to isomorphism".

Define a 2-category where things are defined "up to isomorphism": You get a Bicategory
In a bicategory: Categorical Laws are up to isomorphism.
Since things may not be strictly equal, but only up to isomorphism, you must have coherence laws
for Associators and Unitors.
Every n-category you go up spawns new coherence laws, and they are not unique.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 10.1: Monads 
https://www.youtube.com/watch?v=gHiyzctYqZ0&index=19&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Why do we need functions?
Functions are about structuring code. 
Composition is the key. a -> b -> c -> d

Monads are about structuring code.
Composition is the key.

Monad replaces the (.) of function composition with the Kleisli arrow (>=>) (fish operator)
a >=> b >=> c >=> d

                Function            Monad
composition     .                   >=>
identity        id                  return
category        Types/Functions     Kleisli

`return` can make functional-composition code look more imperative & maybe more readily understandable

`fish` anatomy >=>
* (>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
  - `m` is a Functor (it's a Monad, but wait for it)
  - `m` is a type constructor and has `fmap`, i.e. it knows how to lift functions

  f >=> g = \a -> let mb = f a in mb >>= g
  -- need a function (>>=) to unwrap the b from f so g can use it:
  -- (>>=) :: m b -> (b -> m c) -> m c
  
  (>>=) a.k.a. `bind` arises from the need to compose with these "containers".
  
  class Monad m where
    (>>=) :: m a -> (a -> m b) -> m b    (a.k.a. bind for composition)
    return :: a -> m a                   (Kleisli Identity arrow)
    
  Observe we can define `fmap` from `bind` and `return`. (IOW Monad is a Functor)
  
  This is sufficient to define a monad, but we can go deeper into the fish guts. 
  Let's break down `bind`:
  
  m a >>= (a -> m b) = ??? fmap (a -> m b) (m a)
  ma  >>= f          = ??? fmap     f       ma
                     = ??? m (m b)               -- Not quite
  -- need a function `join :: m (m a) -> m a` to satisfy bind contract
                     = join (fmap f ma) -- With `join`, we can define `bind`
                     
  So: Alternative definition of Monad:
  
  class Functor m => Monad m where 
    join :: m (m a) -> m a
    return :: a -> m a

Why? What problems do Monads solve?
* Composition for Kleisli arrows. Ummmm

Recast the question: Why are Kleisli arrows useful? 
* Everything is pure functions
* This causes some pain when trying to cope with e.g.: side-effects, state, exceptions, continuations ...
* Everything can be converted to pure computation by replacing impure functions with embellished results.

Where does the monad come in to this?
* start with a giant computation a -> Embellished Result
* To decompose this giant computation into small composable parts, you use monads.

Examples:

Maybe Monad 
* any partial function a -> b can be converted to a -> Maybe b
* Now the partial function is a pure function.
* How do you compose these purified functions? Monadic composition.

  join :: Maybe (Maybe a) -> Maybe a
  join (Just (Just x)) = Just x
  join _               = Nothing

  bind :: Maybe a -> (a -> Maybe b) -> Maybe b
  bind Nothing _  = Nothing
  bind (Just x) f = f a
  
  -- observe that we do not invoke `f` when we are dealing with `Nothing`.
  -- this is analogous to an exception. 
  
  return :: a -> Maybe a
  return a = Just a

Either Monad could also be used to encapsulate exceptions, and pass information about the failure along in the Left.

Suppose you have a function a -> b that access some state s. Not a pure function, obv.
We can turn it into a pure function by passing the state along explicitly:

  (a, s) -> (b, s)
  -- not quite Kleisli arro, but we can get there with curry:
  
  a -> (s -> (b, s))
  
  newtype State s a = State (s -> (a, s)) -- parameterized by state s and functorial a (Reader Functor)
                                          -- arrow is functorial in the return type

----------
Monad Laws

1. Associativity
2. Unit
3. Identity
  
Can't be expressed in Haskell directly, so back to CT we go

Terminology map

  Haskell   CT
  m         T    -- n.b.: T must be an endofunctor, i.e. mapping a category into itself
  join      \mu
  return    \eta
  
\eta :: Id -> T     (NT from Identity Functor to T)
\mu  :: T^2 -> T    (NT from T composed with itself to T)

A monad is a Functor T and two NTs. Plus laws.


NT #1: \eta (return)
                    Id
            +-------------------+
           /         ||          \
          /          ||           \
         C           || \eta       C
          \          ||           /
           \         \/          /
            +-------------------+
                     T
  
NT #2 \mu (join)
              T             T
            +------> C ---------+
           /                     \
          /                       \
         C                         C
         |\         T^2           /|
         | +---------------------+ |
         +           ||            + 
          \          || \mu       / 
           \         \/          / 
            +-------------------+
                     T

Chase the diagram to show Associativity: 

\mu . (\mu o I) = \mu . (I o \mu)
\mu . (\mu o T) = \mu . (T o \mu)


            T^3
\mu o I_T  /   \ I_T o \mu
          /     \
        T^2     T^2
          \     /
       \mu \   / \mu
             T

Identity:

Id o T -- \eta o T --> T^2
T o Id -- T o \eta --> T^2
T^2    -- \mu -------> T

Id o T = T = T o Id
QED


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Category Theory 10.2: Monoid in the category of endofunctors
https://www.youtube.com/watch?v=GmgoPd7VQ9Q&index=20&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Let's talk monoids.
* Usually defined in terms of sets
* Can be represented as a single-object category with a bunch on endomorphisms.
    Every single object category is a monoid; and
    Every monoid can be expressed as a single-object category

\mu :: a * a -> a   -- function from a set of pairs from AxA to the product of those pairs
\eta :: () -> a      -- function from id element/terminal object to a

(Recall that at Cartesian Category has a Product and a Terminal Object)

Monoid Laws:
* Associativity
   \mu (\mu (x, y), z) = \mu (x, \mu(y, z))
* Unit
   Left:  \mu (\eta (), x) = x
   Right: \mu (x, \eta ()) = x

See the diagram for how we reduced T^3 to T via \mu and I_T. 
Doing the same thing with ((a * a) * a)
But -- (a * a) * a is not really "equal" to a * (a * a)
But we can define morphisms to make these things equal up to isomorphism.

Conclusion: Product is monoidal up to isomorphism. 

So a monoidal category is a category with
* A Bifunctor :: (a, b) -> a ⊗ b (i.e. Tensor Product)
* Identity object I

Monoid: (I, ⊗)
* object m
* \mu :: m ⊗ m -> m
* \eta :: I -> m

Category of Endofunctors [C, C]
* Objects are Endofunctors
* Morphisms are Natural Transformations
* Tensor Product is composition of endofunctors
* Associativity: (F o G) o H = F o (G o H)
* Unit: Identity Functor: Id o F = F = F o Id

...