From HoTT Require Import TruncType abstract_algebra.From HoTT Require Import TruncType abstract_algebra.
From HoTT Require Import Universes.Smallness.
From HoTT Require Import Spaces.Nat.Core Spaces.Card.

Local Open Scope type.
Local Open Scope hprop_scope.


(** * Formulation of GCH *)

(* GCH states that for any infinite set X with Y between X and P(X) either Y embeds into X or P(X) embeds into Y. *)

Definition GCH :=
  forall X Y : HSet, infinite X -> InjectsInto X Y -> InjectsInto Y (X -> HProp) -> InjectsInto Y X + InjectsInto (X -> HProp) Y.



(** * GCH is a proposition *)

Lemma Cantor_inj {PR : PropResizing} {FE : Funext} X :
  ~ Injection (X -> HProp) X.
PR: PropResizing
FE: Funext
X: Type
~ Injection (X -> HProp) X
Proof.
PR: PropResizing
FE: Funext
X: Type
~ Injection (X -> HProp) X
  intros [i HI].
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
Empty pose (p n := Build_HProp (smalltype (forall q, i q = n -> ~ q n))).
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
Empty
  enough (Hp : p (i p) <-> ~ p (i p)).
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
Hp: p (i p) <-> ~ p (i p)
Empty
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
p (i p) <-> ~ p (i p)
  {
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
Hp: p (i p) <-> ~ p (i p)
Empty apply Hp; apply Hp; intros H; by apply Hp. }
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
p (i p) <-> ~ p (i p)
  unfold p at 1.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p))) <->
~ p (i p) split.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p))) ->
~ p (i p)
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
~ p (i p) ->
Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p)))
  -
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p))) ->
~ p (i p) intros H.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
H: Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p)))
~ p (i p) apply equiv_smalltype in H.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
H: forall q : X -> HProp, i q = i p -> ~ q (i p)
~ p (i p) apply H.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
H: forall q : X -> HProp, i q = i p -> ~ q (i p)
i p = i p reflexivity.
  -
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
~ p (i p) ->
Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p))) intros H.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
H: ~ p (i p)
Build_HProp (smalltype (forall q : X -> HProp, i q = i p -> ~ q (i p))) apply equiv_smalltype.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
H: ~ p (i p)
forall q : X -> HProp, i q = i p -> ~ q (i p) intros q -> % HI.
PR: PropResizing
FE: Funext
X: Type
i: (X -> HProp) -> X
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = n -> ~ q n)): X -> HProp
H: ~ p (i p)
~ p (i p) exact H.
Qed.

(* The concluding disjunction of GCH is exclusive since otherwise we'd obtain an injection of P(X) into X. *)

Lemma hprop_GCH {PR : PropResizing} {FE : Funext} :
  IsHProp GCH.
PR: PropResizing
FE: Funext
IsHProp GCH
Proof.
PR: PropResizing
FE: Funext
IsHProp GCH
  repeat (napply istrunc_forall; intros).
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
IsHProp (InjectsInto a0 a + InjectsInto (a -> HProp) a0)
  apply hprop_allpath.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
forall x y : InjectsInto a0 a + InjectsInto (a -> HProp) a0, x = y intros [H|H] [H'|H'].
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H, H': InjectsInto a0 a
inl H = inl H'
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto a0 a
H': InjectsInto (a -> HProp) a0
inl H = inr H'
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto (a -> HProp) a0
H': InjectsInto a0 a
inr H = inl H'
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H, H': InjectsInto (a -> HProp) a0
inr H = inr H'
  -
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H, H': InjectsInto a0 a
inl H = inl H' enough (H = H') as ->; trivial.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H, H': InjectsInto a0 a
H = H' apply path_ishprop.
  -
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto a0 a
H': InjectsInto (a -> HProp) a0
inl H = inr H' apply Empty_rec.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto a0 a
H': InjectsInto (a -> HProp) a0
Empty eapply merely_destruct; try eapply (Cantor_inj a); trivial.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto a0 a
H': InjectsInto (a -> HProp) a0
merely (Injection (a -> HProp) a) by apply InjectsInto_trans with a0.
  -
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto (a -> HProp) a0
H': InjectsInto a0 a
inr H = inl H' apply Empty_rec.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto (a -> HProp) a0
H': InjectsInto a0 a
Empty eapply merely_destruct; try eapply (Cantor_inj a); trivial.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H: InjectsInto (a -> HProp) a0
H': InjectsInto a0 a
merely (Injection (a -> HProp) a) by apply InjectsInto_trans with a0.
  -
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H, H': InjectsInto (a -> HProp) a0
inr H = inr H' enough (H = H') as ->; trivial.
PR: PropResizing
FE: Funext
a, a0: HSet
a1: infinite a
a2: InjectsInto a a0
a3: InjectsInto a0 (a -> HProp)
H, H': InjectsInto (a -> HProp) a0
H = H' apply path_ishprop.
Qed.



