Category theoretic structure of setoids

A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category SetoidSetoid and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category EquivEquiv of sets and classical equivalence relations, extend the above results, and prove that SetoidSetoid as an EquivEquiv-enriched category has a relaxed form of equalisers. We then recall the definition of EE-category, generalising that of EquivEquiv-enriched category, and show that SetoidSetoid as an EE-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.