proposition: Lemma Equal_Functor_equiv : Equivalence Equal_Functor.
proof: Proof. apply Build_Equivalence; unfold Equal_Functor in |- *. auto. apply Build_Partial_equivalence. unfold Transitive in |- *; intros F G H Ass1 Ass2 a b f. apply Equal_hom_trans with (G a) (G b) (FMor G f); auto. auto. Qed.
imports: Setoid_dup1 Hom_Equality