函数概念并不难,理解“函”字是关键——函数概念如何理解】

【函数概念并不难,理解“函”字是关键——函数概念如何理解】
https://m.toutiaocdn.com/group/6714162037842248205/?app=news_article_lite&timestamp=1563301386&req_id=201907170223060101520450386849493&group_id=6714162037842248205&tt_from=android_share&utm_medium=toutiao_android&utm_campaign=client_share

清. 李善兰 翻译 Function 为函数。函,信也。只能有一个收信人,所以 只有一个 f(x) 值。

The unique 1 single output of a function becomes very important for subsequent development in Math & IT:
functions are composable, associative, identify function,etc (distributive,… ) => it can be treated like vector => structure of a Vector Space “Vect”

Extended to..

“Vect” is a bigger structure “Category” in which “function of functions” is a
Functor” (函子)F:F(f)

Example : F(f) = fmap (in Haskell)

fmap (+1) {2,7,6,3}

=> {3,8,7,4}

here F = fmap, f = +1

The Math branch in the study of functions is called “functional” 泛函。

IT : Functional Programming in Lisp, Haskell, Scala, ensure safety of guaranteed output by math function property. Any unexpected exception (side effects: IO, errors) is handled by a special function called “Monad” (endo-Functor).

(想看更多合你口味的内容,马上下载 今日头条)
http://app.toutiao.com/news_article/?utm_source=link

A Functional Programmer’s Guide to Homotopy Type Theory (HoTT)

Since April 2019 until I re-visit this Youtube video on 12 August 2019, I can now totally understand his speech after a pause of 4 months by viewing other related Youtube (below prerequisite) videos on Category Theory, Type Theory, Homotopy Type Theory.

That is the technique of self-study:

  1. First go through the whole video,
  2. Don’t understand? view other related simpler videos.
  3. Repeat 1.

Prerequisite knowledge:

  1. Homotopy
  2. Type Theory
  3. Homotopy Type Theory
  4. Bijection = Isomorphism
  5. Functional Programming in Category Theory Concept: Monad & Applicative

Two Key Takeaway Points:

  1. In the Homotopy “Space” : Programs are points in the space, Paths are Types.
  2. “Univalence Axiom” : Paths Induce Bijection, vice versa.

Les Categories Pour Les Nuls

“Categories for Dummies”
(French)

Example 1:

Paris (P) -> Rome (R) -> Amsterdam (A)

Objects: cities {P, R , A…}

Morphism (Arrow)
: railway 

  • Identity: railway within the city
  • Associative: (P -> R) -> A = P -> (R ->A)

=> Category of “Euro-Rail” 

Remark: In the similar sense, China “One Belt One Road” (OBOR)” 一带一路” is a “Pan-China-Europe-Asian” Category “泛中-欧-亚” 范畴

Example 2:
A, B are categories

functor f : A -> B 

f (B) has the “information” on A, with some loss of information since f may not be a MONOMORPHISM (单射 Injective).

Remark: Technical Drawing, the views from Top , Left, Right, or Bottom of the object are Functors – which provide only 1 view from 1 direction with loss of information from 3 other directions.

Example 3: Natural Transformation

A = 0 1 2 3 

f : A -> B

B = Ladder steps:
f(0)|
f(1)|
f(2)|
f(3)|

g : A -> B

B = Staircase steps :
g(0)||
g(1)||
g(2)||
g(3)||

Natural Transformation: =>  α 

α : f (i) => g (i)

f(0)| => g(0)||
f(1)| => g(1)||
f(2)| => g(2)||
f(3)| => g(3)||

α  transforms naturally the Ladder to the Staircase.

An Introduction to N-Categories

Tom Leinster

N = 0 : 0-Cat 

  • => Set, 0-morphism = function

N= 1: 1-Cat 

  • => Cat, 1-morphism = functor

N= 2: 2-Cat 

  • => 2-morphism = Natural Transformation

\text {f, g : 1-morphism } 

\alpha \:\: \beta \text { Natural Transformations : 2-morphism } 

Definition of n-Category: 

Composition:

0-Cat : Set
1-Cat : Cat

Examples of n-Categories:

  • Manifold
  • Top (Topological Space) : 2-morphism = homotopy

Ref:  

Best Technical Category Theory Book (2016) by Tom Leinster (Cambridge Press): “Basic Category Theory”

(Free download from arxiv)

Program = Category 

2017 : (PhD Math made simple for IT programmers)

Keywords:

  • Category
  • Monad = Monoid + Endofunctor
  • Lewvere Theory

