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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.