Definition decidableSubtypeCarrier_weq {X : UU} (P : DecidableSubtype X) : decidableSubtypeCarrier' P ≃ decidableSubtypeCarrier P. Proof. intros. apply weqfibtototal. intros x. unfold choice. simpl. change (pr1 (decidabilityProperty (P x))) with (pr1 (decidabilityProperty (P x))). choose (P x) p q. - simpl. apply weqiff. + apply logeq_both_true. * reflexivity. * assumption. + apply isasetbool. + apply (propproperty (DecidableProposition_to_hProp _)). - simpl. apply weqiff. + apply logeq_both_false. * exact nopathsfalsetotrue. * assumption. + apply isasetbool. + apply (propproperty (DecidableProposition_to_hProp _)). Defined.
Require Import UniMath.MoreFoundations.Tactics.