Homotopy Type Theory: Vladimir Voevodsky

Math Online Tom Circle

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 对应)

View original post

Author: tomcircle

Math amateur

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 )

Facebook photo

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

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: