Modest Sets are Equivalent to PERs

TL;DR

This paper demonstrates the categorical equivalence between modest sets and partial equivalence relations using a constructive, predicative approach within homotopy type theory, with formalization in Cubical Agda.

Contribution

It provides a self-contained, formal proof of the equivalence without assuming categorical realizability, employing the subquotient construction and homotopy type theory.

Findings

Establishes an equivalence of categories between modest sets and PERs.

Uses subquotient construction to embed PERs into modest sets.

Formalized all results in Cubical Agda.

Abstract

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.