Library HoTT.HIT.unique_choice

Require Import HoTT.Basics HoTT.Truncations.Core.

Definition atmost1 X:=(∀ x1 x2:X, (x1 = x2)).
Definition atmost1P {X} (P:X→Type):=
    (∀ 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}:
  (∀ x, IsHProp (P x)) → (atmost1P P) → atmost1 (sig P).
intros H H0 [x p] [y q].
specialize (H0 x y p q).
induction H0.
assert (H0: (p =q)) by apply path_ishprop.
now induction H0.
Qed.

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

Lemma unique_choice {X Y} (R:X→Y→Type) :
 (∀ x y, IsHProp (R x y)) → (∀ x, (hunique (R x)))
   → {f : X → Y & ∀ x, (R x (f x))}.
intros X0 X1.
∃ (fun x:X ⇒ (pr1 (iota _ (X0 x) (X1 x)))).
intro x. apply (pr2 (iota _ (X0 x) (X1 x))).
Qed.