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