-(* ACZEL CATEGORIES: *)
-(* We use typoids with a compatible membership relation *)
-(* The category is intended to be the domain of the membership relation *)
-(* The membership relation is necessary because we need to regard the *)
-(* domain of a propositional function (ie a subset in the predicative *)
-(* setting) as a quantification domain and therefore as a category, but *)
-(* there is no type in CIC representing the domain of a propositional *)
-(* function *)
+(* ACZEL CATEGORIES:
+ - We use typoids with a compatible membership relation
+ - The category is intended to be the domain of the membership relation
+ - The membership relation is necessary because we need to regard the
+ domain of a propositional function (ie a predicative subset) as a
+ quantification domain and therefore as a category, but there is no
+ type in CIC representing the domain of a propositional function
+ - We set up a single equality predicate, parametric on the category,
+ defined as the reflexive, symmetic, transitive and compatible closure
+ 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
+ *)