Require Import HoTT.Classes.interfaces.abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Generalizable Variables A B C f g.

Section contents.
Context `{IsApart A}.

Lemma apart_ne x y : PropHolds (x ≶ y) -> PropHolds (x <> y).
A: Type
Aap: Apart A
H: IsApart A
x, y: A
PropHolds (x ≶ y) -> PropHolds (x <> y)
Proof.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
PropHolds (x ≶ y) -> PropHolds (x <> y)
unfold PropHolds.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
x ≶ y -> x <> y
intros ap e;revert ap.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
e: x = y
x ≶ y -> Empty
apply tight_apart.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
e: x = y
x = y assumption.
Qed.

#[export] Instance stable_eq_apartness: forall x y : A, Stable (x = y).
A: Type
Aap: Apart A
H: IsApart A
forall x y : A, Stable (x = y)
Proof.
A: Type
Aap: Apart A
H: IsApart A
forall x y : A, Stable (x = y)
  intros x y.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
Stable (x = y) unfold Stable.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
~~ (x = y) -> x = y
  intros dn.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
dn: ~~ (x = y)
x = y apply tight_apart.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
dn: ~~ (x = y)
~ (x ≶ y)
  intros ap.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
dn: ~~ (x = y)
ap: x ≶ y
Empty apply dn.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
dn: ~~ (x = y)
ap: x ≶ y
x <> y
  apply apart_ne.
A: Type
Aap: Apart A
H: IsApart A
x, y: A
dn: ~~ (x = y)
ap: x ≶ y
PropHolds (x ≶ y) assumption.
Qed.
End contents.

(* Due to bug #2528 *)
#[export]
Hint Extern 3 (PropHolds (_ <> _)) => eapply @apart_ne : typeclass_instances.

Lemma projected_strong_setoid `{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.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
IsApart A
Proof.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
IsApart A
split.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
IsHSet A
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
is_mere_relation A apart
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
Symmetric apart
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
CoTransitive apart
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
forall x y : A, ~ (x ≶ y) <-> x = y
-
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
IsHSet A exact _.
-
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
is_mere_relation A apart exact _.
-
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
Symmetric apart intros x y ap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
ap: x ≶ y
y ≶ x apply apart_correct, symmetry, apart_correct.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
ap: x ≶ y
x ≶ y
  assumption.
-
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
CoTransitive apart intros x y ap z.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
ap: x ≶ y
z: A
hor (x ≶ z) (z ≶ y)
  apply apart_correct in ap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
ap: f x ≶ f y
z: A
hor (x ≶ z) (z ≶ y)
  apply (merely_destruct (cotransitive ap (f z))).
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
ap: f x ≶ f y
z: A
(f x ≶ f z) + (f z ≶ f y) -> hor (x ≶ z) (z ≶ y)
  intros [?|?];apply tr;[left|right];apply apart_correct;assumption.
-
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
forall x y : A, ~ (x ≶ y) <-> x = y intros x y;split.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
~ (x ≶ y) -> x = y
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
x = y -> ~ (x ≶ y)
  +
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
~ (x ≶ y) -> x = y intros nap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
nap: ~ (x ≶ y)
x = y apply eq_correct.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
nap: ~ (x ≶ y)
f x = f y apply tight_apart.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
nap: ~ (x ≶ y)
~ (f x ≶ f y)
    intros ap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
nap: ~ (x ≶ y)
ap: f x ≶ f y
Empty apply nap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
nap: ~ (x ≶ y)
ap: f x ≶ f y
x ≶ y apply apart_correct;assumption.
  +
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
x = y -> ~ (x ≶ y) intros e ap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
e: x = y
ap: x ≶ y
Empty apply apart_correct in ap;revert ap.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
e: x = y
f x ≶ f y -> Empty
    apply tight_apart.
B: Type
Aap: Apart B
H: IsApart B
A: Type
H0: Apart A
IsHSet0: IsHSet A
is_mere_relation0: is_mere_relation A apart
f: A -> B
eq_correct: forall x y : A, x = y <-> f x = f y
apart_correct: forall x y : A, x ≶ y <-> f x ≶ f y
x, y: A
e: x = y
f x = f y apply eq_correct;assumption.
Qed.

Instance sg_apart_mere `{IsApart A} (P : A -> Type)
  : is_mere_relation (sig P) apart.
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
is_mere_relation {x : _ & P x} apart
Proof.
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
is_mere_relation {x : _ & P x} apart
intros.
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
x, y: {x : _ & P x}
IsHProp (x ≶ y) unfold apart,sig_apart.
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
x, y: {x : _ & P x}
IsHProp (x.1 ≶ y.1) exact _.
Qed.

Instance sig_strong_setoid `{IsApart A} (P: A -> Type) `{forall x, IsHProp (P x)}
  : IsApart (sig P).
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
IsApart {x : _ & P x}
Proof.
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
IsApart {x : _ & P x}
apply (projected_strong_setoid (@proj1 _ P)).
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
forall (x : {x : _ & P x}) (y : {x : _ & P x}),
x = y <-> x.1 = y.1
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
forall (x : {x : _ & P x}) (y : {x : _ & P x}),
x ≶ y <-> x.1 ≶ y.1
-
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
forall (x : {x : _ & P x}) (y : {x : _ & P x}),
x = y <-> x.1 = y.1 intros.
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
x, y: {x : _ & P x}
x = y <-> x.1 = y.1 split;apply Sigma.equiv_path_sigma_hprop.
-
A: Type
Aap: Apart A
H: IsApart A
P: A -> Type
H0: forall x : A, IsHProp (P x)
forall (x : {x : _ & P x}) (y : {x : _ & P x}),
x ≶ y <-> x.1 ≶ y.1 intros;apply reflexivity.
Qed.

Section morphisms.
  Context `{IsApart A} `{IsApart B} `{IsApart C}.

  #[export] Instance strong_injective_injective `{!IsStrongInjective (f : A -> B)} :
    IsInjective f.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
IsInjective f
  Proof.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
IsInjective f
  pose proof (strong_injective_mor f).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
X: StrongExtensionality (f : A -> B)
IsInjective f
  intros ? ? e.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
X: StrongExtensionality (f : A -> B)
x, y: A
e: f x = f y
x = y
  apply tight_apart.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
X: StrongExtensionality (f : A -> B)
x, y: A
e: f x = f y
~ (x ≶ y) intros ap.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
X: StrongExtensionality (f : A -> B)
x, y: A
e: f x = f y
ap: x ≶ y
Empty
  apply tight_apart in e.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
X: StrongExtensionality (f : A -> B)
x, y: A
e: ~ (f x ≶ f y)
ap: x ≶ y
Empty apply e.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B
IsStrongInjective0: IsStrongInjective (f : A -> B)
X: StrongExtensionality (f : A -> B)
x, y: A
e: ~ (f x ≶ f y)
ap: x ≶ y
f x ≶ f y
  apply strong_injective;auto.
  Qed.

  (* If a morphism satisfies the binary strong extensionality property, it is
    strongly extensional in both coordinates. *)
  #[export] Instance strong_setoid_morphism_1
    `{!StrongBinaryExtensionality (f : A -> B -> C)} :
    forall z, StrongExtensionality (f z).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
forall z : A, StrongExtensionality (f z)
  Proof.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
forall z : A, StrongExtensionality (f z)
  intros z x y E.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: A
x, y: B
E: f z x ≶ f z y
x ≶ y
  apply (merely_destruct (strong_binary_extensionality f z x z y E)).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: A
x, y: B
E: f z x ≶ f z y
(z ≶ z) + (x ≶ y) -> x ≶ y
  intros [?|?];trivial.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: A
x, y: B
E: f z x ≶ f z y
a: z ≶ z
x ≶ y
  destruct (irreflexivity (≶) z).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: A
x, y: B
E: f z x ≶ f z y
a: z ≶ z
z ≶ z assumption.
  Qed.

  #[export] Instance strong_setoid_morphism_unary_2
    `{!StrongBinaryExtensionality (f : A -> B -> C)} :
    forall z, StrongExtensionality (fun x => f x z).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
forall z : B,
StrongExtensionality (fun x : A => f x z)
  Proof.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
forall z : B,
StrongExtensionality (fun x : A => f x z)
  intros z x y E.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: B
x, y: A
E: f x z ≶ f y z
x ≶ y
  apply (merely_destruct (strong_binary_extensionality f x z y z E)).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: B
x, y: A
E: f x z ≶ f y z
(x ≶ y) + (z ≶ z) -> x ≶ y
  intros [?|?];trivial.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality0: StrongBinaryExtensionality
  (f : A -> B -> C)
z: B
x, y: A
E: f x z ≶ f y z
a: z ≶ z
x ≶ y
  destruct (irreflexivity (≶) z);assumption.
  Qed.

  (* Conversely, if a morphism is strongly extensional in both coordinates, it
    satisfies the binary strong extensionality property. We don't make this an
    instance in order to avoid loops. *)
  Lemma strong_binary_setoid_morphism_both_coordinates
    `{!IsApart A} `{!IsApart B} `{!IsApart C} {f : A -> B -> C}
    `{forall z, StrongExtensionality (f z)} `{forall z, StrongExtensionality (fun x => f x z)}
     : StrongBinaryExtensionality f.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
StrongBinaryExtensionality f
  Proof.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
StrongBinaryExtensionality f
  intros x₁ y₁ x₂ y₂ E.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
hor (x₁ ≶ x₂) (y₁ ≶ y₂)
  apply (merely_destruct (cotransitive E (f x₂ y₁))).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
(f x₁ y₁ ≶ f x₂ y₁) + (f x₂ y₁ ≶ f x₂ y₂) ->
hor (x₁ ≶ x₂) (y₁ ≶ y₂)
  intros [?|?];apply tr.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
a: f x₁ y₁ ≶ f x₂ y₁
((x₁ ≶ x₂) + (y₁ ≶ y₂))%type
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
a: f x₂ y₁ ≶ f x₂ y₂
((x₁ ≶ x₂) + (y₁ ≶ y₂))%type
  -
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
a: f x₁ y₁ ≶ f x₂ y₁
((x₁ ≶ x₂) + (y₁ ≶ y₂))%type left.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
a: f x₁ y₁ ≶ f x₂ y₁
x₁ ≶ x₂ apply (strong_extensionality (fun x => f x y₁));trivial.
  -
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
a: f x₂ y₁ ≶ f x₂ y₂
((x₁ ≶ x₂) + (y₁ ≶ y₂))%type right.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
C: Type
Aap1: Apart C
H1: IsApart C
IsApart0: IsApart A
IsApart1: IsApart B
IsApart2: IsApart C
f: A -> B -> C
H2: forall z : A, StrongExtensionality (f z)
H3: forall z : B,
StrongExtensionality (fun x : A => f x z)
x₁: A
y₁: B
x₂: A
y₂: B
E: f x₁ y₁ ≶ f x₂ y₂
a: f x₂ y₁ ≶ f x₂ y₂
y₁ ≶ y₂ apply (strong_extensionality (f x₂));trivial.
  Qed.

End morphisms.

Section more_morphisms.
  Context `{IsApart A} `{IsApart B}.

  Lemma strong_binary_setoid_morphism_commutative {f : A -> A -> B} `{!Commutative f}
    `{forall z, StrongExtensionality (f z)} : StrongBinaryExtensionality f.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> A -> B
Commutative0: Commutative f
H1: forall z : A, StrongExtensionality (f z)
StrongBinaryExtensionality f
  Proof.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> A -> B
Commutative0: Commutative f
H1: forall z : A, StrongExtensionality (f z)
StrongBinaryExtensionality f
  apply @strong_binary_setoid_morphism_both_coordinates;try exact _.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> A -> B
Commutative0: Commutative f
H1: forall z : A, StrongExtensionality (f z)
forall z : A,
StrongExtensionality (fun x : A => f x z)
  intros z x y.
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> A -> B
Commutative0: Commutative f
H1: forall z : A, StrongExtensionality (f z)
z, x, y: A
f x z ≶ f y z -> x ≶ y
  rewrite !(commutativity _ z).
A: Type
Aap: Apart A
H: IsApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> A -> B
Commutative0: Commutative f
H1: forall z : A, StrongExtensionality (f z)
z, x, y: A
f z x ≶ f z y -> x ≶ y
  apply (strong_extensionality (f z)).
  Qed.
End more_morphisms.

Section default_apart.
  Context `{DecidablePaths A}.

  Instance default_apart : Apart A | 20
    := fun x y =>
      match dec (x = y) with
      | inl _ => false
      | inr _ => true
      end = true.
  Typeclasses Opaque default_apart.

  Instance default_apart_trivial : TrivialApart A (Aap:=default_apart).
A: Type
H: DecidablePaths A
TrivialApart A
  Proof.
A: Type
H: DecidablePaths A
TrivialApart A
  split.
A: Type
H: DecidablePaths A
is_mere_relation A apart
A: Type
H: DecidablePaths A
forall x y : A, x ≶ y <-> x <> y
  -
A: Type
H: DecidablePaths A
is_mere_relation A apart unfold apart,default_apart.
A: Type
H: DecidablePaths A
forall x y : A,
IsHProp
  (match dec (x = y) with
   | inl _ => false
   | inr _ => true
   end = true) exact _.
  -
A: Type
H: DecidablePaths A
forall x y : A, x ≶ y <-> x <> y intros x y;unfold apart,default_apart;split.
A: Type
H: DecidablePaths A
x, y: A
match dec (x = y) with
| inl _ => false
| inr _ => true
end = true -> x <> y
A: Type
H: DecidablePaths A
x, y: A
x <> y ->
match dec (x = y) with
| inl _ => false
| inr _ => true
end = true
    +
A: Type
H: DecidablePaths A
x, y: A
match dec (x = y) with
| inl _ => false
| inr _ => true
end = true -> x <> y intros E.
A: Type
H: DecidablePaths A
x, y: A
E: match dec (x = y) with
| inl _ => false
| inr _ => true
end = true
x <> y destruct (dec (x=y)).
A: Type
H: DecidablePaths A
x, y: A
p: x = y
E: false = true
x <> y
A: Type
H: DecidablePaths A
x, y: A
n: x <> y
E: true = true
x <> y
      *
A: Type
H: DecidablePaths A
x, y: A
p: x = y
E: false = true
x <> y destruct (false_ne_true E).
      *
A: Type
H: DecidablePaths A
x, y: A
n: x <> y
E: true = true
x <> y trivial.
    +
A: Type
H: DecidablePaths A
x, y: A
x <> y ->
match dec (x = y) with
| inl _ => false
| inr _ => true
end = true intros E;destruct (dec (x=y)) as [e|_].
A: Type
H: DecidablePaths A
x, y: A
E: x <> y
e: x = y
false = true
A: Type
H: DecidablePaths A
x, y: A
E: x <> y
true = true
      *
A: Type
H: DecidablePaths A
x, y: A
E: x <> y
e: x = y
false = true destruct (E e).
      *
A: Type
H: DecidablePaths A
x, y: A
E: x <> y
true = true split.
  Qed.

End default_apart.

(* In case we have a decidable setoid, we can construct a strong setoid. Again
  we do not make this an instance as it will cause loops *)
Section dec_setoid.
  Context `{TrivialApart A} `{DecidablePaths A}.

  (* Not Global in order to avoid loops *)
  Instance ne_apart x y : PropHolds (x <> y) -> PropHolds (x ≶ y).
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
PropHolds (x <> y) -> PropHolds (x ≶ y)
  Proof.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
PropHolds (x <> y) -> PropHolds (x ≶ y)
  intros ap.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ap: PropHolds (x <> y)
PropHolds (x ≶ y) apply trivial_apart.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ap: PropHolds (x <> y)
x <> y
  assumption.
  Qed.

  #[export] Instance dec_strong_setoid: IsApart A.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
IsApart A
  Proof.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
IsApart A
  split.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
IsHSet A
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
is_mere_relation A apart
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
Symmetric apart
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
CoTransitive apart
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
forall x y : A, ~ (x ≶ y) <-> x = y
  -
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
IsHSet A exact _.
  -
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
is_mere_relation A apart exact _.
  -
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
Symmetric apart intros x y ne.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x ≶ y
y ≶ x
    apply trivial_apart.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x ≶ y
y <> x apply trivial_apart in ne.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
y <> x
    intros e;apply ne,symmetry,e.
  -
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
CoTransitive apart hnf.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
forall x y : A,
x ≶ y -> forall z : A, hor (x ≶ z) (z ≶ y) intros x y ne z.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x ≶ y
z: A
hor (x ≶ z) (z ≶ y)
    apply trivial_apart in ne.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
hor (x ≶ z) (z ≶ y)
    destruct (dec (x=z)) as [e|ne'];[destruct (dec (z=y)) as [e'|ne']|].
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
e: x = z
e': z = y
hor (x ≶ z) (z ≶ y)
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
e: x = z
ne': z <> y
hor (x ≶ z) (z ≶ y)
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
ne': x <> z
hor (x ≶ z) (z ≶ y)
    +
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
e: x = z
e': z = y
hor (x ≶ z) (z ≶ y) destruct ne.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y, z: A
e: x = z
e': z = y
x = y path_via z.
    +
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
e: x = z
ne': z <> y
hor (x ≶ z) (z ≶ y) apply tr;right.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
e: x = z
ne': z <> y
z ≶ y apply trivial_apart.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
e: x = z
ne': z <> y
z <> y assumption.
    +
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
ne': x <> z
hor (x ≶ z) (z ≶ y) apply tr;left.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
ne': x <> z
x ≶ z  apply trivial_apart.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
ne: x <> y
z: A
ne': x <> z
x <> z assumption.
  -
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
forall x y : A, ~ (x ≶ y) <-> x = y intros x y;split.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
~ (x ≶ y) -> x = y
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
x = y -> ~ (x ≶ y)
    +
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
~ (x ≶ y) -> x = y intros nap.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
nap: ~ (x ≶ y)
x = y
      destruct (dec (x=y));auto.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
nap: ~ (x ≶ y)
n: x <> y
x = y
      destruct nap.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
n: x <> y
x ≶ y apply trivial_apart;trivial.
    +
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
x = y -> ~ (x ≶ y) intros e.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
e: x = y
~ (x ≶ y)
      intros nap.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
e: x = y
nap: x ≶ y
Empty apply trivial_apart in nap.
A: Type
Aap: Apart A
H: TrivialApart A
H0: DecidablePaths A
x, y: A
e: x = y
nap: x <> y
Empty auto.
  Qed.
End dec_setoid.

(* And a similar result for morphisms *)
Section dec_setoid_morphisms.
  Context `{IsApart A} `{!TrivialApart A} `{IsApart B}.

  Instance dec_strong_morphism (f : A -> B) :
    StrongExtensionality f.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> B
StrongExtensionality f
  Proof.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> B
StrongExtensionality f
  intros x y E.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> B
x, y: A
E: f x ≶ f y
x ≶ y apply trivial_apart.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> B
x, y: A
E: f x ≶ f y
x <> y
  intros e.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
f: A -> B
x, y: A
E: f x ≶ f y
e: x = y
Empty
  apply tight_apart in E;auto.
  Qed.

  Context `{!TrivialApart B}.

  Instance dec_strong_injective (f : A -> B) `{!IsInjective f} :
    IsStrongInjective f.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
IsStrongInjective f
  Proof.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
IsStrongInjective f
  split; try exact _.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
forall x y : A, x ≶ y -> f x ≶ f y
  intros x y.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
x ≶ y -> f x ≶ f y
  intros ap.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
ap: x ≶ y
f x ≶ f y
  apply trivial_apart in ap.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
ap: x <> y
f x ≶ f y apply trivial_apart.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
ap: x <> y
f x <> f y intros e.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
ap: x <> y
e: f x = f y
Empty
  apply ap.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
ap: x <> y
e: f x = f y
x = y apply (injective f).
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
f: A -> B
IsInjective0: IsInjective f
x, y: A
ap: x <> y
e: f x = f y
f x = f y assumption.
  Qed.

  Context `{IsApart C}.

  Instance dec_strong_binary_morphism (f : A -> B -> C) :
    StrongBinaryExtensionality f.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality f
  Proof.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
StrongBinaryExtensionality f
  intros x1 y1 x2 y2 hap.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
hor (x1 ≶ x2) (y1 ≶ y2)
  apply (merely_destruct (cotransitive hap (f x2 y1)));intros [h|h];apply tr.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x1 y1 ≶ f x2 y1
((x1 ≶ x2) + (y1 ≶ y2))%type
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x2 y1 ≶ f x2 y2
((x1 ≶ x2) + (y1 ≶ y2))%type
  -
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x1 y1 ≶ f x2 y1
((x1 ≶ x2) + (y1 ≶ y2))%type left.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x1 y1 ≶ f x2 y1
x1 ≶ x2 apply trivial_apart.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x1 y1 ≶ f x2 y1
x1 <> x2
    intros e.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x1 y1 ≶ f x2 y1
e: x1 = x2
Empty
    apply tight_apart in h;auto.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x1 y1 ≶ f x2 y1
e: x1 = x2
X: forall x y : C, x = y -> ~ (x ≶ y)
f x1 y1 = f x2 y1
    exact (ap (fun x => f x y1) e).
  -
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x2 y1 ≶ f x2 y2
((x1 ≶ x2) + (y1 ≶ y2))%type right.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x2 y1 ≶ f x2 y2
y1 ≶ y2 apply trivial_apart.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x2 y1 ≶ f x2 y2
y1 <> y2
    intros e.
A: Type
Aap: Apart A
H: IsApart A
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
H0: IsApart B
TrivialApart1: TrivialApart B
C: Type
Aap1: Apart C
H1: IsApart C
f: A -> B -> C
x1: A
y1: B
x2: A
y2: B
hap: f x1 y1 ≶ f x2 y2
h: f x2 y1 ≶ f x2 y2
e: y1 = y2
Empty
    apply tight_apart in h;auto.
  Qed.
End dec_setoid_morphisms.