Proof that finite sets have choice

finite_choice.v

Require Import HoTT.HoTT.
Require Import HoTT.hit.minus1Trunc.

Generalizable All Variables.
Set Implicit Arguments.

Local Notation "|| T ||" := (minus1Trunc T).
(*Local Notation "| x |" := (min1 x).*)

Fixpoint Fin (n : nat) : Type :=
  match n with
    | O => Empty
    | S n' => Fin n' + Unit
  end.

Instance istrunc_fin n : IsHSet (Fin n).
Proof.
  induction n; simpl;
  typeclasses eauto.
Defined.

Class HasChoice X A (P : forall x : X, A x -> Type)
  := choice : (forall x, minus1Trunc { a : A x | P x a })
              -> minus1Trunc { g : forall x, A x | forall x, P x (g x) }.

Instance haschoice_contr X A P `{Contr X} : @HasChoice X A P.
Proof.
  intro H.
  specialize (H (center _)).
  revert H.
  apply minus1Trunc_map.
  intros [a Pa].
  exists (fun x => transport A (contr x) a).
  intro x.
  destruct (contr x).
  simpl.
  assumption.
Defined.

Instance haschoice_empty A P : @HasChoice Empty A P.
Proof.
  intro H.
  apply min1.
  exists (fun x => match x : Empty with end).
  intros [].
Defined.

Instance haschoice_sum `{Funext} X Y A (P : forall xy : X + Y, A xy -> Type)
         `{HasChoice X (fun x => A (inl x)) (fun x a => P (inl x) a)}
         `{HasChoice Y (fun y => A (inr y)) (fun y a => P (inr y) a)}
: @HasChoice (X + Y) A P.
Proof.
  intro Hc.
  assert (Hx := fun x => Hc (inl x)).
  assert (Hy := fun y => Hc (inr y)).
  clear Hc; simpl in *.
  apply choice in Hx.
  apply choice in Hy.
  revert Hy Hx.
  refine (@minus1Trunc_ind _ _ _ _).
  intro Hy.
  apply minus1Trunc_map.
  intro Hx.
  exists (fun xy => match xy as xy return A xy with
                      | inl x => Hx.1 x
                      | inr y => Hy.1 y
                    end).
  intros [x|y];
    [ apply (Hx.2)
    | apply (Hy.2) ].
Defined.

Instance haschoice_fin `{Funext} n A P : @HasChoice (Fin n) A P.
Proof.
  induction n;
  simpl in *; typeclasses eauto.
Defined.