-definition Type1_OF_SET1: Type_OF_category2 SET1 → Type1.
- intro; whd in t; apply (carr1 t);
-qed.
-coercion Type1_OF_SET1.
-
-definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply rule U;
- | intros; apply c;]
-qed.
-coercion Type_OF_setoid1_of_carr.
-
-definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
-coercion carr'. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_objs1.