From HoTT Require Import ExcludedMiddle canonical_names.From HoTT Require Import ExcludedMiddle canonical_names.
From HoTT Require Import HIT.unique_choice.
From HoTT Require Import Spaces.Card.

From HoTT.Sets Require Import Ordinals.

Local Open Scope hprop_scope.

(** * Set-theoretic formulation of the axiom of choice (AC) *)

Monomorphic Axiom Choice : Type0.
Existing Class Choice.

Definition Choice_type :=
  forall (X Y : HSet) (R : X -> Y -> HProp), (forall x, hexists (R x)) -> hexists (fun f => forall x, R x (f x)).

Axiom AC : forall `{Choice}, Choice_type.

Instance is_global_axiom_propresizing : IsGlobalAxiom Choice := {}.



(** * The well-ordering theorem implies AC *)

Lemma WO_AC {LEM : ExcludedMiddle} :
  (forall (X : HSet), hexists (fun (A : Ordinal) => InjectsInto X A)) -> Choice_type.
LEM: ExcludedMiddle
(forall X : HSet, hexists (fun A : Ordinal => InjectsInto X A)) ->
Choice_type
Proof.
LEM: ExcludedMiddle
(forall X : HSet, hexists (fun A : Ordinal => InjectsInto X A)) ->
Choice_type
  intros H X Y R HR.
LEM: ExcludedMiddle
H: forall X0 : HSet, hexists (fun A : Ordinal => InjectsInto X0 A)
X, Y: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
hexists (fun f : X -> Y => forall x : X, R x (f x)) specialize (H Y).
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A : Ordinal => InjectsInto Y A)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
hexists (fun f : X -> Y => forall x : X, R x (f x))
  eapply merely_destruct; try exact H.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A : Ordinal => InjectsInto Y A)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
{A : Ordinal & InjectsInto Y A} ->
hexists (fun f : X -> Y => forall x : X, R x (f x))
  intros [A HA].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
hexists (fun f : X -> Y => forall x : X, R x (f x)) eapply merely_destruct; try exact HA.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
Injection Y A -> hexists (fun f : X -> Y => forall x : X, R x (f x))
  intros [f Hf].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
hexists (fun f0 : X -> Y => forall x : X, R x (f0 x)) apply tr.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
{f0 : X -> Y & forall x : X, R x (f0 x)} unshelve eexists.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
X -> Y
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
forall x : X, R x (?f x)
  -
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
X -> Y intros x.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
Y assert (HR' : hexists (fun y => merely (R x y * forall y', R x y' -> f y < f y' \/ f y = f y'))).
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
Y
    +
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y'))) pose proof (HAR := ordinal_has_minimal_hsolutions A (fun a => Build_HProp (merely (exists y, f y = a /\ R x y)))).
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y : Y & ((f y = a0) * R x y)%type})) a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) b ->
    a < b \/ a = b))%type}
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
      eapply merely_destruct; try apply HAR.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y : Y & ((f y = a0) * R x y)%type})) a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) b ->
    a < b \/ a = b))%type}
merely {a : A & Build_HProp (merely {y : Y & ((f y = a) * R x y)%type})}
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y : Y & ((f y = a0) * R x y)%type})) a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) b ->
    a < b \/ a = b))%type}
{a : A &
(Build_HProp (merely {y : Y & (f y = a) * R x y}) *
 (forall b : A,
  Build_HProp (merely {y : Y & (f y = b) * R x y}) -> a < b \/ a = b))%type} ->
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
      *
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y : Y & ((f y = a0) * R x y)%type})) a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) b ->
    a < b \/ a = b))%type}
merely {a : A & Build_HProp (merely {y : Y & ((f y = a) * R x y)%type})} eapply merely_destruct; try exact (HR x).
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y : Y & ((f y = a0) * R x y)%type})) a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) b ->
    a < b \/ a = b))%type}
{x0 : Y & R x x0} ->
merely {a : A & Build_HProp (merely {y : Y & ((f y = a) * R x y)%type})} intros [y Hy].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
Hy: R x y
merely {a : A & Build_HProp (merely {y0 : Y & ((f y0 = a) * R x y0)%type})}
        apply tr.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
Hy: R x y
{a : A & Build_HProp (merely {y0 : Y & ((f y0 = a) * R x y0)%type})} exists (f y).
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
Hy: R x y
Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type}) apply tr.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
Hy: R x y
{y0 : Y & ((f y0 = f y) * R x y0)%type} exists y.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
Hy: R x y
(f y = f y) * R x y by split.
      *
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y : Y & ((f y = a0) * R x y)%type})) a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y : Y & (f y = a0) * R x y})) b ->
    a < b \/ a = b))%type}
{a : A &
(Build_HProp (merely {y : Y & (f y = a) * R x y}) *
 (forall b : A,
  Build_HProp (merely {y : Y & (f y = b) * R x y}) -> a < b \/ a = b))%type} ->
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y'))) intros [a [H1 H2]].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a0 : A &
  (fun a1 : A => Build_HProp (merely {y : Y & ((f y = a1) * R x y)%type})) a0} ->
merely
  {a0 : A &
  ((fun a1 : A => Build_HProp (merely {y : Y & (f y = a1) * R x y})) a0 *
   (forall b : A,
    (fun a1 : A => Build_HProp (merely {y : Y & (f y = a1) * R x y})) b ->
    a0 < b \/ a0 = b))%type}
a: A
H1: Build_HProp (merely {y : Y & ((f y = a) * R x y)%type})
H2: forall b : A,
Build_HProp (merely {y : Y & ((f y = b) * R x y)%type}) -> a < b \/ a = b
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y'))) eapply merely_destruct; try exact H1.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a0 : A &
  (fun a1 : A => Build_HProp (merely {y : Y & ((f y = a1) * R x y)%type})) a0} ->
merely
  {a0 : A &
  ((fun a1 : A => Build_HProp (merely {y : Y & (f y = a1) * R x y})) a0 *
   (forall b : A,
    (fun a1 : A => Build_HProp (merely {y : Y & (f y = a1) * R x y})) b ->
    a0 < b \/ a0 = b))%type}
a: A
H1: Build_HProp (merely {y : Y & ((f y = a) * R x y)%type})
H2: forall b : A,
Build_HProp (merely {y : Y & ((f y = b) * R x y)%type}) -> a < b \/ a = b
{y : Y & ((f y = a) * R x y)%type} ->
hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
        intros [y [<- Hy]].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
hexists
  (fun y0 : Y =>
   merely (R x y0 * (forall y' : Y, R x y' -> f y0 < f y' \/ f y0 = f y'))) apply tr.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
{y0 : Y &
merely (R x y0 * (forall y' : Y, R x y' -> f y0 < f y' \/ f y0 = f y'))} exists y.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')) apply tr.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y') split; trivial.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
forall y' : Y, R x y' -> f y < f y' \/ f y = f y'
        intros y' Hy'.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
y': Y
Hy': R x y'
f y < f y' \/ f y = f y' apply H2.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
y': Y
Hy': R x y'
Build_HProp (merely {y0 : Y & ((f y0 = f y') * R x y0)%type}) apply tr.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
y': Y
Hy': R x y'
{y0 : Y & ((f y0 = f y') * R x y0)%type} exists y'.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HAR: merely
  {a : A &
  (fun a0 : A => Build_HProp (merely {y0 : Y & ((f y0 = a0) * R x y0)%type}))
    a} ->
merely
  {a : A &
  ((fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) a *
   (forall b : A,
    (fun a0 : A => Build_HProp (merely {y0 : Y & (f y0 = a0) * R x y0})) b ->
    a < b \/ a = b))%type}
y: Y
H2: forall b : A,
Build_HProp (merely {y0 : Y & ((f y0 = b) * R x y0)%type}) ->
f y < b \/ f y = b
H1: Build_HProp (merely {y0 : Y & ((f y0 = f y) * R x y0)%type})
Hy: R x y
y': Y
Hy': R x y'
(f y' = f y') * R x y' split; trivial.
    +
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
Y edestruct (@iota Y) as [y Hy]; try exact y.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
forall x0 : Y, IsHProp (?P x0)
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
hunique ?P 2: split; try exact HR'.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
forall x0 : Y,
IsHProp
  ((fun y : Y =>
    trunctype_type
      (merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y'))))
     x0)
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
atmost1P
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y'))) 1: exact _.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
atmost1P
  (fun y : Y =>
   merely (R x y * (forall y' : Y, R x y' -> f y < f y' \/ f y = f y')))
      intros y y' Hy Hy'.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
y = y'
      eapply merely_destruct; try exact Hy.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0) -> y = y' intros [H1 H2].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
y = y'
      eapply merely_destruct; try apply Hy'.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0) -> y = y' intros [H3 H4].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
y = y' apply Hf.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
f y = f y'
      eapply merely_destruct; try apply (H2 y'); trivial.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
(f y < f y') + (f y = f y') -> f y = f y' intros [H5|H5]; trivial.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
H5: f y < f y'
f y = f y'
      eapply merely_destruct; try apply (H4 y); trivial.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
H5: f y < f y'
(f y' < f y) + (f y' = f y) -> f y = f y' intros [H6| -> ]; trivial.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
H5: f y < f y'
H6: f y' < f y
f y = f y'
      apply Empty_rec.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
H5: f y < f y'
H6: f y' < f y
Empty apply (irreflexive_ordinal_relation _ _ _ (f y)).
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
HR': hexists
  (fun y0 : Y =>
   merely
     (R x y0 * (forall y'0 : Y, R x y'0 -> f y0 < f y'0 \/ f y0 = f y'0)))
y, y': Y
Hy: merely (R x y * (forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0))
Hy': merely (R x y' * (forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0))
H1: R x y
H2: forall y'0 : Y, R x y'0 -> f y < f y'0 \/ f y = f y'0
H3: R x y'
H4: forall y'0 : Y, R x y'0 -> f y' < f y'0 \/ f y' = f y'0
H5: f y < f y'
H6: f y' < f y
f y < f y
      apply (ordinal_transitivity _ (f y')); trivial.
  -
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x : X, hexists (fun x0 : Y => R x x0)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
forall x : X,
R x
  ((fun x0 : X =>
    let HR' :=
      let HAR :=
        ordinal_has_minimal_hsolutions A
          (fun a : A =>
           Build_HProp (merely {y : Y & ((f y = a) * R x0 y)%type}))
        in
      merely_destruct
        (HAR
           (merely_destruct (HR x0)
              (fun X0 : {x1 : Y & R x0 x1} =>
               (fun (y : Y) (Hy : R x0 y) => tr (f y; tr (y; (1%path, Hy))))
                 X0.1 X0.2)))
        (fun
           X0 : {a : A &
                (Build_HProp (merely {y : Y & (f y = a) * R x0 y}) *
                 (forall b : A,
                  Build_HProp (merely {y : Y & (f y = b) * R x0 y}) ->
                  a < b \/ a = b))%type} =>
         (fun (a : A)
            (proj2 : Build_HProp (merely {y : Y & ((f y = a) * R x0 y)%type}) *
                     (forall b : A,
                      Build_HProp
                        (merely {y : Y & ((f y = b) * R x0 y)%type}) ->
                      a < b \/ a = b)) =>
          (fun
             (H1 : Build_HProp (merely {y : Y & ((f y = a) * R x0 y)%type}))
             (H2 : forall b : A,
                   Build_HProp (merely {y : Y & ((f y = b) * R x0 y)%type}) ->
                   a < b \/ a = b) =>
           merely_destruct H1
             (fun X1 : {y : Y & ((f y = a) * R x0 y)%type} =>
              (fun (y : Y) (proj3 : (f y = a) * R x0 y) =>
               (fun fst : f y = a =>
                internal_paths_rew
                  (fun a0 : A =>
                   Build_HProp
                     (merely {y0 : Y & ((f y0 = a0) * R x0 y0)%type}) ->
                   (forall b : A,
                    Build_HProp
                      (merely {y0 : Y & ((f y0 = b) * R x0 y0)%type}) ->
                    a0 < b \/ a0 = b) ->
                   R x0 y ->
                   hexists
                     (fun y0 : Y =>
                      merely
                        (R x0 y0 *
                         (forall y' : Y,
                          R x0 y' -> f y0 < f y' \/ f y0 = f y'))))
                  (fun
                     (_ : Build_HProp
                            (merely {y0 : Y & ((f y0 = f y) * R x0 y0)%type}))
                     (H3 : forall b : A,
                           Build_HProp
                             (merely {y0 : Y & ((f y0 = b) * R x0 y0)%type}) ->
                           f y < b \/ f y = b)
                     (Hy : R x0 y) =>
                   tr
                     (y;
                     tr
                       (Hy,
                       fun (y' : Y) (Hy' : R x0 y') =>
                       H3 (f y') (tr (y'; (1%path, Hy'))))))
                  fst H1 H2)
                 (fst proj3) (snd proj3))
                X1.1 X1.2))
            (fst proj2) (snd proj2))
           X0.1 X0.2)
      in
    let s :=
      iota
        (fun y : Y =>
         merely
           (R x0 y * (forall y' : Y, R x0 y' -> f y < f y' \/ f y = f y')))
        (fun x1 : Y =>
         istrunc_truncation (-1)
           (R x0 x1 * (forall y' : Y, R x0 y' -> f x1 < f y' \/ f x1 = f y')))
        (HR',
        (fun (y y' : Y)
           (Hy : merely
                   (R x0 y *
                    (forall y'0 : Y, R x0 y'0 -> f y < f y'0 \/ f y = f y'0)))
           (Hy' : merely
                    (R x0 y' *
                     (forall y'0 : Y,
                      R x0 y'0 -> f y' < f y'0 \/ f y' = f y'0))) =>
         merely_destruct Hy
           (fun
              X0 : R x0 y *
                   (forall y'0 : Y, R x0 y'0 -> f y < f y'0 \/ f y = f y'0) =>
            (fun (H1 : R x0 y)
               (H2 : forall y'0 : Y, R x0 y'0 -> f y < f y'0 \/ f y = f y'0) =>
             merely_destruct Hy'
               (fun
                  X1 : R x0 y' *
                       (forall y'0 : Y,
                        R x0 y'0 -> f y' < f y'0 \/ f y' = f y'0) =>
                (fun (H3 : R x0 y')
                   (H4 : forall y'0 : Y,
                         R x0 y'0 -> f y' < f y'0 \/ f y' = f y'0) =>
                 Hf y y'
                   (merely_destruct (H2 y' H3)
                      (fun X2 : (f y < f y') + (f y = f y') =>
                       match X2 with
                       | inl l =>
                           (fun H5 : f y < f y' =>
                            merely_destruct (H4 y H1)
                              (fun X3 : (f y' < f y) + (f y' = f y) =>
                               match X3 with
                               | inl l0 =>
                                   (fun H6 : f y' < f y =>
                                    Empty_rec
                                      (irreflexive_ordinal_relation A lt
                                         (ordinal_property A) 
                                         (f y)
                                         (ordinal_transitivity 
                                            (f y) 
                                            (f y') 
                                            (f y) H5 H6)))
                                     l0
                               | inr p =>
                                   (fun p0 : f y' = f y =>
                                    internal_paths_rew_r
                                      (fun t : A => f y = t) 1%path p0)
                                     p
                               end))
                             l
                       | inr p => idmap p
                       end)))
                  (fst X1) (snd X1)))
              (fst X0) (snd X0)))
        :
        atmost1P
          (fun y : Y =>
           merely
             (R x0 y * (forall y' : Y, R x0 y' -> f y < f y' \/ f y = f y'))))
      in
    (fun (y : Y)
       (_ : (fun y0 : Y =>
             trunctype_type
               (merely
                  (R x0 y0 *
                   (forall y' : Y, R x0 y' -> f y0 < f y' \/ f y0 = f y'))))
              y) =>
     y) s.1 s.2) x) intros x.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
R x
  ((fun x0 : X =>
    let HR' :=
      let HAR :=
        ordinal_has_minimal_hsolutions A
          (fun a : A =>
           Build_HProp (merely {y : Y & ((f y = a) * R x0 y)%type}))
        in
      merely_destruct
        (HAR
           (merely_destruct (HR x0)
              (fun X0 : {x1 : Y & R x0 x1} =>
               (fun (y : Y) (Hy : R x0 y) => tr (f y; tr (y; (1%path, Hy))))
                 X0.1 X0.2)))
        (fun
           X0 : {a : A &
                (Build_HProp (merely {y : Y & (f y = a) * R x0 y}) *
                 (forall b : A,
                  Build_HProp (merely {y : Y & (f y = b) * R x0 y}) ->
                  a < b \/ a = b))%type} =>
         (fun (a : A)
            (proj2 : Build_HProp (merely {y : Y & ((f y = a) * R x0 y)%type}) *
                     (forall b : A,
                      Build_HProp
                        (merely {y : Y & ((f y = b) * R x0 y)%type}) ->
                      a < b \/ a = b)) =>
          (fun
             (H1 : Build_HProp (merely {y : Y & ((f y = a) * R x0 y)%type}))
             (H2 : forall b : A,
                   Build_HProp (merely {y : Y & ((f y = b) * R x0 y)%type}) ->
                   a < b \/ a = b) =>
           merely_destruct H1
             (fun X1 : {y : Y & ((f y = a) * R x0 y)%type} =>
              (fun (y : Y) (proj3 : (f y = a) * R x0 y) =>
               (fun fst : f y = a =>
                internal_paths_rew
                  (fun a0 : A =>
                   Build_HProp
                     (merely {y0 : Y & ((f y0 = a0) * R x0 y0)%type}) ->
                   (forall b : A,
                    Build_HProp
                      (merely {y0 : Y & ((f y0 = b) * R x0 y0)%type}) ->
                    a0 < b \/ a0 = b) ->
                   R x0 y ->
                   hexists
                     (fun y0 : Y =>
                      merely
                        (R x0 y0 *
                         (forall y' : Y,
                          R x0 y' -> f y0 < f y' \/ f y0 = f y'))))
                  (fun
                     (_ : Build_HProp
                            (merely {y0 : Y & ((f y0 = f y) * R x0 y0)%type}))
                     (H3 : forall b : A,
                           Build_HProp
                             (merely {y0 : Y & ((f y0 = b) * R x0 y0)%type}) ->
                           f y < b \/ f y = b)
                     (Hy : R x0 y) =>
                   tr
                     (y;
                     tr
                       (Hy,
                       fun (y' : Y) (Hy' : R x0 y') =>
                       H3 (f y') (tr (y'; (1%path, Hy'))))))
                  fst H1 H2)
                 (fst proj3) (snd proj3))
                X1.1 X1.2))
            (fst proj2) (snd proj2))
           X0.1 X0.2)
      in
    let s :=
      iota
        (fun y : Y =>
         merely
           (R x0 y * (forall y' : Y, R x0 y' -> f y < f y' \/ f y = f y')))
        (fun x1 : Y =>
         istrunc_truncation (-1)
           (R x0 x1 * (forall y' : Y, R x0 y' -> f x1 < f y' \/ f x1 = f y')))
        (HR',
        (fun (y y' : Y)
           (Hy : merely
                   (R x0 y *
                    (forall y'0 : Y, R x0 y'0 -> f y < f y'0 \/ f y = f y'0)))
           (Hy' : merely
                    (R x0 y' *
                     (forall y'0 : Y,
                      R x0 y'0 -> f y' < f y'0 \/ f y' = f y'0))) =>
         merely_destruct Hy
           (fun
              X0 : R x0 y *
                   (forall y'0 : Y, R x0 y'0 -> f y < f y'0 \/ f y = f y'0) =>
            (fun (H1 : R x0 y)
               (H2 : forall y'0 : Y, R x0 y'0 -> f y < f y'0 \/ f y = f y'0) =>
             merely_destruct Hy'
               (fun
                  X1 : R x0 y' *
                       (forall y'0 : Y,
                        R x0 y'0 -> f y' < f y'0 \/ f y' = f y'0) =>
                (fun (H3 : R x0 y')
                   (H4 : forall y'0 : Y,
                         R x0 y'0 -> f y' < f y'0 \/ f y' = f y'0) =>
                 Hf y y'
                   (merely_destruct (H2 y' H3)
                      (fun X2 : (f y < f y') + (f y = f y') =>
                       match X2 with
                       | inl l =>
                           (fun H5 : f y < f y' =>
                            merely_destruct (H4 y H1)
                              (fun X3 : (f y' < f y) + (f y' = f y) =>
                               match X3 with
                               | inl l0 =>
                                   (fun H6 : f y' < f y =>
                                    Empty_rec
                                      (irreflexive_ordinal_relation A lt
                                         (ordinal_property A) 
                                         (f y)
                                         (ordinal_transitivity 
                                            (f y) 
                                            (f y') 
                                            (f y) H5 H6)))
                                     l0
                               | inr p =>
                                   (fun p0 : f y' = f y =>
                                    internal_paths_rew_r
                                      (fun t : A => f y = t) 1%path p0)
                                     p
                               end))
                             l
                       | inr p => idmap p
                       end)))
                  (fst X1) (snd X1)))
              (fst X0) (snd X0)))
        :
        atmost1P
          (fun y : Y =>
           merely
             (R x0 y * (forall y' : Y, R x0 y' -> f y < f y' \/ f y = f y'))))
      in
    (fun (y : Y)
       (_ : (fun y0 : Y =>
             trunctype_type
               (merely
                  (R x0 y0 *
                   (forall y' : Y, R x0 y' -> f y0 < f y' \/ f y0 = f y'))))
              y) =>
     y) s.1 s.2) x) cbn.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
R x
  (iota
     (fun y : Y =>
      Trunc (-1)
        (R x y *
         (forall y' : Y, R x y' -> Trunc (-1) ((f y < f y') + (f y = f y')))))
     (fun x0 : Y =>
      istrunc_truncation (-1)
        (R x x0 *
         (forall y' : Y, R x y' -> Trunc (-1) ((f x0 < f y') + (f x0 = f y')))))
     (merely_destruct
        (ordinal_has_minimal_hsolutions A
           (fun a : ordinal_carrier A =>
            Build_HProp (Trunc (-1) {y : Y & ((f y = a) * R x y)%type}))
           (merely_destruct (HR x)
              (fun X0 : {x0 : Y & R x x0} =>
               tr (f X0.1; tr (X0.1; (1%path, X0.2))))))
        (fun
           X0 : {a : ordinal_carrier A &
                (Trunc (-1) {y : Y & (f y = a) * R x y} *
                 (forall b : ordinal_carrier A,
                  Trunc (-1) {y : Y & (f y = b) * R x y} ->
                  Trunc (-1) ((a < b) + (a = b))))%type} =>
         merely_destruct (fst X0.2)
           (fun X1 : {y : Y & ((f y = X0.1) * R x y)%type} =>
            internal_paths_rew
              (fun a : ordinal_carrier A =>
               Trunc (-1) {y : Y & ((f y = a) * R x y)%type} ->
               (forall b : ordinal_carrier A,
                Trunc (-1) {y : Y & ((f y = b) * R x y)%type} ->
                Trunc (-1) ((a < b) + (a = b))) ->
               R x X1.1 ->
               Trunc (-1)
                 {y : Y &
                 Trunc (-1)
                   (R x y *
                    (forall y' : Y,
                     R x y' -> Trunc (-1) ((f y < f y') + (f y = f y'))))})
              (fun (_ : Trunc (-1) {y : Y & ((f y = f X1.1) * R x y)%type})
                 (H2 : forall b : ordinal_carrier A,
                       Trunc (-1) {y : Y & ((f y = b) * R x y)%type} ->
                       Trunc (-1) ((f X1.1 < b) + (f X1.1 = b)))
                 (Hy : R x X1.1) =>
               tr
                 (X1.1;
                 tr
                   (Hy,
                   fun (y' : Y) (Hy' : R x y') =>
                   H2 (f y') (tr (y'; (1%path, Hy'))))))
              (fst X1.2) (fst X0.2) (snd X0.2) (snd X1.2))),
     fun (y y' : Y)
       (Hy : Trunc (-1)
               (R x y *
                (forall y'0 : Y,
                 R x y'0 -> Trunc (-1) ((f y < f y'0) + (f y = f y'0)))))
       (Hy' : Trunc (-1)
                (R x y' *
                 (forall y'0 : Y,
                  R x y'0 -> Trunc (-1) ((f y' < f y'0) + (f y' = f y'0))))) =>
     merely_destruct Hy
       (fun
          X0 : R x y *
               (forall y'0 : Y,
                R x y'0 -> Trunc (-1) ((f y < f y'0) + (f y = f y'0))) =>
        merely_destruct Hy'
          (fun
             X1 : R x y' *
                  (forall y'0 : Y,
                   R x y'0 -> Trunc (-1) ((f y' < f y'0) + (f y' = f y'0))) =>
           Hf y y'
             (merely_destruct (snd X0 y' (fst X1))
                (fun X2 : (f y < f y') + (f y = f y') =>
                 match X2 with
                 | inl l =>
                     merely_destruct (snd X1 y (fst X0))
                       (fun X3 : (f y' < f y) + (f y' = f y) =>
                        match X3 with
                        | inl l0 =>
                            Empty_rec
                              (irreflexive_ordinal_relation
                                 (ordinal_carrier A) lt 
                                 (ordinal_property A) 
                                 (f y)
                                 (ordinal_transitivity 
                                    (f y) (f y') (f y) l l0))
                        | inr p =>
                            internal_paths_rew_r
                              (fun t : ordinal_carrier A => f y = t) 1%path p
                        end)
                 | inr p => p
                 end)))))).1 destruct iota as [y Hy].
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
y: Y
Hy: Trunc (-1)
  (R x y *
   (forall y' : Y, R x y' -> Trunc (-1) ((f y < f y') + (f y = f y'))))
R x y eapply merely_destruct; try exact Hy.
LEM: ExcludedMiddle
Y: HSet
H: hexists (fun A0 : Ordinal => InjectsInto Y A0)
X: HSet
R: X -> Y -> HProp
HR: forall x0 : X, hexists (fun x1 : Y => R x0 x1)
A: Ordinal
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
x: X
y: Y
Hy: Trunc (-1)
  (R x y *
   (forall y' : Y, R x y' -> Trunc (-1) ((f y < f y') + (f y = f y'))))
R x y * (forall y' : Y, R x y' -> Trunc (-1) ((f y < f y') + (f y = f y'))) ->
R x y by intros [].
Qed.