Definition weq_over_sections {S T} (w:S ≃ T) {s0:S} {t0:T} (k:w s0 = t0) {P:T->Type} (p0:P t0) (pw0:P(w s0)) (l:k#pw0 = p0) (H:(∏ t, P t) -> UU) (J:(∏ s, P(w s)) -> UU) (g:∏ f:(∏ t, P t), weq (H f) (J (maponsec1 P w f))) : weq (hfiber (λ fh:total2 H, pr1 fh t0) p0 ) (hfiber (λ fh:total2 J, pr1 fh s0) pw0). Proof. intros. simple refine (weqbandf _ _ _ _). { simple refine (weqbandf _ _ _ _). { exact (weqonsecbase P w). } { unfold weqonsecbase; simpl. exact g. } } { intros [f h]. simpl. unfold maponsec1; simpl. induction k, l; simpl. unfold transportf; simpl. apply idweq. } Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.