Skip to content

Comment on Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Comments

I asked Gemini AI what the current state of research was for attempts at unifying all of the operators in Mathematics into a single unified operator...

I received several answers including Category Theory (everything reduces down to a single operation called a 'composition'), Lambda Calculus (everything reduces down to function application), Formal Rewriting Systems / Symbol Substitution / Post Canonical System / Markov Algorithm (everything reduces to a single operation: string rewriting, matching a pattern of symbols and replacing it with another. Turing Machines, for example, exist within this space...)

And I also received the following:

"Homotopy Type Theory (Paths as Transformations)

In contemporary foundational mathematics, Homotopy Type Theory (HoTT)—championed by the late Vladimir Voevodsky and a global community of mathematicians—redefines equality itself as a transformation. The Core Idea: In HoTT, statements of equality (a = b) are not static truth values; they are paths (or continuous transformations) living in a higher-dimensional space.

The Reduction: Logical proofs, algebraic manipulations, and geometric deformations are all unified under the concept of "path induction." Proving that two mathematical structures are equivalent is equivalent to finding a continuous path of transformation between them."

How interesting! Homotopy Type Theory is definitely novel in this space of ideas...

Related:

https://homotopytypetheory.org/book/

https://homotopytypetheory.org/

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.