proposition: Lemma injectivity_is_monic `(f : X → Y) : Injective f ↔ @Monic Sets _ _ f.
proof: Proof. unfold Monic, Injective. split; intros; simpl in *. - extensionality z. apply H. apply (equal_f H0). - pose (fun (_ : unit) => x) as const_x. pose (fun (_ : unit) => y) as const_y. specialize (H unit const_x const_y). unfold const_x in H. unfold const_y in H. apply equal_f in H. + assumption. + extensionality tt. assumption. + constructor. Qed.
imports: Hask.Prelude Hask.Crush Coq.Unicode.Utf8 FunctionalExtensionality