Definition weqfibtototal_comp {X} (P Q:X->Type) (f:∏ x:X, (P x) ≃ (Q x)) : invmap (weqfibtototal P Q f) = funfibtototal Q P (λ x, invmap (f x)). Proof. intros. apply funextsec; intros [x q]. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.