Curry-Howard-Lambek Isomorphism

Curry-Howard-Lambek Isomorphism

\boxed {\text {Category} \iff \text {Algebra} \iff \text {Logic} \iff \lambda \text {-Calculus}}

Below the lecturer said every aspect of Math can be folded out from Category Theory, then why not start teaching Category Theory in schools.

That was the idea proposed by Alexander Grothendieck to the Bourbakian Mathematicians who rewrote all Math textbooks after WW2, instead of in Set Theory, should switch to Category Theory. His idea was turned down by André Weil.

\boxed { a^{b + c} = a^{b} \times a^{c} }

\boxed {\text {Left-side: Either b c } \to a}

\boxed {\text {Right-side: } (b \to a , c\to a) }

\boxed { (a^{b})^{c} = a^{b \times c}}

\boxed { c \to (b \to a) \sim (b ,c) \to a}

\boxed { (a \times b)^{c} = a^{c} \times b^{c}}

\boxed {c \to (a,b) \sim (c \to a , c \to b)}

BM Category Theory 8 : Function objects (Exponentials), Curry / unCurry


[Revision] Product (or Sum = co-Product) is a Bifunctor

  • takes 2 objects to produce 3rd object;
  • takes 2 morphisms to produce 3rd morphism. 

Functions are “morphisms between Category objects”  = a Hom-Set, which itself is an object : ‘a -> b’.

Using the same method of Universal Construction of Product objects in category :  

  1. Define a Pattern ,
  2. Ranking which object is better, 
  3. Pick the best object up to an UNIQUE Isomorphism.

we can similarly construct the Function Objects ‘a => b‘ (in Haskell as ‘a -> b’) :

Intuitively, the above diagram is interpreted as: 

  • evalthe Function object(a=>b) x ato return result b
  • g is up to Unique isomorphism (hSAME as ‘eval: \boxed {g = eval \circ (h \text { x } id )}

Curry / Non-curry : Associative (yellow brackets below are optional).

\boxed {z \to (a \to b ) \iff z \to a \to b }

\boxed { (f a ) \: b \iff f a \: b }

Note: function (f a) returns as a new  function which applies on argument b. Equivalently, also read as “f takes 2 arguments a, b”.


f :: Bool -> Int

Bool = {0, 1}
{ f = (Int \text { x }  Int) = Int^{2} = Int ^ {Bool}}

The number of possibilities of applying f from a to b is \boxed {b^{a}} , hence we call:  
\boxed {\text {Function object f as EXPONENTIAL}}

8.2  Algebraic Data Types