`{IsApart B} `{Apart A} `{IsHSet A} `{is_mere_relation A apart} (f: A -> B) (eq_correct : forall x y, x = y <-> f x = f y) (apart_correct : forall x y, x ≶ y <-> f x ≶ f y) : IsApart A. Proof. split. - apply _. - apply _. - intros x y ap. apply apart_correct, symmetry, apart_correct. assumption. - intros x y ap z. apply apart_correct in ap. apply (merely_destruct (cotransitive ap (f z))). intros [?|?];apply tr;[left|right];apply apart_correct;assumption. - intros x y;split. + intros nap. apply eq_correct. apply tight_apart. intros ap. apply nap. apply apart_correct;assumption. + intros e ap. apply apart_correct in ap;revert ap. apply tight_apart. apply eq_correct;assumption. Qed.
Require Import HoTT.Classes.interfaces.abstract_algebra.