Grothendieck’s use of equality
Mathematicians and formal methods researchers are grappling with what “equality” should mean when different constructions are treated as “the same” object up to isomorphism, as in Grothendieck-style algebraic geometry. Commenters contrast classical set-theoretic and type-theoretic foundations with homotopy type theory and proof assistants like Lean, debating whether these tools can faithfully capture informal practices such as “canonical” isomorphisms without breaking rigor or usability. The thread highlights how overloading the equals sign (`=`) obscures important distinctions in both pure math and programming, and why making these notions precise is crucial for large-scale formalization of existing mathematics.
Homotopy Type Theory vs Classical Type Theory
- Several comments argue that homotopy type theory (HoTT) gives a clean account of equality, handling many complications raised in the article (e.g., equalities between different constructions like localizations).
- Others counter that HoTT does not automatically solve the practical problem of “canonical isomorphisms” vs arbitrary isomorphisms, and witnesses of equality are not unique.
- There is debate over tool support: one side praises classical choices in popular proof assistants (impredicative
Prop, choice, classical logic, uniqueness of identity proofs) as pragmatic for mainstream mathematics; another finds it disappointing that the community “retreated” from HoTT after it offered promising conceptual solutions. - Some note that even with HoTT, the system doesn’t “do the work for you”: it exposes issues around equality but still requires significant human effort to resolve them.
Canonical Isomorphism, Universal Properties, and Equality
- A recurring theme is the informal use of “canonical isomorphism” in mathematics and how it breaks down under formalization.
- Universal properties are proposed as the right way to define objects (e.g., products, localizations), making “equal up to isomorphism” effectively equal for all properties defined via these universal properties.
- However, comments stress that:
- Not all arguments are purely universal-property-based.
- Different universal-characterizations of “the same” object may need nontrivial proofs of equivalence.
- Mathematicians often silently switch between “a product” and “the product,” or between specific constructions and abstract characterizations.
Overloaded Uses of “=”
- The equality sign is seen as heavily overloaded: definition, identity, plain equality, isomorphism, proportionality, approximation, hypothesis, or equality “in some restricted context.”
- Examples include projective coordinates, equivalence classes, big-O notation, umbral calculus, and probabilistic notation (e.g., i.i.d. random variables with the same law but not literally equal as functions).
- Several commenters highlight that such overloading is intuitive informally but becomes a “footgun” when you try to encode it in proof assistants or software.
Type Conversions and Implementation Analogies
- Implicit type conversions in programming are used as an analogy for canonical isomorphisms: integers vs rationals vs reals vs complex numbers, or data moving through heterogeneous software systems.
- Path dependence of conversion chains is emphasized: different implicit conversion routes between the “same” conceptual objects can yield different results.
- Spreadsheet behavior (numbers vs strings, formatting vs underlying value, floating-point quirks) is cited as a concrete manifestation of equality/representation confusion.
Philosophical and Cognitive Reflections
- Several comments discuss the gap between:
- Our pre-formal, “chimpanzee-brain” grasp of concepts like number.
- The formal languages (sets, types, axioms) we use to represent them.
- There is extended back-and-forth on whether mathematical objects “really are” their set-theoretic encodings, or whether these are just interchangeable maps of an underlying territory.
- The thread also notes that many logical and metaphysical disputes about equality (numbers, identity, free will, consciousness) may be driven by shifting meanings of symbols rather than substantive disagreement.