Grothendieck's Equality vs Voevodsky's Equality

TL;DR

This paper explores the nature of equality in Homotopy Type Theory, comparing it with Grothendieck's approach, and investigates its implications for formalising various mathematical structures and theories.

Contribution

It provides a comparative analysis of equality concepts in Homotopy Type Theory and Grothendieck's framework, with applications to algebra and cohomology.

Findings

Comparison of equality notions in different frameworks

Application to cohomology and flatness criteria

Insights into formalising mathematics efficiently

Abstract

We discuss how canonical and universal constructions, properties and characterizations interact with equality in the framework of Homotopy Type Theory, comparing it with Grothendieck's use of equality and shedding further light on (efficient) formalisation of mathematics. This is achieved by investigating examples that range from monoids, groups, rings and modules to cohomology theories in the category of modules over commutative rings and culminate in a cohomological criterion of flatness.