  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.