Category Theory is replacing Set Theory as the foundation of Math. Nowadays, few Advanced Math papers are written without using Category to explain, and this trend is spreading to IT through Functional Programming languages (Google’s Kotlin, Haskell, Clojure…) – the latest paradigm to replace Object-Oriented languages like Java, C++, etc, as a safer “Strong Typed” languages for AI, BIG DATA…

\boxed {\text {Type = Category }}

Examples of “Types” in IT:

  • Integers
  • Real
  • Double
  • Boolean
  • String
  • etc

T-program defined in the following 6 examples:

  • list (X), eg. {2, 5 , 3, 7, 1 }
  • partial (X), eg: +1 (error msg)
  • side-effect, eg: update a record
  • continuation (X),
  • non-det (X),
  • prob-dist (X)

A Monad : a T-program which turns an arrow to a “Category” (ie + 2 properties: Identity & Associative).

Proof: List Computation is a Category

Proof: Partial operation is a Category

\boxed {\text {Monad = Lawvere Theory }}

Monad is for only one Category. Lawvere Theory is more general.

Ref:

Slides: http://www.math.jhu.edu/~eriehl/compose.pdf

Ref:
Excellent Intuitive Stackoverflow Answer: What is a Monad ?

Monoid and Monad

Quora: What is the difference between monoid and monad? by Mort Yao https://www.quora.com/What-is-the-difference-between-monoid-and-monad/answer/Mort-Yao?share=41115848&srid=ZyHj

A well-said, perhaps the briefest ever answer is: monad is just a monoid in the category of endofunctors.

monoid is defined as an algebraic structure (generally, a set) M with a binary operation (multiplication) • : M × M → M and an identity element (unit) η : 1 → M, following two axioms:

i. Associativity
∀ a, b, c ∈ M, (a • b) • c = a • (b • c)

ii. Identity
∃ e ∈ M ∀ a ∈ M, e • a = a • e = a

When specifying an endofunctor T : X → X (which is a functor that maps a category to itself) as the set M, the Cartesian product of two sets is just the composition of two endofunctors; what you get from here is a monad, with these two natural transformations:

1. The binary operation is just a functor composition μ : T × T → T
2. The identity element is just an identity endofunctor η : I → T

Satisfied the monoid axioms (i. & ii.), a monad can be seen as a monoid which is an endofunctor together with two natural transformations. 

The name “monad” came from “monoid” and “triad”, which indicated that it is a triple (1 functor + 2 trasformations), monoidic algebraic structure.



In other words, monoid is a more general, abstract term. When applying it to the category of endofunctors, we have a monad.

https://www.quora.com/What-is-the-difference-between-monoid-and-monad/answer/Bartosz-Milewski?share=e4dc6c63&srid=ZyHj

State Monad: Milewski

BM 5&6 : Category Adjunctions 伴随函子

Adjunction is the “weakening of Equality” in Category Theory.

Equivalence of 2 Categories if:

5.2  Adjunction definition: (L, R, \epsilon, \eta ) such that the 2 triangle identities below ( red and blue) exist.

6.1 Prove: Let C any category, D a Set.

\boxed {\text {C(L 1, -)} \simeq \text {R}}

{\text {Right Adjoint R in Set category is }} {\text {ALWAYS Representable}}

1 = Singleton in Set D

From an element in the singleton Set always ‘picks’ (via the function) an image element from the other Set, hence :
\boxed {\text{Set (1, R c) } \simeq \text{Rc }}

Examples : Product & Exponential are Right Adjoints 

Note: Adjoint is a more powerful concept to understand than the universal construction of Product and Exponential.

6.2

\boxed  {\text {Every Adjunction gives a Monad}}

vice-versa.

\boxed {\text {Left Adjoint: L } \dashv \text { R }}

R \circ \ L = m = \text { Monad}

L \circ \ C = \text { Co-Monad}

With Product (Left Adjoint) and Exponential (Right Adjoint) => \text {State Monad}

Category Theory II 2: Limits, Higher order functors

1.2 Introduction to Limit 

Analogy : Product to Cones (Limit)

2.1 Five categories used to define Limit:

  1. Index category (I)
  2. Category C: Functors (constant ,  D)
  3. Cones (Lim D)
  4. Functor Category [I, C ]:objects are (constant, D ), morphisms are natural transormations
  5. Set category of Hom-Set Cones [I,C] to Hom-Set C (c , Lim D )

2.2 Naturality

3.1 Examples: Equalizer

CoLimit = duality of Limit (inverted cone = co-Cone)

Functor Continuity = preserve Limit

BM Category Theory 10: Monad & Monoid

10.1 Monad
Analogy

Function : compose “.“, Id

