Algebra

I’ve been pointed to a pretty nice algebra package for Coq. Unfortunately it seems to use classical logic in some places. I wonder how hard it would be to turn this into a constructive algebra package? As an example, here is their definition of a category.

Section Category_def1.
Variable Ob:Type.
Variable Hom:Ob -> Ob ->Setoid.
Variable Hom_comp:(a, b, c:Ob)(MAP (cart (Hom b c) (Hom a b)) (Hom a c)).
Variable Hom_id:(a:Ob)(Hom a a).
Definition Hom_comp_assoc :=
   (a, b, c, d:Ob) (f:(Hom a b)) (g:(Hom b c)) (h:(Hom c d))
   (Equal
      ((Hom_comp a b d) (couple ((Hom_comp b c d) (couple h g)) f))
      ((Hom_comp a c d) (couple h ((Hom_comp a b c) (couple g f))))).
Definition Hom_comp_unit_l :=
   (a, b:Ob) (f:(Hom a b))(Equal ((Hom_comp a b b) (couple (Hom_id b) f)) f).
Definition Hom_comp_unit_r :=
   (a, b:Ob) (f:(Hom a b))(Equal ((Hom_comp a a b) (couple f (Hom_id a))) f).
End Category_def1.
Record category: Type := {
   Ob:> Type;
   Hom: Ob -> Ob ->Setoid;
   Hom_comp: (a, b, c:Ob)(MAP (cart (Hom b c) (Hom a b)) (Hom a c));
   Hom_id: (a:Ob)(Hom a a);
   Hom_comp_assoc_prf: (Hom_comp_assoc Hom_comp);
   Hom_comp_unit_l_prf: (Hom_comp_unit_l Hom_comp Hom_id);
   Hom_comp_unit_r_prf: (Hom_comp_unit_r Hom_comp Hom_id) }.

What is interesting is that objects (Ob) are some Type, while homomorphisms from a to b ((Hom a b)) form a Setoid.In classical set theory, I understand that objects can form classes, while the homomorphisms from a to b form sets, but I’m not sure why this is, nor am I sure that this expression in type theory is analogous.