Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.00747 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912995231137792 |
|---|---|
| author | Eckl, Thomas |
| author_facet | Eckl, Thomas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_00747 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Grothendieck's Equality vs Voevodsky's Equality Eckl, Thomas Logic Algebraic Geometry 03A05 (Primary), 14A05 (Secondary) 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. |
| title | Grothendieck's Equality vs Voevodsky's Equality |
| topic | Logic Algebraic Geometry 03A05 (Primary), 14A05 (Secondary) |
| url | https://arxiv.org/abs/2604.00747 |