coq - How to understand Setoid definition of category? -

i having trouble understanding following coq definition of categories (defined here), involves setoid. , don't understand why setoid necessary or 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 learned far requires

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

i understand setoid equivalent classes, can't see setoids come in. can please explain definition above , explain difference usual category definition without setoids?

let me quote setoids subsection (sect. 2.4) paper j. gross, a. chlipala, d.i. spivak -- experience implementing performant category-theory library in coq (2014):

a setoid [5] carrier type equipped equivalence relation; map of setoids function between carrier types , proof function respects equivalence relations of domain , codomain. many authors [11, 12, 15, 18] choose use setoid of morphisms, allows definition of category of set(oid)s, category of (small) categories, without assuming functional extensionality, , allows definition of categories objects quotient types.

the source above referring [12] math-classes library. however, authors proceed caveat:

however, there significant overhead associated using setoids everywhere, can lead slower compile times. every type talk needs come relation , proof relation equivalence relation. every function use needs come proof sends equivalent elements equivalent elements. worse, if need equivalence relation on universe of “types equivalence relations,” need provide transport function between equivalent types respects equivalence relations of types.