+
+alias symbol "exists" (instance 1) = "CProp2 exists".
+definition full2 ≝
+ λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
+ ∀o1,o2:A.∀f.∃g:arrows2 A o1 o2.F⎽⇒ g =_2 f.
+alias symbol "exists" (instance 1) = "CProp exists".
+
+definition faithful2 ≝
+ λA,B:CAT2.λF:carr3 (arrows3 CAT2 A B).
+ ∀o1,o2:A.∀f,g:arrows2 A o1 o2.F⎽⇒ f =_2 F⎽⇒ g → f =_2 g.
+
+
+notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
+notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
+
+notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
+
+notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.