Definition compute_iscontrweqb_weqfibtototal_1 {T} {P Q:T->Type} (f:∏ t, (P t) ≃ (Q t)) (is:iscontr (total2 Q)) : pr1 (iscontrpr1 (iscontrweqb (weqfibtototal P Q f) is)) = pr1 (iscontrpr1 is). Proof. intros. destruct is as [ctr uni]. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.