-definition setoid1_of_REL: REL → setoid ≝ λS. S.
-coercion setoid1_of_REL.
-
-lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → Type_OF_setoid1 ?(*(setoid1_of_SET o1)*).
- [ apply (setoid1_of_SET o1);
- | intros; apply t;]
-qed.
-coercion Type_OF_setoid1_of_REL.
-
-definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
+alias symbol "arrows1_SET" (instance 2) = "'arrows1_SET low".
+definition comprehension: ∀b:REL. (b ⇒_1 CPROP) → Ω^b.
+ apply (λb:REL. λP: b ⇒_1 CPROP. {x | P x});