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. Proof. induction p ; cbn. induction (h x). apply pathscomp0rid. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Core.Examples.TwoType. Require Import UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor. Require Import UniMath.Bicategories.Transformations.Examples.ApTransformation.