proposition: Lemma injectivity_is_monic {X Y : SetoidObject} (f : X ~{Sets}~> Y) : (∀ x y : X, f x ≈ f y → x ≈ y) ↔ Monic f.
proof: Proof. split. - intros HA. constructor. autounfold in *; intros ??? HB. simpl in *; intros. apply HA, HB. - intros HA ?? HB. given (const_x : unit_setoid_object ~{ Sets }~> X). { construct. - apply x. - proper. } given (const_y : unit_setoid_object ~{ Sets }~> X). { construct. - apply y. - proper. } destruct HA. specialize (monic unit_setoid_object const_x const_y). unfold const_x in monic. unfold const_y in monic. simpl in *. eapply monic; eauto. constructor. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Functor Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Initial Category.Structure.Monoidal