Require Import HoTT.Basics HoTT.Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Definition atmost1 X:=(forall x1 x2:X, (x1 = x2)).
Definition atmost1P {X} (P:X->Type):=
    (forall x1 x2:X, P x1 -> P x2 -> (x1 = x2)).
Definition hunique {X} (P:X->Type):=(hexists P) * (atmost1P P).

Lemma atmost {X} {P : X -> Type}:
  (forall x, IsHProp (P x)) -> (atmost1P P) -> atmost1 (sig  P).
X: Type
P: X -> Type
(forall x : X, IsHProp (P x)) ->
atmost1P P -> atmost1 {x : _ & P x}
intros H H0 [x p] [y q].
X: Type
P: X -> Type
H: forall x : X, IsHProp (P x)
H0: atmost1P P
x: X
p: P x
y: X
q: P y
(x; p) = (y; q)
specialize (H0 x y p q).
X: Type
P: X -> Type
H: forall x : X, IsHProp (P x)
x, y: X
H0: x = y
p: P x
q: P y
(x; p) = (y; q)
induction H0.
X: Type
P: X -> Type
H: forall x : X, IsHProp (P x)
x: X
p, q: P x
(x; p) = (x; q)
assert (H0: (p =q)) by apply path_ishprop.
X: Type
P: X -> Type
H: forall x : X, IsHProp (P x)
x: X
p, q: P x
H0: p = q
(x; p) = (x; q)
by induction H0.
Qed.

Lemma iota {X} (P:X-> Type):
  (forall x, IsHProp (P x)) -> (hunique P) -> sig P.
X: Type
P: X -> Type
(forall x : X, IsHProp (P x)) ->
hunique P -> {x : _ & P x}
Proof.
X: Type
P: X -> Type
(forall x : X, IsHProp (P x)) ->
hunique P -> {x : _ & P x}
intros H1 [H H0].
X: Type
P: X -> Type
H1: forall x : X, IsHProp (P x)
H: hexists P
H0: atmost1P P
{x : _ & P x}
apply (@Trunc_rec (-1) (sig P) );auto.
X: Type
P: X -> Type
H1: forall x : X, IsHProp (P x)
H: hexists P
H0: atmost1P P
IsHProp {x : _ & P x}
by apply hprop_allpath, atmost.
Qed.

Lemma unique_choice {X Y} (R:X->Y->Type) :
 (forall x y, IsHProp (R x y)) -> (forall x, (hunique (R x)))
   -> {f : X -> Y & forall x, (R x (f x))}.
X, Y: Type
R: X -> Y -> Type
(forall (x : X) (y : Y), IsHProp (R x y)) ->
(forall x : X, hunique (R x)) ->
{f : X -> Y & forall x : X, R x (f x)}
intros X0 X1.
X, Y: Type
R: X -> Y -> Type
X0: forall (x : X) (y : Y), IsHProp (R x y)
X1: forall x : X, hunique (R x)
{f : X -> Y & forall x : X, R x (f x)}
exists (fun x:X => (pr1 (iota _ (X0 x) (X1 x)))).
X, Y: Type
R: X -> Y -> Type
X0: forall (x : X) (y : Y), IsHProp (R x y)
X1: forall x : X, hunique (R x)
forall x : X, R x (iota (R x) (X0 x) (X1 x)).1
intro x.
X, Y: Type
R: X -> Y -> Type
X0: forall (x : X) (y : Y), IsHProp (R x y)
X1: forall x : X, hunique (R x)
x: X
R x (iota (R x) (X0 x) (X1 x)).1 exact (pr2 (iota _ (X0 x) (X1 x))).
Qed.