(** * GCH implies LEM *)

Section LEM.

  Variable X : HSet.
  Variable P : HProp.

  Context {PR : PropResizing}.
  Context {FE : Funext}.

  Definition hpaths (x y : X) :=
    Build_HProp (paths x y).

  Definition sing (p : X -> HProp) :=
    exists x, p = hpaths x.

  Let sings :=
    { p : X -> HProp | sing p \/ (P + ~ P) }.

  (* The main idea is that for a given set X and proposition P, the set sings fits between X and P(X).
     Then CH for X implies that either sings embeds into X (which can be refuted constructively),
     or that P(X) embeds into sings, from which we can extract a proof of P + ~P. *)  

  Lemma Cantor_sing (i : (X -> HProp) -> (X -> HProp)) :
    IsInjective i -> exists p, ~ sing (i p).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
IsInjective i -> {p : X -> HProp & ~ sing (i p)}
  Proof.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
IsInjective i -> {p : X -> HProp & ~ sing (i p)}
    intros HI.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
{p : X -> HProp & ~ sing (i p)} pose (p n := Build_HProp (smalltype (forall q, i q = hpaths n -> ~ q n))).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)): X -> HProp
{p0 : X -> HProp & ~ sing (i p0)}
    exists p.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)): X -> HProp
~ sing (i p) intros [n HN].
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
Empty enough (Hp : p n <-> ~ p n).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
Hp: p n <-> ~ p n
Empty
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
p n <-> ~ p n
    {
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
Hp: p n <-> ~ p n
Empty apply Hp; apply Hp; intros H; by apply Hp. }
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
p n <-> ~ p n
    unfold p at 1.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)) <->
~ p n split.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)) ->
~ p n
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
~ p n ->
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n))
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)) ->
~ p n intros H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
H: Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n))
~ p n apply equiv_smalltype in H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
H: forall q : X -> HProp, i q = hpaths n -> ~ q n
~ p n apply H, HN.
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
~ p n ->
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)) intros H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
H: ~ p n
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n -> ~ q n)) apply equiv_smalltype.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q : X -> HProp, i q = hpaths n0 -> ~ q n0)): X -> HProp
n: X
HN: i p = hpaths n
H: ~ p n
forall q : X -> HProp, i q = hpaths n -> ~ q n intros q HQ.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q0 : X -> HProp, i q0 = hpaths n0 -> ~ q0 n0)): X -> HProp
n: X
HN: i p = hpaths n
H: ~ p n
q: X -> HProp
HQ: i q = hpaths n
~ q n rewrite <- HN in HQ.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
i: (X -> HProp) -> X -> HProp
HI: IsInjective i
p:= fun n0 : X =>
Build_HProp (smalltype (forall q0 : X -> HProp, i q0 = hpaths n0 -> ~ q0 n0)): X -> HProp
n: X
HN: i p = hpaths n
H: ~ p n
q: X -> HProp
HQ: i q = i p
~ q n by apply HI in HQ as ->.
  Qed.

  Lemma injective_proj1 {Z} (r : Z -> HProp) :
    IsInjective (@proj1 Z r).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
IsInjective pr1
  Proof.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
IsInjective pr1
    intros [p Hp] [q Hq]; cbn.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
p: Z
Hp: r p
q: Z
Hq: r q
p = q -> (p; Hp) = (q; Hq)
    intros ->.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
q: Z
Hp, Hq: r q
(q; Hp) = (q; Hq) unshelve eapply path_sigma; cbn.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
q: Z
Hp, Hq: r q
q = q
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
q: Z
Hp, Hq: r q
transport (fun x : Z => r x) ?Goal Hp = Hq
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
q: Z
Hp, Hq: r q
q = q reflexivity.
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
q: Z
Hp, Hq: r q
transport (fun x : Z => r x) 1 Hp = Hq cbn.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
Z: Type
r: Z -> HProp
q: Z
Hp, Hq: r q
Hp = Hq apply path_ishprop.
  Qed.

  Lemma inject_sings :
    (P + ~ P) -> Injection (X -> HProp) sings.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
P + ~ P -> Injection (X -> HProp) sings
  Proof.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
P + ~ P -> Injection (X -> HProp) sings
    intros HP.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
