Definition iscontr_rect_compute'' X (i : iscontr X) (P : X ->UU) (p : P(pr1 i)) : iscontr_rect'' X i P p (pr1 i) = p. Proof. try reflexivity. intros. exact (homotweqinvweq (weqsecovercontr P i) p). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.