# Algebra

2003-09-10T05:42:00Z

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.

## Tags

Russell O’Connor: contact me