Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Grothendieck's Equality vs Voevodsky's Equality

Thomas Eckl

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.

Grothendieck's Equality vs Voevodsky's Equality

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.

Paper Structure

This paper contains 27 sections, 54 theorems, 81 equations.

Table of Contents

  1. Introduction
  2. Equalities in Homotopy Type Theory
  3. Identity Types
  4. Propositions and Sets
  5. Univalence and Function Extensionality
  6. Categories
  7. Universal properties from inductive constructions
  8. Cartesian products
  9. Natural types
  10. Universal Properties from Higher Inductive Constructions
  11. Set quotients
  12. Subsets
  13. Monoids
  14. Groups
  15. Rings and Modules
  16. ...and 12 more sections

Key Result

Proposition 1.3

Equalities $p : A = B$ of sets $A, B$ are in one-to-one correspondence with bijective maps $f : A \rightarrow B$. $\Box$$\blacktriangleleft$$\blacktriangleleft$

Theorems & Definitions (151)

  • Definition 1.1
  • Definition 1.2
  • Proposition 1.3
  • Definition 2.1
  • Proposition 2.2
  • proof
  • Proposition 2.3
  • proof
  • Proposition 2.4
  • proof
  • ...and 141 more