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