Corollary weqsecovercontr': ∏ (X:UU) (P:X->UU) (is:iscontr X), (∏ x:X, P x) ≃ P (pr1 is). Proof. intros. set (x0 := pr1 is). set (secs := ∏ x : X, P x). set (fib := P x0). set (destr := (λ f, f x0) : secs->fib). set (constr:= iscontr_rect X is x0 P : fib->secs). exists destr. apply (isweq_iso destr constr). - intros f. apply funextsec; intros x. unfold destr, constr. apply transport_section. - apply iscontr_rect_compute. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.