proposition: Lemma funextsec_id'' {C : univalent_category} (T : C -> C -> C) : ∏ x : C, toforallpaths (λ _ : C,C) _ _ (funextsec (λ _ : C, C) (T x) (T x) (λ x0 : C, idpath (T x x0))) = toforallpaths (λ _ : C, C) _ _ (toforallpaths (λ _ : C, C → C) T T (idpath T) x).
proof: Proof. intro x. etrans. { apply toforallpaths_funextsec. } apply funextsec ; intro y. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.Core.Univalence UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories