From HoTT Require Import ExcludedMiddle canonical_names.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 X : HSet,
hexists (fun A : Ordinal => InjectsInto X 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 A : Ordinal => InjectsInto Y A)
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 A : Ordinal => InjectsInto Y A)
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 A : Ordinal => InjectsInto Y A)
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 f : X -> Y => forall x : X, R x (f x)) apply tr.
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
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
{f : X -> Y & forall x : X, R x (f x)} unshelve eexists.
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
HA: InjectsInto Y A
f: Y -> A
Hf: IsInjective f
X -> 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)
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 A : Ordinal => InjectsInto Y A)
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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
Hy: R x y
merely
  {a : A &
  Build_HProp
    (merely {y : Y & ((f y = a) * R x y)%type})}
        apply tr.
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
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}
y: Y
Hy: R x y
{a : A &
Build_HProp
  (merely {y : Y & ((f y = a) * R x y)%type})} exists (f 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)
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}
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 A : Ordinal => InjectsInto Y A)
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: 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}
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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
Hy: R x y
((f y = f y) * R x y)%type by split.
      *
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
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 A : Ordinal => InjectsInto Y A)
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: 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
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 A : Ordinal => InjectsInto Y A)
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: 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
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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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 y : 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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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 &
merely
  (R x y *
   (forall y' : Y, R x y' -> f y < f y' \/ f y = f y'))} exists 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)
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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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'))%type split; trivial.
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
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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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 A : Ordinal => InjectsInto Y A)
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: 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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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 {y : Y & ((f y = f y') * R x y)%type}) apply tr.
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
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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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'
{y : Y & ((f y = f y') * R x y)%type} exists 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)
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}
y: Y
H2: forall b : A,
Build_HProp
  (merely {y : Y & ((f y = b) * R x y)%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')%type split; trivial.
    +
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
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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y') ->
y = y' intros [H1 H2].
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
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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
y = y'
      eapply merely_destruct; try apply Hy'.
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
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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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: 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, y': Y
Hy: merely
  (R x y *
   (forall y' : Y,
    R x y' -> f y < f y' \/ f y = f y'))
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' : Y, R x y' -> f y < f y' \/ f y = f y'
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 A : Ordinal => InjectsInto Y A)
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 & (... = 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 & (... * ...)%type}) ->
                      a < b \/ a = b)) =>
          (fun
             (H1 : Build_HProp
                     (merely
                        {y : Y &
                        ((...) * R x0 y)%type}))
             (H2 : forall b : A,
                   Build_HProp
                     (merely {y : Y & (...)%type}) ->
                   a < b \/ a = b) =>
           merely_destruct H1
             (fun X1 : {y : Y & ((...) * R x0 y)%type}
              =>
              (fun (y : Y) (proj3 : ... * ...) =>
               (... => ...) (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' * (...) =>
                (fun ... ... => Hf y y' ...) (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 A : Ordinal => InjectsInto Y A)
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: X
R x
  ((fun x : X =>
    let HR' :=
      let HAR :=
        ordinal_has_minimal_hsolutions A
          (fun a : A =>
           Build_HProp
             (merely
                {y : Y & ((f y = a) * R x y)%type}))
        in
      merely_destruct
        (HAR
           (merely_destruct (HR x)
              (fun X0 : {x0 : Y & R x x0} =>
               (fun (y : Y) (Hy : R x 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 x y}) *
                 (forall b : A,
                  Build_HProp
                    (merely
                       {y : Y & (f y = b) * R x y}) ->
                  a < b \/ a = b))%type} =>
         (fun (a : A)
            (proj2 : Build_HProp
                       (merely
                          {y : Y &
                          ((f y = a) * R x y)%type}) *
                     (forall b : A,
                      Build_HProp
                        (merely
                           {y : Y &
                           ((...) * R x y)%type}) ->
                      a < b \/ a = b)) =>
          (fun
             (H1 : Build_HProp
                     (merely
                        {y : Y &
                        ((... = a) * R x y)%type}))
             (H2 : forall b : A,
                   Build_HProp
                     (merely
                        {y : Y & (... * ...)%type}) ->
                   a < b \/ a = b) =>
           merely_destruct H1
             (fun
                X1 : {y : Y &
                     ((... = a) * R x y)%type} =>
              (fun (y : Y) (proj3 : (...) * R x y) =>
               (fun ... =>
                internal_paths_rew ... ... 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 x y *
            (forall y' : Y,
             R x y' -> f y < f y' \/ f y = f y')))
        (fun x0 : Y =>
         istrunc_truncation (-1)
           (R x x0 *
            (forall y' : Y,
             R x y' -> f x0 < f y' \/ f x0 = f y')))
        (HR',
        (fun (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)))
         =>
         merely_destruct Hy
           (fun
              X0 : R x y *
                   (forall y'0 : Y,
                    R x y'0 ->
                    f y < f y'0 \/ f y = f y'0) =>
            (fun (H1 : R x y)
               (H2 : forall y'0 : Y,
                     R x y'0 ->
                     f y < f y'0 \/ f y = f y'0) =>
             merely_destruct Hy'
               (fun X1 : R x y' * (forall ..., ...) =>
                (fun (H3 : ...) (H4 : ...) =>
                 Hf y y' (...)) (fst X1) (snd X1)))
              (fst X0) (snd X0)))
        :
        atmost1P
          (fun y : Y =>
           merely
             (R x y *
              (forall y' : Y,
               R x y' -> f y < f y' \/ f y = f y'))))
      in
    (fun (y : Y)
       (_ : (fun y0 : Y =>
             trunctype_type
               (merely
                  (R x y0 *
                   (forall y' : Y,
                    R x y' ->
                    f y0 < f y' \/ f y0 = f y')))) y)
     => y) s.1 s.2) x) cbn.
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
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) (... + ...)))})
              (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
                                 (...) lt (...) (...)
                                 (...))
                        | inr p =>
                            internal_paths_rew_r
                              (fun ... => ... = t)
                              1%path p
                        end)
                 | inr p => p
                 end)))))).1 destruct iota as [y Hy].
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
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 A : Ordinal => InjectsInto Y A)
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: 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.