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 *)
+
interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.