proposition: Lemma Equal_Pmor_equiv : Equivalence Equal_Pmor.
proof: Proof. apply Build_Equivalence. unfold Reflexive, Equal_Pmor in |- *; intro x; split; apply Refl. apply Build_Partial_equivalence. unfold Transitive, Equal_Pmor in |- *; intros x1 x2 x3 H H0. elim H; intros H1 H2; elim H0; intros H3 H4; split. apply Trans with (Hom_l x2); assumption. apply Trans with (Hom_r x2); assumption. unfold Symmetric, Equal_Pmor in |- *; intros x1 x2 H. elim H; intros H1 H2; split; apply Sym; assumption. Qed.
imports: Category SetoidPROD