Lemma funextsec_toforallpaths {T : UU} {P : T -> UU} {f g : ∏ t : T, P t} : ∏ (h : f = g), funextsec _ _ _ (toforallpaths _ _ _ h) = h. Proof. intro h; exact (!homotinvweqweq0 (weqtoforallpaths _ _ _) h). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.