+definition functor2_of_functor2_setoid: ∀S,T. functor2_setoid S T → functor2 S T ≝ λS,T,x.x.
+coercion functor2_of_functor2_setoid.
+
+definition CAT2: category3.
+ constructor 1;
+ [ apply category2;
+ | apply functor2_setoid;
+ | intros; constructor 1;
+ [ apply (λx.x);
+ | intros; constructor 1;
+ [ apply (λx.x);
+ | intros; assumption;]
+ | intros; apply rule #;
+ | intros; apply rule #; ]
+ | intros; constructor 1;
+ [ intros; constructor 1;
+ [ intros; apply (c1 (c o));
+ | intros; constructor 1;
+ [ intro; apply (map_arrows2 ?? c1 ?? (map_arrows2 ?? c ?? c2));
+ | intros; apply (††e); ]
+ | intros; simplify;
+ apply (.= †(respects_id2 : ?));
+ apply (respects_id2 : ?);
+ | intros; simplify;
+ apply (.= †(respects_comp2 : ?));
+ apply (respects_comp2 : ?); ]
+ | intros; intro; simplify;
+ apply (cic:/matita/logic/equality/eq_ind.con ????? (e ?));
+ apply (cic:/matita/logic/equality/eq_ind.con ????? (e1 ?));
+ constructor 1; ]
+ | intros; intro; simplify; constructor 1;
+ | intros; intro; simplify; constructor 1;
+ | intros; intro; simplify; constructor 1; ]
+qed.
+
+definition category2_of_objs3_CAT2: objs3 CAT2 → category2 ≝ λx.x.
+coercion category2_of_objs3_CAT2.
+
+definition functor2_setoid_of_arrows3_CAT2: ∀S,T. arrows3 CAT2 S T → functor2_setoid S T ≝ λS,T,x.x.
+coercion functor2_setoid_of_arrows3_CAT2.
+
+definition unary_morphism_setoid: setoid → setoid → setoid.