From HoTT Require Import Basics Types TruncType.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
From HoTT Require Import Universes.Smallness.
From HoTT Require Import Spaces.Card Spaces.Nat.Core.

(** * Definition of Power types *)

(* The definition is only used in Hartogs.v to allow defining a coercion, and one place below.  Everywhere else we prefer to write out the definition for clarity. *)

Definition power_type (A : Type) : Type
  := A -> HProp.

(** * Iterated powers *)

Lemma Injection_power {PR : PropResizing} X
  : IsHSet X -> Injection X (X -> HProp).
PR: PropResizing
X: Type
IsHSet X -> Injection X (X -> HProp)
Proof.
PR: PropResizing
X: Type
IsHSet X -> Injection X (X -> HProp)
  intros HX.
PR: PropResizing
X: Type
HX: IsHSet X
Injection X (X -> HProp)
  set (f (x : X) := fun y => Build_HProp (smalltype (x = y))).
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
Injection X (X -> HProp)
  exists f.
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
IsInjective f intros x x' H.
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
x, x': X
H: f x = f x'
x = x'
  eapply equiv_smalltype.
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
x, x': X
H: f x = f x'
smalltype (x = x') change (f x x').
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
x, x': X
H: f x = f x'
f x x'
  rewrite H.
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
x, x': X
H: f x = f x'
f x' x' cbn.
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
x, x': X
H: f x = f x'
smalltype (x' = x') apply equiv_smalltype.
PR: PropResizing
X: Type
HX: IsHSet X
f:= fun x y : X => Build_HProp (smalltype (x = y)): X -> X -> HProp
x, x': X
H: f x = f x'
x' = x' reflexivity.
Qed.

Definition power_iterated X n := nat_iter n power_type X.

Definition power_iterated_shift X n
  : power_iterated (X -> HProp) n = (power_iterated X n -> HProp)
  := (nat_iter_succ_r _ _ _)^.

Instance hset_power {UA : Univalence} (X : HSet)
  : IsHSet (X -> HProp).
UA: Univalence
X: HSet
IsHSet (X -> HProp)
Proof.
UA: Univalence
X: HSet
IsHSet (X -> HProp)
  apply istrunc_S.
UA: Univalence
X: HSet
is_mere_relation (X -> HProp) paths
  intros p q.
UA: Univalence
X: HSet
p, q: X -> HProp
IsHProp (p = q) apply hprop_allpath.
UA: Univalence
X: HSet
p, q: X -> HProp
forall x y : p = q, x = y intros H H'.
UA: Univalence
X: HSet
p, q: X -> HProp
H, H': p = q
H = H'
  destruct (equiv_path_arrow p q) as [f [g Hfg Hgf _]].
UA: Univalence
X: HSet
p, q: X -> HProp
H, H': p = q
f: p == q -> p = q
g: p = q -> p == q
Hfg: (fun x : p = q => f (g x)) == idmap
Hgf: (fun x : p == q => g (f x)) == idmap
H = H'
  rewrite <- (Hfg H), <- (Hfg H').
UA: Univalence
X: HSet
p, q: X -> HProp
H, H': p = q
f: p == q -> p = q
g: p = q -> p == q
Hfg: (fun x : p = q => f (g x)) == idmap
Hgf: (fun x : p == q => g (f x)) == idmap
f (g H) = f (g H') apply ap.
UA: Univalence
X: HSet
p, q: X -> HProp
H, H': p = q
f: p == q -> p = q
g: p = q -> p == q
Hfg: (fun x : p = q => f (g x)) == idmap
Hgf: (fun x : p == q => g (f x)) == idmap
g H = g H' apply path_forall.
UA: Univalence
X: HSet
p, q: X -> HProp
H, H': p = q
f: p == q -> p = q
g: p = q -> p == q
Hfg: (fun x : p = q => f (g x)) == idmap
Hgf: (fun x : p == q => g (f x)) == idmap
g H == g H'
  intros x.
UA: Univalence
X: HSet
p, q: X -> HProp
H, H': p = q
f: p == q -> p = q
g: p = q -> p == q
Hfg: (fun x : p = q => f (g x)) == idmap
Hgf: (fun x : p == q => g (f x)) == idmap
x: X
g H x = g H' x apply path_ishprop.
Qed.

Instance hset_power_iterated {UA : Univalence} (X : HSet) n
  : IsHSet (power_iterated X n).
UA: Univalence
X: HSet
n: nat
IsHSet (power_iterated X n)
Proof.
UA: Univalence
X: HSet
n: nat
IsHSet (power_iterated X n)
  napply (nat_iter_invariant n power_type (fun A => IsHSet A)).
UA: Univalence
X: HSet
n: nat
forall x : Type, IsHSet x -> IsHSet (power_type x)
UA: Univalence
X: HSet
n: nat
IsHSet X
  -
UA: Univalence
X: HSet
n: nat
forall x : Type, IsHSet x -> IsHSet (power_type x) intros Y HS.
UA: Univalence
X: HSet
n: nat
Y: Type
HS: IsHSet Y
IsHSet (power_type Y) rapply hset_power.
  -
UA: Univalence
X: HSet
n: nat
IsHSet X exact _.
Defined.

Lemma Injection_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n
  : Injection X (power_iterated X n).
UA: Univalence
PR: PropResizing
X: HSet
n: nat
Injection X (power_iterated X n)
Proof.
UA: Univalence
PR: PropResizing
X: HSet
n: nat
Injection X (power_iterated X n)
  induction n as [|n IHn].
UA: Univalence
PR: PropResizing
X: HSet
Injection X (power_iterated X 0)
UA: Univalence
PR: PropResizing
X: HSet
n: nat
IHn: Injection X (power_iterated X n)
Injection X (power_iterated X n.+1)
  -
UA: Univalence
PR: PropResizing
X: HSet
Injection X (power_iterated X 0) reflexivity.
  -
UA: Univalence
PR: PropResizing
X: HSet
n: nat
IHn: Injection X (power_iterated X n)
Injection X (power_iterated X n.+1) eapply Injection_trans; try exact IHn.
UA: Univalence
PR: PropResizing
X: HSet
n: nat
IHn: Injection X (power_iterated X n)
Injection (power_iterated X n) (power_iterated X n.+1)
    apply Injection_power.
UA: Univalence
PR: PropResizing
X: HSet
n: nat
IHn: Injection X (power_iterated X n)
IsHSet (power_iterated X n) exact _.
Qed.

Lemma infinite_inject X Y
  : infinite X -> Injection X Y -> infinite Y.
X, Y: Type
infinite X -> Injection X Y -> infinite Y
Proof.
X, Y: Type
infinite X -> Injection X Y -> infinite Y
  apply Injection_trans.
Qed.

Lemma infinite_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n
  : infinite X -> infinite (power_iterated X n).
UA: Univalence
PR: PropResizing
X: HSet
n: nat
infinite X -> infinite (power_iterated X n)
Proof.
UA: Univalence
PR: PropResizing
X: HSet
n: nat
infinite X -> infinite (power_iterated X n)
  intros H.
UA: Univalence
PR: PropResizing
X: HSet
n: nat
H: infinite X
infinite (power_iterated X n) eapply infinite_inject; try apply H.
UA: Univalence
PR: PropResizing
X: HSet
n: nat
H: infinite X
Injection X (power_iterated X n) apply Injection_power_iterated.
Qed.