proposition: Theorem fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice : FunctionalChoice -> ExtensionalPredicateRepresentative -> ProofIrrelevance -> RepresentativeFunctionalChoice.
proof: Proof. intros FunChoice PredExtRepr PI A R (Hrefl,Hsym,Htrans). pose (isclass P := exists x:A, P x). pose (class := {P:A -> Prop | isclass P}). pose (contains (c:class) (a:A) := proj1_sig c a). pose (class_of a := R a). destruct (FunChoice class A contains) as (f,Hf). - intros c. apply proj2_sig. - destruct (PredExtRepr A) as (h,Hh). assert (Hisclass:forall a, isclass (h (class_of a))). { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). rewrite <- Ha; apply Hrefl. } pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). exists (fun a => f (f' a)). intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + specialize Hf with (f' x). simpl in Hf. rewrite <- Hx in Hf. assumption. + intros y Hxy. f_equal. assert (Heq1: h (class_of x) = h (class_of y)). { apply Huniqx. intro z. unfold class_of. firstorder. } assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). { apply PI. } unfold f'. rewrite <- Heq2. rewrite <- Heq1. reflexivity. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts