Definition total2_contr {X : UU} (P : X → UU) (H : ∏ x, iscontr (P x)) : (∑ x, P x) ≃ X. Proof. use weq_iso. - exact pr1. - intro x. exact (x ,, iscontrpr1 (H x)). - abstract ( intro x; apply subtypePath; [ intro; apply isapropifcontr; apply H | reflexivity ] ). - reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.