fact: 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).
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.PartA