Yet another category of setoids with equality on objects

TL;DR

This paper compares two categories of setoids with equality on objects, proves their isomorphism, and shows the full image of a category along an E-functor into an E-category is also a category, simplifying formalizations in proof assistants.

Contribution

It introduces and proves the isomorphism between two different constructions of categories of setoids with equality on objects, and demonstrates a new result about categories along E-functors.

Findings

The two categories of setoids are isomorphic.

The second category's arrows are simpler due to disappearance of transportation maps.

Full image of a category along an E-functor into an E-category is a category.

Abstract

When formalizing mathematics in (generalized predicative) constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family $F$ of setoids. The objects of the categories are the index setoid $I$ of the family, whereas the definition of arrows differs. The first category has for arrows triples $(a,b,f:F(a) \to F(b))$ where $f$ is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by $F$) makes them equal. In the second category the arrows are triples $(a,b,R \hookrightarrow \Sigma(I,F)^2)$ where $R$ is a total functional relation between the subobjects $F(a), F(b) \hookrightarrow \Sigma(I,F)$ of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is category.