How to understand Setoid definition of category?

Question

I am having trouble understanding the following Coq definition of Categories (defined here), which involves Setoid. And I don't understand why Setoid is necessary or its role here.

Class Category O `{!Arrows O} `{∀ x y: O, Equiv (x ⟶ y)}
 `{!CatId O} `{!CatComp O}: Prop :=
  { arrow_equiv :> ∀ x y, Setoid (x ⟶ y)
  ; comp_proper :> ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
  ; comp_assoc :> ArrowsAssociative O
  ; id_l :> ∀ x y, LeftIdentity (comp x y y) cat_id
  ; id_r :> ∀ x y, RightIdentity (comp x x y) cat_id }.
      (* note: no equality on objects. *)

The basic notion of Categories I learned so far only requires that

1. there are arrows between objects,
2. the arrows compose (respects associativity) and
3. identity arrows exist and behave.

I understand that Setoid is about equivalent classes, but I can't see where Setoids come in. Can someone please help explain the definition above and explain the difference from the usual category definition without Setoids?

Answer 1

Let me quote the setoids subsection (sect. 2.4) from a paper by J. Gross, A. Chlipala, D.I. Spivak -- Experience Implementing a Performant Category-Theory Library in Coq (2014):

A setoid [5] is a carrier type equipped with an equivalence relation; a map of setoids is a function between the carrier types and a proof that the function respects the equivalence relations of its domain and codomain. Many authors [11, 12, 15, 18] choose to use a setoid of morphisms, which allows for the definition of the category of set(oid)s, as well as the category of (small) categories, without assuming functional extensionality, and allows for the definition of categories where the objects are quotient types.

The source the above is referring to as [12] is the Math-Classes library. However, then the authors proceed with a caveat:

However, there is significant overhead associated with using setoids everywhere, which can lead to slower compile times. Every type that we talk about needs to come with a relation and a proof that this relation is an equivalence relation. Every function that we use needs to come with a proof that it sends equivalent elements to equivalent elements. Even worse, if we need an equivalence relation on the universe of “types with equivalence relations,” we need to provide a transport function between equivalent types that respects the equivalence relations of those types.