proposition: Lemma Equal_Arrs_equiv : Equivalence Equal_Arrs.
proof: Proof. apply Build_Equivalence; [ trivial | apply Build_Partial_equivalence ]; red in |- *; unfold Equal_Arrs in |- *. intro x; auto. intros f g h; exact (Equal_hom_trans (f:=Arrow f) (g:=Arrow g) (h:=Arrow h)). intros f g; exact (Equal_hom_sym (f:=Arrow f) (g:=Arrow g)). Qed.
imports: Category