Definition iscontr_rect_compute X (is : iscontr X) (x : X) (P : X ->UU) (p : P x) : iscontr_rect X is x P p x = p. Proof. intros. unfold iscontr_rect. now rewrite iscontr_adjointness. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.