of the aceq predicate given inside the category. Then we prove the
properties of the equality that usually are axiomatized inside the
category structure. This makes categories easier to use
-*)
+ *)
record AC: Type \def {
ac: Type;
coercion ac.
-inductive eq (A:AC) : A \to A \to Prop \def
- | eq_refl: \forall a. acin ? a \to eq A a a.
+inductive eq (A:AC) (a:A): A \to Prop \def
+ | eq_refl: acin ? a \to eq A a a.
+(* | eq_sing_r: \forall b,c. eq A a b \to aceq A b c \to eq A a c. *)