Grothendieck’s use of equality
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.