Monad: compose “>>=“, return

Imperative (with side effects eg. state, I/O, exception ) to Pure function by hiding or embellishment in Pure function but return “embellished” result.

10. 2 Monoid

Monoid in category of endo functors = Monad

Ref Book : 

What is the significance of monoids in category theory? by Bartosz Milewski 

Category Theory 9: Natural Transformations, BiCategories

In essence, in all kinds of Math, we do 3 things:

1) Find Pattern among objects (numbers, shapes, …),
2) Operate inside the objects (+ – × / …),
3) Swap the object without modifying it (rotate, flip, move around, exchange…).

Category consists of :
1) Find pattern thru Universal Construction in Objects (Set, Group, Ring, Vector Space, anything )
2) Functor which operates on 1).
3) Natural Transformation as in 3).

\boxed {\text {Natural Transformation}}
\Updownarrow

\boxed {\text {Morphism of Functors}}

Analogy:

Functors (F, G) := operation inside a container
\boxed { F :: X \to F_{X}, \: F :: Y \to F_{Y}}

\boxed {G :: X \to G_{X}, \: G :: Y \to G_{Y}}

Natural Transformation ({\eta_{X}, \eta_{Y}}) := swap the content ( F_{X} \text { with } G_{X}, F_{Y} \text { with } G_{Y} ) in the container without modifying it.
\boxed{\eta_{X} :: F_{X} \to G_{X} , \: \eta_{Y} :: F_{Y} \to G_{Y}}

9.2 Bicategories

“Diagram Chasing”:

2- Category:

Cat = Category of categories (C, D)

The functors {F, G} instead of being a Set (“Hom-Set”) – like functions form a function objectExponentialfunctors also form a category, noted : \boxed {[C,D] = D^{C} }

BiCategory (different from 2-Category): the Associativity and Identity are not equal (as in 2-Category), but only up to Isomorphism.
Note : when n is infinity, n-Category & Groupoid (HOTT: Homotopy Type Theory)

Reading Book: chap 10

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

8.1 

