Definition homotsec_natural_natural {X Y : UU} {f g : X → Y} (e : f ~ g) {x y : X} {p q : x = y} (h : p = q) : maponpaths (λ s : g x = g y, e x @ s) (maponpaths (maponpaths g) h) @ homotsec_natural e q = homotsec_natural e p @ maponpaths (λ s : f x = f y, s @ e y) (maponpaths (maponpaths f) h). Proof. induction h. exact (!(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. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Core.Examples.TwoType. Require Import UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor.