Grothendieck's Equality vs Voevodsky's Equality

Thomas Eckl

We discuss how canonical and universal constructions, properties and characterizations interact with equality in the framework of Homotopy Type Theory, comparing it with Grothendie…