+ Definition func_diagonal : Functor C (C ×× C) (fun c => (pair_obj c c)).
+ refine {| fmor := fun a b f => @pair_mor _ _ C _ _ C (pair_obj a a) (pair_obj b b) f f |}.
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ abstract (intros; simpl; repeat split; simpl; auto).
+ Defined.