HP: P + ~ P
Injection (X -> HProp) sings unshelve eexists.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
HP: P + ~ P
(X -> HProp) -> sings
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
HP: P + ~ P
IsInjective ?f
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
HP: P + ~ P
(X -> HProp) -> sings intros p.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p: X -> HProp
sings exists p.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p: X -> HProp
sing p \/ P + ~ P apply tr.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p: X -> HProp
sing p + (P + ~ P) by right.
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
HP: P + ~ P
IsInjective (fun p : X -> HProp => (p; tr (inr HP))) intros p q.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p, q: X -> HProp
(p; tr (inr HP)) = (q; tr (inr HP)) -> p = q intros H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p, q: X -> HProp
H: (p; tr (inr HP)) = (q; tr (inr HP))
p = q change p with ((exist (fun r => sing r \/ (P + ~ P)) p (tr (inr HP))).1).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p, q: X -> HProp
H: (p; tr (inr HP)) = (q; tr (inr HP))
(p; tr (inr HP)).1 = q
      rewrite H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p, q: X -> HProp
H: (p; tr (inr HP)) = (q; tr (inr HP))
(q; tr (inr HP)).1 = q cbn.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
HP: P + ~ P
p, q: X -> HProp
H: (p; tr (inr HP)) = (q; tr (inr HP))
q = q reflexivity.
  Qed.

  Theorem CH_LEM :
    (Injection X sings -> Injection sings (X -> HProp) -> ~ (Injection sings X) -> InjectsInto (X -> HProp) sings)
    -> P \/ ~ P.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
(Injection X sings ->
 Injection sings (X -> HProp) ->
 ~ Injection sings X -> InjectsInto (X -> HProp) sings) ->
P \/ ~ P
  Proof.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
(Injection X sings ->
 Injection sings (X -> HProp) ->
 ~ Injection sings X -> InjectsInto (X -> HProp) sings) ->
P \/ ~ P
    intros ch.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
P \/ ~ P eapply merely_destruct; try apply ch.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
Injection X sings
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
Injection sings (X -> HProp)
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
~ Injection sings X
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
Injection (X -> HProp) sings -> P \/ ~ P
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
Injection X sings unshelve eexists.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
X -> sings
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
IsInjective ?f
      +
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
X -> sings intros x.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x: X
sings exists (hpaths x).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x: X
sing (hpaths x) \/ P + ~ P apply tr.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x: X
sing (hpaths x) + (P + ~ P) left.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x: X
sing (hpaths x) exists x.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x: X
hpaths x = hpaths x reflexivity.
      +
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
IsInjective (fun x : X => (hpaths x; tr (inl (x; 1%path)))) intros x y.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x, y: X
(hpaths x; tr (inl (x; 1%path))) = (hpaths y; tr (inl (y; 1%path))) -> x = y intros H % pr1_path.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x, y: X
H: (hpaths x; tr (inl (x; 1%path))).1 = (hpaths y; tr (inl (y; 1%path))).1
x = y cbn in H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x, y: X
H: hpaths x = hpaths y
x = y change (hpaths x y).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
x, y: X
H: hpaths x = hpaths y
hpaths x y by rewrite H.
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
Injection sings (X -> HProp) exists (@proj1 _ _).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
IsInjective pr1 by apply injective_proj1.
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
~ Injection sings X intros H.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
Empty assert (HP' : ~ ~ (P + ~ P)).
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
~~ (P + ~ P)
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP': ~~ (P + ~ P)
Empty
      {
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
~~ (P + ~ P) intros HP.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: ~ (P + ~ P)
Empty apply HP.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: ~ (P + ~ P)
P + ~ P right.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: ~ (P + ~ P)
~ P intros p.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: ~ (P + ~ P)
p: P
Empty apply HP.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: ~ (P + ~ P)
p: P
P + ~ P by left. }
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP': ~~ (P + ~ P)
Empty
      apply HP'.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP': ~~ (P + ~ P)
~ (P + ~ P) intros HP % inject_sings.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP': ~~ (P + ~ P)
HP: Injection (X -> HProp) sings
Empty clear HP'.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: Injection (X -> HProp) sings
Empty
      apply Cantor_inj with X.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
H: Injection sings X
HP: Injection (X -> HProp) sings
Injection (X -> HProp) X by eapply (Injection_trans _ _ _ HP).
    -
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
Injection (X -> HProp) sings -> P \/ ~ P intros [i Hi].
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
i: (X -> HProp) -> sings
Hi: IsInjective i
P \/ ~ P destruct (Cantor_sing (fun p => @proj1 _ _ (i p))) as [p HP].
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
i: (X -> HProp) -> sings
Hi: IsInjective i
IsInjective (fun p : X -> HProp => (i p).1)
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
i: (X -> HProp) -> sings
Hi: IsInjective i
p: X -> HProp
HP: ~ sing (i p).1
P \/ ~ P
      +
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
i: (X -> HProp) -> sings
Hi: IsInjective i
IsInjective (fun p : X -> HProp => (i p).1) intros x y H % injective_proj1.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p : X -> HProp & sing p \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
i: (X -> HProp) -> sings
Hi: IsInjective i
x, y: X -> HProp
H: i x = i y
x = y by apply Hi.
      +
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & sing p0 \/ P + ~ P}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> InjectsInto (X -> HProp) sings
i: (X -> HProp) -> sings
Hi: IsInjective i
p: X -> HProp
HP: ~ sing (i p).1
P \/ ~ P destruct (i p) as [q Hq]; cbn in *.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & Trunc (-1) (sing p0 + (P + ~ P))}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> Trunc (-1) (Injection (X -> HProp) sings)
i: (X -> HProp) -> sings
Hi: IsInjective i
p, q: X -> HProp
Hq: Trunc (-1) (sing q + (P + ~ P))
HP: ~ sing q
Trunc (-1) (P + ~ P)
        eapply merely_destruct; try exact Hq.
