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.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s