Definition toforallpaths_funextsec_comp {T : UU} {P : T -> UU} (f g : ∏ t, P t) : toforallpaths P f g ∘ funextsec P f g = idfun _. Proof. apply funextsec; intro. simpl. apply toforallpaths_funextsec. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.