From HoTT Require Import TruncType ExcludedMiddle abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
From HoTT Require Import Universes.Smallness.
From HoTT Require Import Spaces.Nat.Core Spaces.Card.
From HoTT Require Import Equiv.BiInv.
From HoTT Require Import HIT.unique_choice.

From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.

Open Scope type.
Close Scope trunc_scope.

(* The proof of Sierpinski's results that GCH implies AC given in this file consists of two ingredients:
   1. Adding powers of infinite sets does not increase the cardinality (path_infinite_power).
   2. A variant of Cantor's theorem saying that P(X) <= (X + Y) implies P(X) <= Y for large X (Cantor_injects_injects).
   Those are used to obtain that cardinality-controlled functions are well-behaved in the presence of GCH (Sierpinski), from which we obtain by instantiation with the Hartogs number that every set embeds into an ordinal, which is enough to conclude GCH -> AC (GCH_AC) since the well-ordering theorem implies AC (WO_AC). *)


(** * Constructive equivalences *)

(* For the first ingredient, we establish a bunch of paths and conclude the desired result by equational reasoning. *)

Section Preparation.

Context {UA : Univalence}.

Lemma path_sum_prod X Y Z :
  (X -> Z) * (Y -> Z) = ((X + Y) -> Z).
UA: Univalence
X, Y, Z: Type
(X -> Z) * (Y -> Z) = (X + Y -> Z)
Proof.
UA: Univalence
X, Y, Z: Type
(X -> Z) * (Y -> Z) = (X + Y -> Z)
  apply path_universe_uncurried.
UA: Univalence
X, Y, Z: Type
(X -> Z) * (Y -> Z) <~> (X + Y -> Z) apply equiv_sum_distributive.
Qed.

Lemma path_sum_assoc X Y Z :
  X + (Y + Z) = X + Y + Z.
UA: Univalence
X, Y, Z: Type
X + (Y + Z) = X + Y + Z
Proof.
UA: Univalence
X, Y, Z: Type
X + (Y + Z) = X + Y + Z
  symmetry.
UA: Univalence
X, Y, Z: Type
X + Y + Z = X + (Y + Z) apply path_universe_uncurried.
UA: Univalence
X, Y, Z: Type
X + Y + Z <~> X + (Y + Z) apply equiv_sum_assoc.
Qed.

Lemma path_sum_bool X :
  X + X = Bool * X.
UA: Univalence
X: Type
X + X = Bool * X
Proof.
UA: Univalence
X: Type
X + X = Bool * X
  apply path_universe_uncurried.
UA: Univalence
X: Type
X + X <~> Bool * X srapply equiv_adjointify.
UA: Univalence
X: Type
X + X -> Bool * X
UA: Univalence
X: Type
Bool * X -> X + X
UA: Univalence
X: Type
?f o ?g == idmap
UA: Univalence
X: Type
?g o ?f == idmap
  -
UA: Univalence
X: Type
X + X -> Bool * X exact (fun x => match x with inl x => (true, x) | inr x => (false, x) end).
  -
UA: Univalence
X: Type
Bool * X -> X + X exact (fun x => match x with (true, x) => inl x | (false, x) => inr x end).
  -
UA: Univalence
X: Type
(fun x : X + X =>
 match x with
 | inl x0 => (true, x0)
 | inr x0 => (false, x0)
 end)
o (fun x : Bool * X =>
   let x0 := x in
   let fst := fst x0 in
   let x1 := snd x0 in if fst then inl x1 else inr x1) ==
idmap intros [[]]; reflexivity.
  -
UA: Univalence
X: Type
(fun x : Bool * X =>
 let x0 := x in
 let fst := fst x0 in
 let x1 := snd x0 in if fst then inl x1 else inr x1)
o (fun x : X + X =>
   match x with
   | inl x0 => (true, x0)
   | inr x0 => (false, x0)
   end) == idmap intros []; reflexivity.
Qed.

Lemma path_unit_nat :
  Unit + nat = nat.
UA: Univalence
Unit + nat = nat
Proof.
UA: Univalence
Unit + nat = nat
  apply path_universe_uncurried.
UA: Univalence
Unit + nat <~> nat srapply equiv_adjointify.
UA: Univalence
Unit + nat -> nat
UA: Univalence
nat -> Unit + nat
UA: Univalence
?f o ?g == idmap
UA: Univalence
?g o ?f == idmap
  -
UA: Univalence
Unit + nat -> nat exact (fun x => match x with inl _ => O | inr n => S n end).
  -
UA: Univalence
nat -> Unit + nat exact (fun n => match n with O => inl tt | S n => inr n end).
  -
UA: Univalence
(fun x : Unit + nat =>
 match x with
 | inl _ => 0%nat
 | inr n => n.+1%nat
 end)
o (fun n : nat =>
   match n with
   | 0%nat => inl tt
   | n0.+1%nat => inr n0
   end) == idmap by intros [].
  -
UA: Univalence
(fun n : nat =>
 match n with
 | 0%nat => inl tt
 | n0.+1%nat => inr n0
 end)
o (fun x : Unit + nat =>
   match x with
   | inl _ => 0%nat
   | inr n => n.+1%nat
   end) == idmap by intros [[]|n]. 
Qed.

Lemma path_unit_fun X :
  X = (Unit -> X).
UA: Univalence
X: Type
X = (Unit -> X)
Proof.
UA: Univalence
X: Type
X = (Unit -> X)
  apply path_universe_uncurried.
UA: Univalence
X: Type
X <~> (Unit -> X) apply equiv_unit_rec.
Qed.


(** * Equivalences relying on LEM **)

Context {EM : ExcludedMiddle}.

Lemma path_bool_prop :
  HProp = Bool.
UA: Univalence
EM: ExcludedMiddle
HProp = Bool
Proof.
UA: Univalence
EM: ExcludedMiddle
HProp = Bool
  apply path_universe_uncurried.
UA: Univalence
EM: ExcludedMiddle
HProp <~> Bool srapply equiv_adjointify.
UA: Univalence
EM: ExcludedMiddle
HProp -> Bool
UA: Univalence
EM: ExcludedMiddle
Bool -> HProp
UA: Univalence
EM: ExcludedMiddle
?f o ?g == idmap
UA: Univalence
EM: ExcludedMiddle
?g o ?f == idmap
  -
UA: Univalence
EM: ExcludedMiddle
HProp -> Bool exact (fun P => if LEM P _ then true else false).
  -
UA: Univalence
EM: ExcludedMiddle
Bool -> HProp exact (fun b : Bool => if b then merely Unit else merely Empty).
  -
UA: Univalence
EM: ExcludedMiddle
(fun P : HProp =>
 if LEM P (trunctype_istrunc P) then true else false)
o (fun b : Bool =>
   if b then merely Unit else merely Empty) == idmap intros []; destruct LEM as [H|H]; auto.
UA: Univalence
EM: ExcludedMiddle
H: ~ merely Unit
false = true
UA: Univalence
EM: ExcludedMiddle
H: merely Empty
true = false
    +
UA: Univalence
EM: ExcludedMiddle
H: ~ merely Unit
false = true destruct (H (tr tt)).
    +
