+interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \eta.f p =
+ (mk_unary_morphism1 s _ f p).
+
+definition hint: Type_OF_category2 SET1 → setoid2.
+ intro; apply (setoid2_of_setoid1 t); qed.
+coercion hint.
+
+definition hint2: Type_OF_category1 SET → objs2 SET1.
+ intro; apply (setoid1_of_setoid t); qed.
+coercion hint2.
+
+(* per il set-indexing vedere capitolo BPTools (foundational tools), Sect. 0.3.4 complete
+ lattices, Definizione 0.9 *)
+(* USARE L'ESISTENZIALE DEBOLE *)
+(*alias symbol "comprehension_by" = "unary morphism comprehension with proof".*)
+record OAlgebra : Type2 := {
+ oa_P :> SET1;
+ oa_leq : binary_morphism1 oa_P oa_P CPROP; (* CPROP is setoid1, CPROP importante che sia small *)