Modest Sets are Equivalent to PERs
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_ | 1866909388081463296 |
|---|---|
| author | Chhabra, Rahul |
| author_facet | Chhabra, Rahul |
| contents | The aim of this article is to give an expository account of the equivalence between modest sets and partial equivalence relations. Our proof is entirely self-contained in that we do not assume any knowledge of categorical realizability. At the heart of the equivalence lies the subquotient construction on a partial equivalence relation. The subquotient construction embeds the category of partial equivalence relations into the category of modest sets. We show that this embedding is a split essentially surjective functor, and thereby, an equivalence of categories. Our development is both constructive and predicative, and employs the language of homotopy type theory. All the mathematics presented in this article has been mechanised in Cubical Agda. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_08421 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Modest Sets are Equivalent to PERs Chhabra, Rahul Category Theory Logic in Computer Science The aim of this article is to give an expository account of the equivalence between modest sets and partial equivalence relations. Our proof is entirely self-contained in that we do not assume any knowledge of categorical realizability. At the heart of the equivalence lies the subquotient construction on a partial equivalence relation. The subquotient construction embeds the category of partial equivalence relations into the category of modest sets. We show that this embedding is a split essentially surjective functor, and thereby, an equivalence of categories. Our development is both constructive and predicative, and employs the language of homotopy type theory. All the mathematics presented in this article has been mechanised in Cubical Agda. |
| title | Modest Sets are Equivalent to PERs |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2411.08421 |