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.

…

…

…