# 函数概念并不难，理解“函”字是关键——函数概念如何理解】 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).

(想看更多合你口味的内容，马上下载 今日头条)

# 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

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. # Debate (French): Set Theory vs Category Theory 4. Category, Logic and IT Pierre Cartier’s Key Points:

1. The Roles of Categories in Science and Organisation of Knowledges.
2. Homology <- cohomology (Reversed Arrow)
3. Natural Transformation and Duality of Vector Spaces

# 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”

# 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: Ref:

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.