Definition weqonsec {X Y} (P:X->Type) (Q:Y->Type) (f:X ≃ Y) (g:∏ x, weq (P x) (Q (f x))) : (∏ x:X, P x) ≃ (∏ y:Y, Q y). Proof. intros. exact (weqcomp (weqonsecfibers P (λ x, Q(f x)) g) (invweq (weqonsecbase Q f))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.