Homotopy Type Theory as a Framework for Geometric Equality: The Case of Triangles

The language of Euclidean geometry traditionally employs multiple, informally distinguished no tions of equality, such as ”congruence” and ”similarity.” This paper introduces a formal framework using Homotopy Type Theory (HoTT) to precisely define and differentiate these concepts. By in terpreting geometric figures as types and their equivalences as paths, we show that strict equality, congruence, and similarity for triangles correspond to distinct structures within the HoTT hierar chy. We define a type ‘Triangle‘ and formalize its identity type. Crucially, we introduce a higher inductive type ‘TriangleShape‘ to represent the moduli space of triangles, where paths correspond to congruences. We leverage the univalence axiom to establish a formal equivalence between the type of congruences and the identity type of ‘TriangleShape‘. This framework not only resolves foundational ambiguities but also has applications in improving geometry education, automated theorem proving, and spatial reasoning in AI.