Homotopy Type Theory: Vladimir Voevodsky

A self-study Math genius Vladimir Voevodsky, Fields Medalist, Russian.

Voevodsky borrowed idea from Computer Science (“Interface” =hide implementation details) to Math, and vice-versa, from Math to Computer Science :
Homotopy Type Theory (HoTT)

Result: Computer to prove math theorems.

Computer Science Idea:

  • Hiding Implementation Detail
  • Black Box “Interface”
  • Type (类) : Boolean, Integer, String, … (stronger structure than "Set" 集合)

Math Idea (Abstract Geometry : Algebraic Geometry) :

  • Homotopy (同伦)
  • eg. Cup ~ Donut, both are homotopic or same “Type” (in Computer)
  • Isomorphism is Equality “=”
  • Homotopy Type Theory (HoTT):
    • Univalent Theorem: both objects are considered “=” if they are isomorphic (prove if 1-to-1 correspondence 对应)


One thought on “Homotopy Type Theory: Vladimir Voevodsky

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