UA: Univalence
EM: ExcludedMiddle
H: merely Empty
true = false apply (@merely_destruct Empty); try done.
UA: Univalence
EM: ExcludedMiddle
H: merely Empty
IsHProp (true = false) exact _.
  -
UA: Univalence
EM: ExcludedMiddle
(fun b : Bool =>
 if b then merely Unit else merely Empty)
o (fun P : HProp =>
   if LEM P (trunctype_istrunc P) then true else false) ==
idmap intros P.
UA: Univalence
EM: ExcludedMiddle
P: HProp
(if
  if LEM P (trunctype_istrunc P) then true else false
 then merely Unit
 else merely Empty) = P destruct LEM as [H|H]; apply equiv_path_iff_hprop.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: P
merely Unit <-> P
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: ~ P
merely Empty <-> P
    +
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: P
merely Unit <-> P split; auto.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: P
P -> merely Unit intros _.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: P
merely Unit apply tr.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: P
Unit exact tt.
    +
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: ~ P
merely Empty <-> P split; try done.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: ~ P
merely Empty -> P intros HE.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: ~ P
HE: merely Empty
P apply (@merely_destruct Empty); try done.
UA: Univalence
EM: ExcludedMiddle
P: HProp
H: ~ P
HE: merely Empty
IsHProp P exact _.
Qed.

Lemma path_bool_subsingleton :
  (Unit -> HProp) = Bool.
UA: Univalence
EM: ExcludedMiddle
(Unit -> HProp) = Bool
Proof.
UA: Univalence
EM: ExcludedMiddle
(Unit -> HProp) = Bool
  rewrite <- path_unit_fun.
UA: Univalence
EM: ExcludedMiddle
HProp = Bool exact path_bool_prop.
Qed.

Lemma path_pred_sum X (p : X -> HProp) :
  X = sig p + sig (fun x => ~ p x).
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
X = {x : X & p x} + {x : X & ~ p x}
Proof.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
X = {x : X & p x} + {x : X & ~ p x}
  apply path_universe_uncurried.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
X <~> {x : X & p x} + {x : X & ~ p x} srapply equiv_adjointify.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
X -> {x : X & p x} + {x : X & ~ p x}
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
{x : X & p x} + {x : X & ~ p x} -> X
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
?f o ?g == idmap
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
?g o ?f == idmap
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
X -> {x : X & p x} + {x : X & ~ p x} intros x.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
{x : X & p x} + {x : X & ~ p x} destruct (LEM (p x) _) as [H|H]; [left | right]; by exists x.
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
{x : X & p x} + {x : X & ~ p x} -> X intros [[x _]|[x _]]; exact x.
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
(fun x : X =>
 let s := LEM (p x) (trunctype_istrunc (p x)) in
 match s with
 | inl t => (fun H : p x => inl (x; H)) t
 | inr n => (fun H : ~ p x => inr (x; H)) n
 end)
o (fun X0 : {x : X & p x} + {x : X & ~ p x} =>
   match X0 with
   | inl s =>
       (fun s0 : {x : X & p x} =>
        (fun (x : X) (_ : p x) => x) s0.1 s0.2) s
   | inr s =>
       (fun s0 : {x : X & ~ p x} =>
        (fun (x : X) (_ : ~ p x) => x) s0.1 s0.2) s
   end) == idmap cbn.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
(fun x : {x : X & p x} + {x : X & ~ p x} =>
 match
   LEM
     (p match x with
        | inl s => s.1
        | inr s => s.1
        end)
     (trunctype_istrunc
        (p
           match x with
           | inl s => s.1
           | inr s => s.1
           end))
 with
 | inl t =>
     inl
       (match x with
        | inl s => s.1
        | inr s => s.1
        end; t)
 | inr n =>
     inr
       (match x with
        | inl s => s.1
        | inr s => s.1
        end; n)
 end) == idmap intros [[x Hx]|[x Hx]]; destruct LEM as [H|H]; try contradiction.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: p x
inl (x; H) = inl (x; Hx)
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: ~ p x
inr (x; H) = inr (x; Hx)
    +
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: p x
inl (x; H) = inl (x; Hx) enough (H = Hx) as -> by reflexivity.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: p x
H = Hx apply path_ishprop.
    +
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: ~ p x
inr (x; H) = inr (x; Hx) enough (H = Hx) as -> by reflexivity.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: ~ p x
H = Hx apply path_forall.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
Hx, H: ~ p x
H == Hx by intros HP.
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
(fun X0 : {x : X & p x} + {x : X & ~ p x} =>
 match X0 with
 | inl s =>
     (fun s0 : {x : X & p x} =>
      (fun (x : X) (_ : p x) => x) s0.1 s0.2) s
 | inr s =>
     (fun s0 : {x : X & ~ p x} =>
      (fun (x : X) (_ : ~ p x) => x) s0.1 s0.2) s
 end)
o (fun x : X =>
   let s := LEM (p x) (trunctype_istrunc (p x)) in
   match s with
   | inl t => (fun H : p x => inl (x; H)) t
   | inr n => (fun H : ~ p x => inr (x; H)) n
   end) == idmap cbn.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
(fun x : X =>
 match
   match LEM (p x) (trunctype_istrunc (p x)) with
   | inl t => inl (x; t)
   | inr n => inr (x; n)
   end
 with
 | inl s => s.1
 | inr s => s.1
 end) == idmap intros x.
UA: Univalence
EM: ExcludedMiddle
X: Type
p: X -> HProp
x: X
match
  match LEM (p x) (trunctype_istrunc (p x)) with
  | inl t => inl (x; t)
  | inr n => inr (x; n)
  end
with
| inl s => s.1
| inr s => s.1
end = x by destruct LEM.
Qed.

Definition ran {X Y : Type} (f : X -> Y) :=
  fun y => hexists (fun x => f x = y).

Lemma path_ran {X} {Y : HSet} (f : X -> Y) :
  IsInjective f -> sig (ran f) = X.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
IsInjective f -> {y : Y & ran f y} = X
Proof.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
IsInjective f -> {y : Y & ran f y} = X
  intros Hf.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
{y : Y & ran f y} = X apply path_universe_uncurried.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
{y : Y & ran f y} <~> X srapply equiv_adjointify.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
{y : Y & ran f y} -> X
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
X -> {y : Y & ran f y}
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
?f o ?g == idmap
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
?g o ?f == idmap
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
{y : Y & ran f y} -> X intros [y H].
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
X destruct (iota (fun x => f x = y) _) as [x Hx]; try exact x.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
hunique (fun x : X => f x = y)
    split; try apply H.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
