proposition: Lemma maponpaths_funextsec {T : UU} {P : T -> UU} (f g : ∏ t, P t) (t : T) (p : f ~ g) : maponpaths (λ h, h t) (funextsec _ f g p) = p t.
proof: Proof. intermediate_path (toforallpaths _ _ _ (funextsec _ f g p) t). - generalize (funextsec _ f g p); intros q. induction q. reflexivity. - apply (eqtohomot (eqtohomot (toforallpaths_funextsec_comp f g) p) t). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.PartA