+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.