Definition compute_pr2_invmap_weqfibtototal {T} {P Q:T->Type} (f:∏ t, (P t) ≃ (Q t)) (w:total2 Q) : pr2 (invmap (weqfibtototal P Q f) w) = invmap (f (pr1 w)) (pr2 w). Proof. intros. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.