[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”.

Example: 

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

BM Category Theory 6: Functors & Examples

6.1 

Discrete Category:  no other Morphism except the Identity Morphism. 

Functor between 2 categories : preserve structures.

6.2 Examples of functors

In-lining & Refactoring (in Pure Function)

1. In-lining: function f = function g
Replace everywhere in the program each f by g.

2. Re-factoring: In the program: {expressions}
We can define a function h = {expresions}, then use h throughout.

class Functor f where
\boxed {fmap : : (a \to b) \to (f a \to f b)}

Examples of Functors:

1. List

2. Reader

Functor (esp. Endo-functor) can be viewed as a Container where you can opetate on its content. Eg. Functor List [1 ..] = container of 1 2 3 … infinity, operared on it by generating (lazily) the next number.

Illustrations of Functors and Monad (Endo-functors): a “wrapped container”.

http://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_pictures.html#functors

BM Category Theory 5: Coproducts = Sum types

5.1 Coproducts = Sum types

Product c is the “Best” than any others like c’, with projections p, q into a and b respectively (Haskell “fst“, “snd“) — because all c’ = c (up to a unique isomorphism m).

Coproduct is like “yin-yang” (阴阳合一) sum of 2 objects {a, b} into c – injection “discriminately” (in Haskell by “Left” and “Right”)

5.2 Algebraic Data Types

Prove that Product and Sum are Monoids ? They are!

  • Both are Associative. 
  • Identity for Product = Unit ()
  • Identity for Sum  = Void

 Product (*) , Sum (+) are Distributive : 

a * (b + c ) = a * b + a * c \iff (a , (Either \: b \: c)) = Either \:  (a, b) \:( a, c)

There is is no inverse for “sum”, or negative.

Hence, it is a  structure  Ring without “n” = Rig (or Semi-Ring)

Maybe (= 1+a)

data Maybe = Nothing | Just a

\boxed {\text {Maybe } a = \text {Either () } a}

Algebraic Data Types: 

We can solve algebraic equation with Product & Sum :

BM Category Theory 3 & 4 Monoid, Kleisli Category (Monad), Terminal /Initial Object, Product… Free Monoid 

[Continued from 1.1 to 2.2]

3.1 Monoid M (m, m)

Same meaning in Category as in Set: Only  1 object, Associative, Identity

Thin / Thick Category:

  • “Thin” with only 1 arrow between 2 objects; 
  • “Thick” with many arrows between 2 objects.

Arrow : relation between 2 objects. We don’t care what an arrow actually is (may be total / partial order relations like = or \leq , or any relation), just treat arrow abstractly.

Note: Category Theory’s “Abstract Nonsense” is like Buddhism “空即色, 色即空” (Form = Emptiness).

Example of Monoid: String Concatenation: identity = Null string.

Strong Typing: function f calls function g, the type of the output of f must match with the type of the input of g.

Weak Typing:   no need to match type. eg. Monoid.

Category induces a Hom-Set: (Set of “Arrows”, aka Homomorphism 同态, which preserves structure after the “Arrow”)

  • C (a, b) : a -> b
  • C (a,a) for Monoid : a -> a

3.2 Kleisli Category (Monad) 

Morphism between a, b :
\boxed{a \to (b, \text {string})}

In brief, embellish the returned output b with string. 

In the example of Kleisli Category, using Monoid (single object) with embellishing string => Monad (covered in later videos).

4.1 Monad (one definition) : Kleisli

Set and Category SET: 

  • Set has elements and function between sets.
  • Category SET has NO element, only arrows (morphisms)

Universal Construction: define relations between Objects.

Set is rich with functions, except 1 case: There is no function from a non-empty set to Void (because a function must have an image in the co-domain, but Void has no element as the Image.)

Terminal Object : all other objects (each with UNIQUE arrow) point to it. [Denoted as () or Unit]

\boxed { \forall a, \exists f :: a \to ()}

\boxed { \forall a, f :: a \to (), g :: a \to () \implies f = g } (Uniqueness of arrow)

Note: Terminal Object (T.O.) is the largest object. There is no T.O. in Natural numbers.

Initial Object: reverse of Terminal object. Outgoing arrow from Void.

absurd :: Void -> a

Category “Equality”:

  • 2 objects are isomorphic (exists an inverse arrow), but we don’t say they are equal;
  • Arrows can be equal by associativity :  f \circ (g \circ h) = (f \circ g) \circ h

Terminal Object (Similarly, Initial Object) is unique (up to ONLY ONE Isomorphism). 

Assume both Ta and Tb are Terminal Objects. Prove Ta = Tb by showing there is only one isomorphism.

Note1: example of 2 isomorphisms between 2 Objects : (0, 1) and (T, F) => 

  • 1st isomorphism : (1 ~ T), (0 ~ F)
  • 2nd isomorphism: (1 ~ F), (0 ~ T)

Note2: There are outgoing arrows from T.O. => generalising.

4.2 Products

C^{op} : also a Category with all arrows in C reversed.

Products (Cartesian) of 2 objects (a,b): by Universal Construction.

p and q are (good) projections of c.
p’ and q’ are (another) projections of c’.

c is the product of (a, b) if 
there is a UNIQUE  isomorphism m,
\boxed {m :: c' \to c }
\boxed {p' = p  \circ m}
\boxed{q' = q  \circ m}

II 3.2 Free Monoid

Monoid : with a Set of 2 generators (a, b)

  • Identity: e*a = a*e = a; 
  • Associativity

Free Monoid = {e, a, b, ab, ba, aab, abb, ….}, notice it is generated by the set {a, b} and thus not a Monoid (noted as Mon).

We can create a Functor U (aka  Forgetting function) between Monoid and its underlying Set: 

\boxed { U :: Mon \to Set }

Category Theory for Functional Programming

Category Theory is called “The Mathematics of Mathematics“, also the “Abstract Nonsense“.

image

Key Motivations for Category Theory 范畴 :
1. Programming is Math.
2. Object-Oriented is based on Set Theory which has 2 weaknesses:
◇ Set has contradiction: The famous “Russell’s Barber Paradox”.

image

image

Data Immutability for Concurrent Processing : OO can’t control the mutable state of objects, making debugging impossible.

Category (“cat“) has 3 properties:
1. Objects
eg. Set, List, Group, Vector Space, anything…
2. Arrows (“Morphism”, between Objects) which are Associative
eg. function, sheaf, etc
3. Identity Object

Note: If the Identity is “0” or “Nothing”, then it is called Free Category.

Extensions :
1. “Cat” = Category of categories, is also a category.
2. Functor 函子 = Arrows between Categories.
3. Monoid = A Category with ONLY 1 Object.

image

image

Monoid (么半群) is a very powerful concept (used in Natural Language Processing) — basically it is a Group with No ‘I‘nverse (Mo‘No‘-‘I‘-d).

image

image

Note: In the pure Functional Programming Language Haskell:
Monad (单子) = Monoid with endo-functor.
Endo- = to itself (自己) eg. “f : A -> A”

image

Recommended :
1. The Best Book on Category Theory : Lawvere et al, Cambridge (2009, 2nd Edition)

image

2. A humorous book on Category Theory by Dr. Eugenia Cheng (2016): (found in Singapore NLB Loan book #501.1 CHE)

image

Math Education Evolution: From Function to Set to Category

Interesting Math education evolves since 19th century.

“Elementary Math from An Advanced Standpoint” (3 volumes) was proposed by German Göttingen School Felix Klein (19th century) :
1)  Math teaching based on Function (graph) which is visible to students. This has influenced  all Secondary school Math worldwide.

2) Geometry = Group

After WW1, French felt being  behind the German school, the “Bourbaki” Ecole Normale Supérieure students rewrote all Math teachings – aka “Abstract Math” – based on the structure “Set” as the foundation to build further algebraic structures (group, ring, field, vector space…) and all Math.

After WW2, the American prof MacLane & Eilenburg summarised all these Bourbaki structures into one super-structure: “Category” (范畴) with a “morphism” (aka ‘relation’) between them.

Grothendieck proposed rewriting the Bourbaki Abstract Math from ‘Set’ to ‘Category’, but was rejected by the jealous Bourbaki founder Andre Weil.

Category is still a graduate syllabus Math,  also called “Abstract Nonsense”! It is very useful in IT  Functional Programming for “Artificial Intelligence” – the next revolution in “Our Human Brain” !

Category Theory (Steven Roman) – (Part II)

[Continued from (Part I)…]

Category Theory (范畴学) is the “lingua franca” (通用语) of mathematicians, used commonly by the 2 different major Math branches : Algebra & Analysis.

比喻:
武术分”外家拳”少林派, “内家拳” 武当派。
两家的 lingua franca (通用语)是 “” – 硬气功(少林), 柔气功(武当)。

In essence: A Category consists of
1. Objects
2. Relationship among objects (Morphism = a set denoted by Hom (A,B), where A, B are objects)
3. Structure: preserved by Morphism
4. An Identity morphism

Examples:
1. SET Category:
◇ Objects (Sets),
◇ Structure (Cardinality)
◇ Morphism (Set Functions: which preserve Set Structure)
◇ Identity morphism (Set to itself)

2. GROUP Category
◇ Objects (groups)
◇ Structure (Set, 1 closed binary operation)
◇ Morphism (group homomorphisms)
◇ Identity (neutral element ‘e’)

3. SINGAPOREAN Category
◇ Objects (Singapore citizens)
◇ Structure (multi-racial)
◇ Morphism (kiasu-ism)
◇ Identity morphism (I = ME-ism = 令伯 ‘lim-peh-ism’)

Lecture 2: [Video]
◇ Functor: morphism between Categories
◇ Diagrams: Morphisms uses arrows –> (Functors use double arrows ==>)
◇ Commute
Special Types of Functors:
Full (Surjective)/ Faithful (Injective) /Fully Faithful (Bijective) / Embedding (Fully Faithful + Objects injective)

Yoneda’s Lemma (Deep and Trivial Philosophy)

◇ Intuitively, All objects are defined by its actions (or by all the actions acting upon it).

◇ Hence, it is more important to study the actions / relationships (Functors) than the object (Category) itself.

Formal definition explained below (last 5 mins of Tom Galatta’s video,

image

Special Type of Morphisms
Epi(c): right cancellable f
gof = hof => g = h
Mono (monics) : left cancellable f
fog = foh => g = h

Concrete Categories: Objects are Sets, morphisms are set functions.
Otherwise, they are called Abstract Categories

Notes: Analogy of Yoneda’s Lemma

This corresponds to the old saying, 

“A man is judged by (all) his actions“.

《易·系辞上》:“言行,君子之枢机。

圣经里也是如此说:

image


原来最高深的数学( Category Theory) 回归 到 哲学(易经, 宗教)。
数学只是把它 符号化 / 规律 化, 一个tool, 容易推理, 从人类看得见的空间到看不见的无限大(或无限小)的大千世界。

Introduction to Category Theory 范畴论

[Source: ] All lectures & exercises here:
http://ureddit.com/class/36451

image

Introduction to Category Theory 1:

Course Overview:

Category Theory = Abstract Algebra of Functions

Lambda Calculus = Calculus of Functions

Lambda Calculus = Category

History:

image

image

\cap \bigotimes

Introduction to Category Theory (2) Monoids 么群


Introduction to Category Theory (3)
Real lecture begins from here: Categories, Functors, Natural Transformation:

1. Category Definition:

image

1a) Examples of Categories:
image

Excellent example on “Natural Transformation“:

image

Ref: Classic Textbook

image

范畴论 Category Theory :
image