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