Definition funfibtototal {X} (P Q:X->Type) (f:∏ x:X, P x -> Q x) : total2 P -> total2 Q. Proof. intros [x p]. exact (x,,f x p). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.