Definition dependent_choice {W : UU} (P : DecidableProposition) : (P -> W) -> (¬ P -> W) -> W. Proof. intros yes no. choose P p q. - exact (yes p). - exact (no q). Defined.
Require Import UniMath.MoreFoundations.Tactics.