X: HSet
P: HProp
PR: PropResizing
FE: Funext
sings:= {p0 : X -> HProp & Trunc (-1) (sing p0 + (P + ~ P))}: Type
ch: Injection X sings ->
Injection sings (X -> HProp) ->
~ Injection sings X -> Trunc (-1) (Injection (X -> HProp) sings)
i: (X -> HProp) -> sings
Hi: IsInjective i
p, q: X -> HProp
Hq: Trunc (-1) (sing q + (P + ~ P))
HP: ~ sing q
sing q + (P + ~ P) -> Trunc (-1) (P + ~ P)
        intros [H|H]; [destruct (HP H)|by apply tr].
  Qed.

End LEM.

(* We can instantiate the previous lemma with nat to obtain GCH -> LEM. *)

Theorem GCH_LEM {PR : PropResizing} {UA : Univalence} :
  GCH -> (forall P : HProp, P \/ ~ P).
PR: PropResizing
UA: Univalence
GCH -> forall P : HProp, P \/ ~ P
Proof.
PR: PropResizing
UA: Univalence
GCH -> forall P : HProp, P \/ ~ P
  intros gch P.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
P \/ ~ P eapply (CH_LEM (Build_HSet nat)); try exact _.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P} ->
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp) ->
~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat) ->
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P} intros H1 H2 H3.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  pose (sings := { p : nat -> HProp | sing (Build_HSet nat) p \/ (P + ~ P) }).
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  destruct (gch (Build_HSet nat) (Build_HSet sings)) as [H|H].
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
infinite (Build_HSet nat)
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
InjectsInto (Build_HSet nat) (Build_HSet sings)
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
InjectsInto (Build_HSet sings) (Build_HSet nat -> HProp)
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
H: InjectsInto (Build_HSet sings) (Build_HSet nat)
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
H: InjectsInto (Build_HSet nat -> HProp) (Build_HSet sings)
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  -
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
infinite (Build_HSet nat) cbn.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
infinite nat exists idmap.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
IsInjective idmap apply isinj_idmap.
  -
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
InjectsInto (Build_HSet nat) (Build_HSet sings) apply tr.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
Injection (Build_HSet nat) (Build_HSet sings) exact H1.
  -
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
InjectsInto (Build_HSet sings) (Build_HSet nat -> HProp) apply tr.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
Injection (Build_HSet sings) (Build_HSet nat -> HProp) exact H2.
  -
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
H: InjectsInto (Build_HSet sings) (Build_HSet nat)
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P} apply Empty_rec.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
H: InjectsInto (Build_HSet sings) (Build_HSet nat)
Empty eapply merely_destruct; try exact H.
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
H: InjectsInto (Build_HSet sings) (Build_HSet nat)
Injection (Build_HSet sings) (Build_HSet nat) -> Empty exact H3.
  -
PR: PropResizing
UA: Univalence
gch: GCH
P: HProp
H1: Injection (Build_HSet nat)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
H2: Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat -> HProp)
H3: ~
Injection {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}
  (Build_HSet nat)
sings:= {p : nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P}: Type
H: InjectsInto (Build_HSet nat -> HProp) (Build_HSet sings)
InjectsInto (Build_HSet nat -> HProp)
  {p : Build_HSet nat -> HProp & sing (Build_HSet nat) p \/ P + ~ P} exact H.
Qed.