atmost1P (fun x : X => f x = y) intros x x'.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
x, x': X
f x = y -> f x' = y -> x = x' cbn.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
x, x': X
f x = y -> f x' = y -> x = x' intros Hy Hy'.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
x, x': X
Hy: f x = y
Hy': f x' = y
x = x' rewrite <- Hy' in Hy.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
H: ran f y
x, x': X
Hy: f x = f x'
Hy': f x' = y
x = x' by apply Hf.
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
X -> {y : Y & ran f y} intros x.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
x: X
{y : Y & ran f y} exists (f x).
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
x: X
ran f (f x) apply tr.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
x: X
{x0 : X & f x0 = f x} exists x.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
x: X
f x = f x reflexivity.
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
(fun X0 : {y : Y & ran f y} =>
 (fun (y : Y) (H : ran f y) =>
  let s :=
    iota (fun x : X => f x = y)
      (fun x : X => istrunc_paths Y (-1) (f x) y)
      (H,
      (fun x x' : X =>
       (fun (Hy : f x = y) (Hy' : f x' = y) =>
        let Hy0 :=
          internal_paths_rew_r
            (fun y0 : Y => f x = y0) Hy Hy' in
        Hf x x' Hy0)
       :
       f x = y -> f x' = y -> x = x')
      :
      atmost1P (fun x : X => f x = y)) in
  (fun (x : X) (_ : f x = y) => x) s.1 s.2) X0.1 X0.2)
o (fun x : X => (f x; tr (x; 1%path))) == idmap cbn.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
(fun x : X =>
 (iota (fun x0 : X => f x0 = f x)
    (fun x0 : X => istrunc_paths Y (-1) (f x0) (f x))
    (tr (x; 1%path),
    fun (x0 x' : X) (Hy : f x0 = f x)
      (Hy' : f x' = f x) =>
    Hf x0 x'
      (internal_paths_rew_r (fun y : Y => f x0 = y) Hy
         Hy'))).1) == idmap intros x.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
x: X
(iota (fun x0 : X => f x0 = f x)
   (fun x0 : X => istrunc_paths Y (-1) (f x0) (f x))
   (tr (x; 1%path),
   fun (x0 x' : X) (Hy : f x0 = f x)
     (Hy' : f x' = f x) =>
   Hf x0 x'
     (internal_paths_rew_r (fun y : Y => f x0 = y) Hy
        Hy'))).1 = x destruct iota as [x' H].
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
x, x': X
H: f x' = f x
x' = x by apply Hf.
  -
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
(fun x : X => (f x; tr (x; 1%path)))
o (fun X0 : {y : Y & ran f y} =>
   (fun (y : Y) (H : ran f y) =>
    let s :=
      iota (fun x : X => f x = y)
        (fun x : X => istrunc_paths Y (-1) (f x) y)
        (H,
        (fun x x' : X =>
         (fun (Hy : f x = y) (Hy' : f x' = y) =>
          let Hy0 :=
            internal_paths_rew_r
              (fun y0 : Y => f x = y0) Hy Hy' in
          Hf x x' Hy0)
         :
         f x = y -> f x' = y -> x = x')
        :
        atmost1P (fun x : X => f x = y)) in
    (fun (x : X) (_ : f x = y) => x) s.1 s.2) X0.1
     X0.2) == idmap cbn.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
(fun x : {y : Y & Trunc (-1) {x : X & f x = y}} =>
 (f
    (iota (fun x0 : X => f x0 = x.1)
       (fun x0 : X => istrunc_paths Y (-1) (f x0) x.1)
       (x.2,
       fun (x0 x' : X) (Hy : f x0 = x.1)
         (Hy' : f x' = x.1) =>
       Hf x0 x'
         (internal_paths_rew_r (fun y : Y => f x0 = y)
            Hy Hy'))).1;
 tr
   ((iota (fun x0 : X => f x0 = x.1)
       (fun x0 : X => istrunc_paths Y (-1) (f x0) x.1)
       (x.2,
       fun (x0 x' : X) (Hy : f x0 = x.1)
         (Hy' : f x' = x.1) =>
       Hf x0 x'
         (internal_paths_rew_r (fun y : Y => f x0 = y)
            Hy Hy'))).1; 1%path))) == idmap intros [y x].
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
x: Trunc (-1) {x : X & f x = y}
(f
   (iota (fun x : X => f x = y)
      (fun x : X => istrunc_paths Y (-1) (f x) y)
      (x,
      fun (x x' : X) (Hy : f x = y) (Hy' : f x' = y)
      =>
      Hf x x'
        (internal_paths_rew_r (fun y : Y => f x = y)
           Hy Hy'))).1;
tr
  ((iota (fun x : X => f x = y)
      (fun x : X => istrunc_paths Y (-1) (f x) y)
      (x,
      fun (x x' : X) (Hy : f x = y) (Hy' : f x' = y)
      =>
      Hf x x'
        (internal_paths_rew_r (fun y : Y => f x = y)
           Hy Hy'))).1; 1%path)) = (y; x) apply path_sigma_hprop.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
x: Trunc (-1) {x : X & f x = y}
(f
   (iota (fun x : X => f x = y)
      (fun x : X => istrunc_paths Y (-1) (f x) y)
      (x,
      fun (x x' : X) (Hy : f x = y) (Hy' : f x' = y)
      =>
      Hf x x'
        (internal_paths_rew_r (fun y : Y => f x = y)
           Hy Hy'))).1;
tr
  ((iota (fun x : X => f x = y)
      (fun x : X => istrunc_paths Y (-1) (f x) y)
      (x,
      fun (x x' : X) (Hy : f x = y) (Hy' : f x' = y)
      =>
      Hf x x'
        (internal_paths_rew_r (fun y : Y => f x = y)
           Hy Hy'))).1; 1%path)).1 = (y; x).1 cbn.
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
x: Trunc (-1) {x : X & f x = y}
f
  (iota (fun x : X => f x = y)
     (fun x : X => istrunc_paths Y (-1) (f x) y)
     (x,
     fun (x x' : X) (Hy : f x = y) (Hy' : f x' = y) =>
     Hf x x'
       (internal_paths_rew_r (fun y : Y => f x = y) Hy
          Hy'))).1 = y
    destruct iota as [x' Hx].
UA: Univalence
EM: ExcludedMiddle
X: Type
Y: HSet
f: X -> Y
Hf: IsInjective f
y: Y
x: Trunc (-1) {x : X & f x = y}
x': X
Hx: f x' = y
f x' = y exact Hx.
Qed.


(** * Equivalences on infinite sets *)

Lemma path_infinite_unit (X : HSet) :
  infinite X -> Unit + X = X.
UA: Univalence
EM: ExcludedMiddle
X: HSet
infinite X -> Unit + X = X
Proof.
UA: Univalence
EM: ExcludedMiddle
X: HSet
infinite X -> Unit + X = X
  intros [f Hf].
UA: Univalence
EM: ExcludedMiddle
X: HSet
f: nat -> X
Hf: IsInjective f
Unit + X = X rewrite (@path_pred_sum X (ran f)).
UA: Univalence
EM: ExcludedMiddle
X: HSet
f: nat -> X
Hf: IsInjective f
Unit + ({x : X & ran f x} + {x : X & ~ ran f x}) =
{x : X & ran f x} + {x : X & ~ ran f x}
  rewrite (path_ran _ Hf).
UA: Univalence
EM: ExcludedMiddle
X: HSet
f: nat -> X
Hf: IsInjective f
Unit + (nat + {x : X & ~ ran f x}) =
nat + {x : X & ~ ran f x} rewrite path_sum_assoc.
UA: Univalence
EM: ExcludedMiddle
X: HSet
f: nat -> X
Hf: IsInjective f
Unit + nat + {x : X & ~ ran f x} =
nat + {x : X & ~ ran f x}
  rewrite path_unit_nat.
UA: Univalence
EM: ExcludedMiddle
X: HSet
f: nat -> X
Hf: IsInjective f
nat + {x : X & ~ ran f x} = nat + {x : X & ~ ran f x} reflexivity.
Qed.

Fact path_infinite_power (X : HSet) :
  infinite X -> (X -> HProp) + (X -> HProp) = (X -> HProp).
UA: Univalence
EM: ExcludedMiddle
X: HSet
infinite X ->
(X -> HProp) + (X -> HProp) = (X -> HProp)
Proof.
UA: Univalence
EM: ExcludedMiddle
X: HSet
infinite X ->
(X -> HProp) + (X -> HProp) = (X -> HProp)
  intros H.
UA: Univalence
EM: ExcludedMiddle
X: HSet
H: infinite X
(X -> HProp) + (X -> HProp) = (X -> HProp) rewrite path_sum_bool.
UA: Univalence
EM: ExcludedMiddle
X: HSet
H: infinite X
Bool * (X -> HProp) = (X -> HProp) rewrite <- path_bool_subsingleton.
UA: Univalence
EM: ExcludedMiddle
X: HSet
H: infinite X
(Unit -> HProp) * (X -> HProp) = (X -> HProp)
  rewrite path_sum_prod.
UA: Univalence
EM: ExcludedMiddle
X: HSet
H: infinite X
(Unit + X -> HProp) = (X -> HProp) by rewrite path_infinite_unit.
Qed.


(** * Variants of Cantors's theorem *)

(* For the second ingredient, we give a preliminary version (Cantor_path_inject) to see the idea, as well as a stronger refinement (Cantor_injects_injects) which is then a mere reformulation. *)

Context {PR : PropResizing}.

Lemma Cantor X (f : X -> X -> Type) :
  { p | forall x, f x <> p }.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
{p : X -> Type & forall x : X, f x <> p}
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
{p : X -> Type & forall x : X, f x <> p}
  exists (fun x => ~ f x x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
forall x : X, f x <> (fun x0 : X => ~ f x0 x0) intros x H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
Empty
  enough (Hx : f x x <-> ~ f x x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
Hx: f x x <-> ~ f x x
Empty
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
f x x <-> ~ f x x
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
Hx: f x x <-> ~ f x x
Empty apply Hx; apply Hx; intros H'; by apply Hx.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
f x x <-> ~ f x x pattern (f x) at 1.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
(fun T : X -> Type => T x <-> ~ f x x) (f x) rewrite H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> Type
x: X
H: f x = (fun x : X => ~ f x x)
~ f x x <-> ~ f x x reflexivity.
Qed.

Lemma hCantor {X} (f : X -> X -> HProp) :
  { p | forall x, f x <> p }.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
{p : X -> HProp & forall x : X, f x <> p}
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
{p : X -> HProp & forall x : X, f x <> p}
  exists (fun x => Build_HProp (f x x -> Empty)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
forall x : X,
f x <> (fun x0 : X => Build_HProp (f x0 x0 -> Empty)) intros x H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
Empty
  enough (Hx : f x x <-> ~ f x x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
Hx: f x x <-> ~ f x x
Empty
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
f x x <-> ~ f x x
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
Hx: f x x <-> ~ f x x
Empty apply Hx; apply Hx; intros H'; by apply Hx.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
f x x <-> ~ f x x pattern (f x) at 1.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
(fun t : X -> HProp => t x <-> ~ f x x) (f x) rewrite H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
f: X -> X -> HProp
x: X
H: f x = (fun x : X => Build_HProp (f x x -> Empty))
Build_HProp (f x x -> Empty) <-> ~ f x x reflexivity.
Qed.

Definition clean_sum {X Y Z} (f : X -> Y + Z) :
  (forall x y, f x <> inl y) -> forall x, { z | inr z = f x }.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
(forall (x : X) (y : Y), f x <> inl y) ->
forall x : X, {z : Z & inr z = f x}
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
(forall (x : X) (y : Y), f x <> inl y) ->
forall x : X, {z : Z & inr z = f x}
  intros Hf.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
forall x : X, {z : Z & inr z = f x} enough (H : forall x a, a = f x -> {z : Z & inr z = f x}).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
H: forall (x : X) (a : Y + Z),
a = f x -> {z : Z & inr z = f x}
forall x : X, {z : Z & inr z = f x}
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
forall (x : X) (a : Y + Z),
a = f x -> {z : Z & inr z = f x}
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
H: forall (x : X) (a : Y + Z),
a = f x -> {z : Z & inr z = f x}
forall x : X, {z : Z & inr z = f x} intros x.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
H: forall (x : X) (a : Y + Z),
a = f x -> {z : Z & inr z = f x}
x: X
{z : Z & inr z = f x} by apply (H x (f x)).
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
forall (x : X) (a : Y + Z),
a = f x -> {z : Z & inr z = f x} intros x a Hxa.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
Hf: forall (x : X) (y : Y), f x <> inl y
x: X
a: Y + Z
Hxa: a = f x
{z : Z & inr z = f x} specialize (Hf x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
x: X
Hf: forall y : Y, f x <> inl y
a: Y + Z
Hxa: a = f x
{z : Z & inr z = f x} destruct (f x) as [y|z].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
x: X
y: Y
Hf: forall y0 : Y, inl y <> inl y0
a: Y + Z
Hxa: a = inl y
{z : Z & inr z = inl y}
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
x: X
z: Z
Hf: forall y : Y, inr z <> inl y
a: Y + Z
Hxa: a = inr z
{z0 : Z & inr z0 = inr z}
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
x: X
y: Y
Hf: forall y0 : Y, inl y <> inl y0
a: Y + Z
Hxa: a = inl y
{z : Z & inr z = inl y} apply Empty_rect.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
x: X
y: Y
Hf: forall y0 : Y, inl y <> inl y0
a: Y + Z
Hxa: a = inl y
Empty by apply (Hf y).
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y, Z: Type
f: X -> Y + Z
x: X
z: Z
Hf: forall y : Y, inr z <> inl y
a: Y + Z
Hxa: a = inr z
{z0 : Z & inr z0 = inr z} by exists z.
Qed.

Fact Cantor_path_injection {X Y} :
  (X -> HProp) = (X + Y) -> (X + X) = X -> Injection (X -> HProp) Y.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
(X -> HProp) = X + Y ->
X + X = X -> Injection (X -> HProp) Y
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
(X -> HProp) = X + Y ->
X + X = X -> Injection (X -> HProp) Y
  intros H1 H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
Injection (X -> HProp) Y assert (H : X + Y = (X -> HProp) * (X -> HProp)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
X + Y = (X -> HProp) * (X -> HProp)
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
H: X + Y = (X -> HProp) * (X -> HProp)
Injection (X -> HProp) Y
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
X + Y = (X -> HProp) * (X -> HProp) by rewrite <- H1, path_sum_prod, H2. 
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
H: X + Y = (X -> HProp) * (X -> HProp)
Injection (X -> HProp) Y apply equiv_path in H as [f [g Hfg Hgf _]].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
Injection (X -> HProp) Y
    pose (f' x := fst (f (inl x))).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
Injection (X -> HProp) Y destruct (hCantor f') as [p Hp].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
Injection (X -> HProp) Y
    pose (g' q := g (p, q)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
Injection (X -> HProp) Y assert (H' : forall q x, g' q <> inl x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
forall (q : X -> HProp) (x : X), g' q <> inl x
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
Injection (X -> HProp) Y
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
forall (q : X -> HProp) (x : X), g' q <> inl x intros q x H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: g' q = inl x
Empty apply (Hp x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: g' q = inl x
f' x = p unfold f'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: g' q = inl x
fst (f (inl x)) = p rewrite <- H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: g' q = inl x
fst (f (g' q)) = p unfold g'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: g' q = inl x
fst (f (g (p, q))) = p by rewrite Hfg.
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
Injection (X -> HProp) Y exists (fun x => proj1 (clean_sum _ H' x)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
IsInjective
  (fun x : X -> HProp => (clean_sum g' H' x).1) intros q q' H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
q = q' assert (Hqq' : g' q = g' q').
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
g' q = g' q'
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
Hqq': g' q = g' q'
q = q'
      *
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
g' q = g' q' destruct clean_sum as [z <-].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
z: Y
H: (z; 1%path).1 = (clean_sum g' H' q').1
inr z = g' q' destruct clean_sum as [z' <-].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
z, z': Y
H: (z; 1%path).1 = (z'; 1%path).1
inr z = inr z' cbn in H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
z, z': Y
H: z = z'
inr z = inr z' by rewrite H.
      *
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
Hqq': g' q = g' q'
q = q' unfold g' in Hqq'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
Hqq': g (p, q) = g (p, q')
q = q' change (snd (p, q) = snd (p, q')).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
Hqq': g (p, q) = g (p, q')
snd (p, q) = snd (p, q')
        rewrite <- (Hfg (p, q)), <- (Hfg (p, q')).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
H1: (X -> HProp) = X + Y
H2: X + X = X
f: X + Y -> (X -> HProp) * (X -> HProp)
g: (X -> HProp) * (X -> HProp) -> X + Y
Hfg: (fun x : (X -> HProp) * (X -> HProp) => f (g x)) == idmap
Hgf: (fun x : X + Y => g (f x)) == idmap
f':= fun x : X => fst (f (inl x)): X -> X -> HProp
p: X -> HProp
Hp: forall x : X, f' x <> p
g':= fun q : X -> HProp => g (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), g' q <> inl x
q, q': X -> HProp
H: (clean_sum g' H' q).1 = (clean_sum g' H' q').1
Hqq': g (p, q) = g (p, q')
snd (f (g (p, q))) = snd (f (g (p, q'))) by rewrite Hqq'.
Qed.

(* Version just requiring propositional injections *)

Lemma Cantor_rel X (R : X -> (X -> HProp) -> HProp) :
  (forall x p p', R x p -> R x p' -> merely (p = p')) -> { p | forall x, ~ R x p }.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
(forall (x : X) (p p' : X -> HProp),
 R x p -> R x p' -> merely (p = p')) ->
{p : X -> HProp & forall x : X, ~ R x p}
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
(forall (x : X) (p p' : X -> HProp),
 R x p -> R x p' -> merely (p = p')) ->
{p : X -> HProp & forall x : X, ~ R x p}
  intros HR.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
{p : X -> HProp & forall x : X, ~ R x p} pose (pc x := Build_HProp (smalltype (forall p : X -> HProp, R x p -> ~ p x))).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
{p : X -> HProp & forall x : X, ~ R x p}
  exists pc.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
forall x : X, ~ R x pc intros x H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Empty enough (Hpc : pc x <-> ~ pc x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hpc: pc x <-> ~ pc x
Empty
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
pc x <-> ~ pc x 2: split.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hpc: pc x <-> ~ pc x
Empty
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
pc x -> ~ pc x
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
~ pc x -> pc x
  {
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hpc: pc x <-> ~ pc x
Empty apply Hpc; apply Hpc; intros H'; by apply Hpc. }
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
pc x -> ~ pc x
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
~ pc x -> pc x
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
pc x -> ~ pc x intros Hx.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hx: pc x
~ pc x apply equiv_smalltype in Hx.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hx: forall p : X -> HProp, R x p -> ~ p x
~ pc x by apply Hx.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
~ pc x -> pc x intros Hx.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hx: ~ pc x
pc x apply equiv_smalltype.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hx: ~ pc x
forall p : X -> HProp, R x p -> ~ p x intros p Hp.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hx: ~ pc x
p: X -> HProp
Hp: R x p
~ p x
    eapply merely_destruct; try exact (HR _ _ _ Hp H).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X: Type
R: X -> (X -> HProp) -> HProp
HR: forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
pc:= fun x : X =>
Build_HProp
  (smalltype
     (forall p : X -> HProp, R x p -> ~ p x)): X -> HProp
x: X
H: R x pc
Hx: ~ pc x
p: X -> HProp
Hp: R x p
p = pc -> ~ p x by intros ->.
Qed.

Lemma InjectsInto_power_morph X Y :
  InjectsInto X Y -> InjectsInto (X -> HProp) (Y -> HProp).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
InjectsInto X Y ->
InjectsInto (X -> HProp) (Y -> HProp)
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
InjectsInto X Y ->
InjectsInto (X -> HProp) (Y -> HProp)
  intros HF.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
InjectsInto (X -> HProp) (Y -> HProp) eapply merely_destruct; try exact HF.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
Injection X Y -> InjectsInto (X -> HProp) (Y -> HProp) intros [f Hf].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
InjectsInto (X -> HProp) (Y -> HProp)
  apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
Injection (X -> HProp) (Y -> HProp) exists (fun p => fun y => hexists (fun x => p x /\ y = f x)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
IsInjective
  (fun (p : X -> HProp) (y : Y) =>
   hexists (fun x : X => p x * (y = f x)))
  intros p q H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
p = q apply path_forall.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
p == q intros x.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
p x = q x apply equiv_path_iff_hprop.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
p x <-> q x split; intros Hx.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
q x
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
p x
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
q x assert (Hp : (fun y : Y => hexists (fun x : X => p x * (y = f x))) (f x)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
hexists (fun x0 : X => p x0 * (f x = f x0))
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
Hp: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) (f x)
q x {
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
hexists (fun x0 : X => p x0 * (f x = f x0)) apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
{x0 : X & p x0 * (f x = f x0)} exists x.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
p x * (f x = f x) split; trivial. }
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
Hp: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) (f x)
q x
    pattern (f x) in Hp.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
Hp: (fun y : Y =>
 trunctype_type
   ((fun y0 : Y =>
     hexists (fun x : X => p x * (y0 = f x))) y))
  (f x)
q x rewrite H in Hp.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
Hp: hexists (fun x0 : X => q x0 * (f x = f x0))
q x eapply merely_destruct; try exact Hp.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: p x
Hp: hexists (fun x0 : X => q x0 * (f x = f x0))
{x0 : X & q x0 * (f x = f x0)} -> q x by intros [x'[Hq <- % Hf]].
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
p x assert (Hq : (fun y : Y => hexists (fun x : X => q x * (y = f x))) (f x)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
hexists (fun x0 : X => q x0 * (f x = f x0))
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
Hq: (fun y : Y =>
 hexists (fun x : X => q x * (y = f x))) (f x)
p x {
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
hexists (fun x0 : X => q x0 * (f x = f x0)) apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
{x0 : X & q x0 * (f x = f x0)} exists x.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
q x * (f x = f x) split; trivial. }
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
Hq: (fun y : Y =>
 hexists (fun x : X => q x * (y = f x))) (f x)
p x
    pattern (f x) in Hq.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
Hq: (fun y : Y =>
 trunctype_type
   ((fun y0 : Y =>
     hexists (fun x : X => q x * (y0 = f x))) y))
  (f x)
p x rewrite <- H in Hq.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
Hq: hexists (fun x0 : X => p x0 * (f x = f x0))
p x eapply merely_destruct; try exact Hq.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: Type
HF: InjectsInto X Y
f: X -> Y
Hf: IsInjective f
p, q: X -> HProp
H: (fun y : Y =>
 hexists (fun x : X => p x * (y = f x))) =
(fun y : Y =>
 hexists (fun x : X => q x * (y = f x)))
x: X
Hx: q x
Hq: hexists (fun x0 : X => p x0 * (f x = f x0))
{x0 : X & p x0 * (f x = f x0)} -> p x by intros [x'[Hp <- % Hf]].
Qed.

Fact Cantor_injects_injects {X Y : HSet} :
  InjectsInto (X -> HProp) (X + Y) -> InjectsInto (X + X) X -> InjectsInto (X -> HProp) Y.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
InjectsInto (X -> HProp) (X + Y) ->
InjectsInto (X + X) X -> InjectsInto (X -> HProp) Y
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
InjectsInto (X -> HProp) (X + Y) ->
InjectsInto (X + X) X -> InjectsInto (X -> HProp) Y
  intros H1 H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
InjectsInto (X -> HProp) Y assert (HF : InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
InjectsInto (X -> HProp) Y
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y) eapply InjectsInto_trans; try exact H1.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
InjectsInto ((X -> HProp) * (X -> HProp)) (X -> HProp)
    eapply InjectsInto_trans; try apply InjectsInto_power_morph, H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
InjectsInto ((X -> HProp) * (X -> HProp))
  (X + X -> HProp)
    rewrite path_sum_prod.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
InjectsInto (X + X -> HProp) (X + X -> HProp) apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
Injection (X + X -> HProp) (X + X -> HProp) reflexivity.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
InjectsInto (X -> HProp) Y eapply merely_destruct; try exact HF.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
Injection ((X -> HProp) * (X -> HProp)) (X + Y) ->
InjectsInto (X -> HProp) Y intros [f Hf].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
InjectsInto (X -> HProp) Y
    pose (R x p := hexists (fun q => f (p, q) = inl x)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
InjectsInto (X -> HProp) Y destruct (@Cantor_rel _ R) as [p Hp].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p')
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
InjectsInto (X -> HProp) Y
    {
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
forall (x : X) (p p' : X -> HProp),
R x p -> R x p' -> merely (p = p') intros x p p' H3 H4.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
merely (p = p') eapply merely_destruct; try exact H3.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
{q : X -> HProp & f (p, q) = inl x} -> merely (p = p') intros [q Hq].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
q: X -> HProp
Hq: f (p, q) = inl x
merely (p = p')
      eapply merely_destruct; try apply H4.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
q: X -> HProp
Hq: f (p, q) = inl x
{q : X -> HProp & f (p', q) = inl x} ->
merely (p = p') intros [q' Hq'].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
q: X -> HProp
Hq: f (p, q) = inl x
q': X -> HProp
Hq': f (p', q') = inl x
merely (p = p') apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
q: X -> HProp
Hq: f (p, q) = inl x
q': X -> HProp
Hq': f (p', q') = inl x
p = p'
      change p with (fst (p, q)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
q: X -> HProp
Hq: f (p, q) = inl x
q': X -> HProp
Hq': f (p', q') = inl x
fst (p, q) = p' rewrite (Hf (p, q) (p', q')); trivial.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
x: X
p, p': X -> HProp
H3: R x p
H4: R x p'
q: X -> HProp
Hq: f (p, q) = inl x
q': X -> HProp
Hq': f (p', q') = inl x
f (p, q) = f (p', q') by rewrite Hq, Hq'. }
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
InjectsInto (X -> HProp) Y
    pose (f' q := f (p, q)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
InjectsInto (X -> HProp) Y assert (H' : forall q x, f' q <> inl x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
forall (q : X -> HProp) (x : X), f' q <> inl x
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
InjectsInto (X -> HProp) Y
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
forall (q : X -> HProp) (x : X), f' q <> inl x intros q x H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: f' q = inl x
Empty apply (Hp x).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: f' q = inl x
R x p apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: f' q = inl x
{q : X -> HProp & f (p, q) = inl x} exists q.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
q: X -> HProp
x: X
H: f' q = inl x
f (p, q) = inl x exact H.
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
InjectsInto (X -> HProp) Y apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
Injection (X -> HProp) Y exists (fun x => proj1 (clean_sum _ H' x)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
IsInjective
  (fun x : X -> HProp => (clean_sum f' H' x).1) intros q q' H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
q = q' assert (Hqq' : f' q = f' q').
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
f' q = f' q'
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
Hqq': f' q = f' q'
q = q'
      *
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
f' q = f' q' destruct clean_sum as [z <-].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
z: Y
H: (z; 1%path).1 = (clean_sum f' H' q').1
inr z = f' q' destruct clean_sum as [z' <-].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
z, z': Y
H: (z; 1%path).1 = (z'; 1%path).1
inr z = inr z' cbn in H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
z, z': Y
H: z = z'
inr z = inr z' by rewrite H.
      *
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
Hqq': f' q = f' q'
q = q' apply Hf in Hqq'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
Hqq': (p, q) = (p, q')
q = q' change q with (snd (p, q)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
X, Y: HSet
H1: InjectsInto (X -> HProp) (X + Y)
H2: InjectsInto (X + X) X
HF: InjectsInto ((X -> HProp) * (X -> HProp)) (X + Y)
f: (X -> HProp) * (X -> HProp) -> X + Y
Hf: IsInjective f
R:= fun (x : X) (p : X -> HProp) =>
hexists (fun q : X -> HProp => f (p, q) = inl x): X -> (X -> HProp) -> HProp
p: X -> HProp
Hp: forall x : X, ~ R x p
f':= fun q : X -> HProp => f (p, q): (X -> HProp) -> X + Y
H': forall (q : X -> HProp) (x : X), f' q <> inl x
q, q': X -> HProp
H: (clean_sum f' H' q).1 = (clean_sum f' H' q').1
Hqq': (p, q) = (p, q')
snd (p, q) = q' by rewrite Hqq'.
Qed.

End Preparation.


(** * Sierpinski's Theorem *)

Section Sierpinski.

Context {UA : Univalence}.
Context {EM : ExcludedMiddle}.
Context {PR : PropResizing}.

Definition powfix X :=
  forall n, (power_iterated X n + power_iterated X n) = (power_iterated X n).

Variable HN : HSet -> HSet.

Hypothesis HN_ninject : forall X, ~ InjectsInto (HN X) X.

Variable HN_bound : nat.
Hypothesis HN_inject : forall X, InjectsInto (HN X) (power_iterated X HN_bound).

(* This section then concludes the intermediate result that abstractly, any function [HN] behaving like the Hartogs number is tamed in the presence of GCH.  Morally we show that [X <= HN X] for all [X], we just ensure that [X] is large enough by considering P(N + X). *)

Lemma InjectsInto_sum X Y X' Y' :
  InjectsInto X X' -> InjectsInto Y Y' -> InjectsInto (X + Y) (X' + Y').
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
InjectsInto X X' ->
InjectsInto Y Y' -> InjectsInto (X + Y) (X' + Y')
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
InjectsInto X X' ->
InjectsInto Y Y' -> InjectsInto (X + Y) (X' + Y')
  intros H1 H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
InjectsInto (X + Y) (X' + Y')
  eapply merely_destruct; try exact H1.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
Injection X X' -> InjectsInto (X + Y) (X' + Y') intros [f Hf].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
InjectsInto (X + Y) (X' + Y')
  eapply merely_destruct; try exact H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
Injection Y Y' -> InjectsInto (X + Y) (X' + Y') intros [g Hg].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
InjectsInto (X + Y) (X' + Y')
  apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
Injection (X + Y) (X' + Y') exists (fun z => match z with inl x => inl (f x) | inr y => inr (g y) end).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
IsInjective
  (fun z : X + Y =>
   match z with
   | inl x => inl (f x)
   | inr y => inr (g y)
   end)
  intros [x|y] [x'|y'] H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x, x': X
H: inl (f x) = inl (f x')
inl x = inl x'
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x: X
y': Y
H: inl (f x) = inr (g y')
inl x = inr y'
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y: Y
x': X
H: inr (g y) = inl (f x')
inr y = inl x'
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y, y': Y
H: inr (g y) = inr (g y')
inr y = inr y'
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x, x': X
H: inl (f x) = inl (f x')
inl x = inl x' apply ap.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x, x': X
H: inl (f x) = inl (f x')
x = x' apply Hf.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x, x': X
H: inl (f x) = inl (f x')
f x = f x' apply path_sum_inl with Y'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x, x': X
H: inl (f x) = inl (f x')
inl (f x) = inl (f x') exact H.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
x: X
y': Y
H: inl (f x) = inr (g y')
inl x = inr y' by apply inl_ne_inr in H.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y: Y
x': X
H: inr (g y) = inl (f x')
inr y = inl x' by apply inr_ne_inl in H.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y, y': Y
H: inr (g y) = inr (g y')
inr y = inr y' apply ap.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y, y': Y
H: inr (g y) = inr (g y')
y = y' apply Hg.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y, y': Y
H: inr (g y) = inr (g y')
g y = g y' apply path_sum_inr with X'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X, Y, X', Y': Type
H1: InjectsInto X X'
H2: InjectsInto Y Y'
f: X -> X'
Hf: IsInjective f
g: Y -> Y'
Hg: IsInjective g
y, y': Y
H: inr (g y) = inr (g y')
inr (g y) = inr (g y') exact H.
Qed.

(* The main proof is by induction on the cardinality bound for [HN].  As the Hartogs number is bounded by P^3(X), we'd actually just need finitely many instances of GCH. *)

Lemma Sierpinski_step (X : HSet) n :
  GCH -> infinite X -> powfix X -> InjectsInto (HN X) (power_iterated X n) -> InjectsInto X (HN X).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
GCH ->
infinite X ->
powfix X ->
InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
GCH ->
infinite X ->
powfix X ->
InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
  intros gch H1 H2 Hi.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n)
InjectsInto X (HN X) induction n.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X 0)
InjectsInto X (HN X)
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto X (HN X)
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X 0)
InjectsInto X (HN X) by apply HN_ninject in Hi.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto X (HN X) destruct (gch (Build_HSet (power_iterated X n)) (Build_HSet (power_iterated X n + HN X))) as [H|H].
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
infinite (Build_HSet (power_iterated X n))
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (Build_HSet (power_iterated X n))
  (Build_HSet (power_iterated X n + HN X))
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n) -> HProp)
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
InjectsInto X (HN X)
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n) -> HProp)
  (Build_HSet (power_iterated X n + HN X))
InjectsInto X (HN X)
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
infinite (Build_HSet (power_iterated X n)) by apply infinite_power_iterated.
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (Build_HSet (power_iterated X n))
  (Build_HSet (power_iterated X n + HN X)) apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
Injection (Build_HSet (power_iterated X n))
  (Build_HSet (power_iterated X n + HN X)) exists inl.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
IsInjective inl intros x x'.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
x, x': Build_HSet (power_iterated X n)
inl x = inl x' -> x = x' apply path_sum_inl.
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n) -> HProp) eapply InjectsInto_trans.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (Build_HSet (power_iterated X n + HN X))
  ?Y
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto ?Y
  (Build_HSet (power_iterated X n) -> HProp)
      *
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (Build_HSet (power_iterated X n + HN X))
  ?Y apply InjectsInto_sum; try apply Hi.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto (power_iterated X n) ?X' apply tr, Injection_power.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
IsHSet (power_iterated X n) exact _.
      *
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
InjectsInto
  ((power_iterated X n -> HProp) +
   power_iterated X n.+1)
  (Build_HSet (power_iterated X n) -> HProp) cbn.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
Trunc (-1)
  (Injection
     ((power_iterated X n -> HProp) +
      power_type (nat_iter n power_type X))
     (power_iterated X n -> HProp)) specialize (H2 (S n)).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: power_iterated X n.+1 + power_iterated X n.+1 =
power_iterated X n.+1
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
Trunc (-1)
  (Injection
     ((power_iterated X n -> HProp) +
      power_type (nat_iter n power_type X))
     (power_iterated X n -> HProp)) cbn in H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: power_type (nat_iter n power_type X) +
power_type (nat_iter n power_type X) =
power_type (nat_iter n power_type X)
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
Trunc (-1)
  (Injection
     ((power_iterated X n -> HProp) +
      power_type (nat_iter n power_type X))
     (power_iterated X n -> HProp)) rewrite H2.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: power_type (nat_iter n power_type X) +
power_type (nat_iter n power_type X) =
power_type (nat_iter n power_type X)
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
Trunc (-1)
  (Injection (power_type (nat_iter n power_type X))
     (power_iterated X n -> HProp)) apply tr, Injection_refl.
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
InjectsInto X (HN X) apply IHn.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
InjectsInto (HN X) (power_iterated X n) eapply InjectsInto_trans; try apply H.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
InjectsInto (HN X)
  (Build_HSet (power_iterated X n + HN X)) apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
Injection (HN X)
  (Build_HSet (power_iterated X n + HN X)) exists inr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
IsInjective inr intros x y.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n + HN X))
  (Build_HSet (power_iterated X n))
x, y: HN X
inr x = inr y -> x = y apply path_sum_inr.
    +
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n) -> HProp)
  (Build_HSet (power_iterated X n + HN X))
InjectsInto X (HN X) apply InjectsInto_trans with (power_iterated X (S n)); try apply tr, Injection_power_iterated.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n) -> HProp)
  (Build_HSet (power_iterated X n + HN X))
InjectsInto (power_iterated X n.+1) (HN X)
      cbn.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n) -> HProp)
  (Build_HSet (power_iterated X n + HN X))
Trunc (-1)
  (Injection (power_type (nat_iter n power_type X))
     (HN X)) apply (Cantor_injects_injects H).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n) -> HProp)
  (Build_HSet (power_iterated X n + HN X))
InjectsInto
  (Build_HSet (power_iterated X n) +
   Build_HSet (power_iterated X n))
  (Build_HSet (power_iterated X n)) rewrite (H2 n).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
n: nat
gch: GCH
H1: infinite X
H2: powfix X
Hi: InjectsInto (HN X) (power_iterated X n.+1)
IHn: InjectsInto (HN X) (power_iterated X n) ->
InjectsInto X (HN X)
H: InjectsInto
  (Build_HSet (power_iterated X n) -> HProp)
  (Build_HSet (power_iterated X n + HN X))
InjectsInto (power_iterated X n)
  (Build_HSet (power_iterated X n)) apply tr, Injection_refl.
Qed.

Theorem GCH_injects' (X : HSet) :
  GCH -> infinite X -> InjectsInto X (HN (Build_HSet (X -> HProp))).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
GCH ->
infinite X ->
InjectsInto X (HN (Build_HSet (X -> HProp)))
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
GCH ->
infinite X ->
InjectsInto X (HN (Build_HSet (X -> HProp)))
  intros gch HX.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
InjectsInto X (HN (Build_HSet (X -> HProp))) eapply InjectsInto_trans; try apply tr, Injection_power; try apply X.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
InjectsInto (X -> HProp)
  (HN (Build_HSet (X -> HProp)))
  apply (@Sierpinski_step (Build_HSet (X -> HProp)) HN_bound gch).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
infinite (Build_HSet (X -> HProp))
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
powfix (Build_HSet (X -> HProp))
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
InjectsInto (HN (Build_HSet (X -> HProp)))
  (power_iterated (Build_HSet (X -> HProp)) HN_bound)
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
infinite (Build_HSet (X -> HProp)) apply infinite_inject with X; trivial.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
Injection X (Build_HSet (X -> HProp)) apply Injection_power.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
IsHSet X apply X.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
powfix (Build_HSet (X -> HProp)) intros n.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
n: nat
power_iterated (Build_HSet (X -> HProp)) n +
power_iterated (Build_HSet (X -> HProp)) n =
power_iterated (Build_HSet (X -> HProp)) n cbn.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
n: nat
power_iterated (X -> HProp) n +
power_iterated (X -> HProp) n =
power_iterated (X -> HProp) n rewrite !power_iterated_shift.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
n: nat
(power_iterated X n -> HProp) +
(power_iterated X n -> HProp) =
(power_iterated X n -> HProp) eapply path_infinite_power.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
n: nat
infinite
  (default_TruncType 0 (power_iterated X n)
     (hset_power_iterated X n)) cbn.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
n: nat
infinite (power_iterated X n) by apply infinite_power_iterated.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
HX: infinite X
InjectsInto (HN (Build_HSet (X -> HProp)))
  (power_iterated (Build_HSet (X -> HProp)) HN_bound) apply HN_inject.
Qed.

Theorem GCH_injects (X : HSet) :
  GCH -> InjectsInto X (HN (Build_HSet (Build_HSet (nat + X) -> HProp))).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
GCH ->
InjectsInto X
  (HN (Build_HSet (Build_HSet (nat + X) -> HProp)))
Proof.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
GCH ->
InjectsInto X
  (HN (Build_HSet (Build_HSet (nat + X) -> HProp)))
  intros gch.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
InjectsInto X
  (HN (Build_HSet (Build_HSet (nat + X) -> HProp))) eapply InjectsInto_trans with (nat + X).
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
InjectsInto X (nat + X)
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
InjectsInto (nat + X)
  (HN (Build_HSet (Build_HSet (nat + X) -> HProp)))
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
InjectsInto X (nat + X) apply tr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
Injection X (nat + X) exists inr.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
IsInjective inr intros x y.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
x, y: X
inr x = inr y -> x = y apply path_sum_inr.
  -
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
InjectsInto (nat + X)
  (HN (Build_HSet (Build_HSet (nat + X) -> HProp))) apply GCH_injects'; trivial.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
infinite (Build_HSet (nat + X)) exists inl.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
IsInjective inl intros x y.
UA: Univalence
EM: ExcludedMiddle
PR: PropResizing
HN: HSet -> HSet
HN_ninject: forall X : HSet, ~ InjectsInto (HN X) X
HN_bound: nat
HN_inject: forall X : HSet,
InjectsInto (HN X)
  (power_iterated X HN_bound)
X: HSet
gch: GCH
x, y: nat
inl x = inl y -> x = y apply path_sum_inl.
Qed.

End Sierpinski.

(* Main result: GCH implies AC *)

Theorem GCH_AC {UA : Univalence} {PR : PropResizing} {LEM : ExcludedMiddle} :
  GCH -> Choice_type.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
GCH -> Choice_type
Proof.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
GCH -> Choice_type
  intros gch.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
Choice_type
  apply WO_AC.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
forall X : HSet,
hexists (fun A : Ordinal => InjectsInto X A) intros X.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
hexists (fun A : Ordinal => InjectsInto X A) apply tr.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
{A : Ordinal & InjectsInto X A} exists (hartogs_number (Build_HSet (Build_HSet (nat + X) -> HProp))).
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
InjectsInto X
  (hartogs_number
     (Build_HSet (Build_HSet (nat + X) -> HProp)))
  unshelve eapply (@GCH_injects UA LEM PR hartogs_number _ 3 _ X gch).
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
forall X : HSet,
~
InjectsInto
  ((fun A : HSet => ordinal_as_hset (hartogs_number A))
     X) X
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
forall X : HSet,
InjectsInto
  ((fun A : HSet => ordinal_as_hset (hartogs_number A))
     X) (power_iterated X 3)
  -
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
forall X : HSet,
~
InjectsInto
  ((fun A : HSet => ordinal_as_hset (hartogs_number A))
     X) X intros Y.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X, Y: HSet
~
InjectsInto
  ((fun A : HSet => ordinal_as_hset (hartogs_number A))
     Y) Y intros H.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X, Y: HSet
H: InjectsInto (hartogs_number Y) Y
Empty eapply merely_destruct; try apply H.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X, Y: HSet
H: InjectsInto (hartogs_number Y) Y
Injection (hartogs_number Y) Y -> Empty apply hartogs_number_no_injection.
  -
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X: HSet
forall X : HSet,
InjectsInto
  ((fun A : HSet => ordinal_as_hset (hartogs_number A))
     X) (power_iterated X 3) intros Y.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X, Y: HSet
InjectsInto
  ((fun A : HSet => ordinal_as_hset (hartogs_number A))
     Y) (power_iterated Y 3) apply tr.
UA: Univalence
PR: PropResizing
LEM: ExcludedMiddle
gch: GCH
X, Y: HSet
Injection (hartogs_number Y) (power_iterated Y 3) apply hartogs_number_injection.
Qed.

(* Note that the assumption of LEM is actually not necessary due to GCH_LEM. *)