String diagrams (1 – 5)
2. Natural Transformation:
The most interesting “Category Theory” （范畴论) for Programmers course III by Dr. Bartosz Milewski , a follow-up of last year’s course II.
- Fundamental of Category Theory: Functor, Natural Transformation, etc. (Course II Series)
- (Nice to have) : Basic Haskell Functional Programming Language. (Quick Haskell Tutorial)
1.1: Overview Part 1
Category Theory (CT) = Summary of ALL Mathematics
Functional Programming = Application of CT
- Math originated 3,000 years ago in Geometry by Greek Euclid with Axioms and deductive （演译） Proof-driven Logic.
- Geometry = Geo (Earth) + Metry (Measurement).
- Math evolved from 2-dimensional Euclidean Geometry through 17 CE French Descartes’s Cartesian Geometry using the 13CE Arabic invention “Algebra” in Equations of n dimensions: ,
- Use of Algebra: 1) Evaluation of algebraic equations (in CT: “Functor”) ; 2) Manipulation. eg. Substitution (in CT : “Monad” ), Container (in CT: “Endo-Functor” ), Algebraic Operations (in CT: “Pure, Return, Binding” ).
- Lawvere Theories: unified all definitions of Monoids (from Set to CT)
- Free Monoid = “List” (in Programming). Eg. Concatenation of Lists = new List (Composition, Associative Law) ; Empty List (Unit Law).
- Advance of Math in 21CE comes back to Geometry in new Math branches like Algebraic Geometry, Algebraic Topology, etc.
Note: The only 2 existing human Languages invented were derived from forms & shapes (images) of the mother Earth & Nature:
- Ancient Greek Geometry (3000 years) ;
- Ancient Chinese Pictogram Characters (象形汉字, 3000 years 商朝. 甲骨文 ) .
1.1: Overview Part 2
Keypoints: (just a ‘helicopter’ view of the whole course syllabus)
- Calculus: infinite Product, infinite Sum (co-Product), End, co-End.
- Geometry in “Abstract” aka Topology: “Topos”
- Enriched Category : (2-category) Analogy : complex number makes Trigonometry easy; same does Enriched Category.
- Groupoid => “HTT” : Homotopic Type Theory
2.1 String Diagrams (Part 1)
Composing Natural Transformations (Vertical & Horizontal): (assumed naturality)
2.2 Monad & Adjunction
1. Download BM’s book “Category Theory for Programmers” :
Join John Baez’s Azimuth Math Forum 导读 (Study Tour Guide) in Applied Category Theory (CT):
John Baez (1961-) is the world’s expert in Category Theory. He gave a talk on CT in Hokkaido University last year.
The 导读 is using a book by 2 mathematicians Brenden Fong and David Spivak in “Applied Category Theory” – Download the free book of this course here.
Note: Both John Baez and his wife Lisa Raphals (Professor in Chinese) work now in National University of Singapore – Center of Quantum Technologies & Philosophy, respectively.
Haskell & any FP compiler don’t check the Category Theory proof if your codes (eg. fmap) follow Functor’s Laws (eg. Preserve structure, identity) or Monad’s Laws !
Category Theory can be approved from 2 directions: 1) Pure Math, 2) IT Functional Programming (FP) .
Dr. Eugenia Cheng doesn’t know 2), she comes from 1).
The second video (below) approaches Category Theory from 2): Scala – FP language.