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