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:

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

**Prerequisite** knowledge:

- Homotopy
- Type Theory
- Homotopy Type Theory
- Bijection = Isomorphism
- Functional Programming in Category Theory Concept: Monad & Applicative

**Two Key Takeaway Points:**

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

…

…

…