proposition: Lemma Equal_PULB_mor_equiv : Equivalence Equal_PULB_mor.
proof: Proof. apply Build_Equivalence; [ trivial | apply Build_Partial_equivalence ]; red in |- *; unfold Equal_PULB_mor in |- *; simpl in |- *; auto. Qed.
imports: Category BasicTypes