fact: Definition homothomotsec_natural {X Y : UU} {f g : X → Y} {e₁ e₂ : f ~ g} (h : e₁ ~ e₂) {x y : X} (p : x = y) : homotsec_natural e₁ p @ maponpaths (λ s : f y = g y, maponpaths f p @ s) (h y) = maponpaths (λ s : f x = g x, s @ maponpaths g p) (h x) @ homotsec_natural e₂ p.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.Core.Examples.TwoType UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor UniMath.Bicategories.Transformations.Examples.ApTransformation