Formalizing equivalences without tears
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908523137335296 |
|---|---|
| author | de Jong, Tom |
| author_facet | de Jong, Tom |
| contents | This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_11501 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formalizing equivalences without tears de Jong, Tom Logic in Computer Science This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory. |
| title | Formalizing equivalences without tears |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2408.11501 |