Definition pre_comp_post_comp_commute {b₁ b₂ : B} (f : b₁ --> b₂) {c₁ c₂ : B} (g : c₁ --> c₂) : pre_comp c₁ f ∙ post_comp b₁ g ⟹ post_comp b₂ g ∙ pre_comp c₂ f. Proof. use make_nat_trans. - exact (λ _, rassociator _ _ _). - abstract (intros h₁ h₂ α ; cbn ; rewrite rwhisker_lwhisker_rassociator ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Import PullbackFunctions.Notations. Require Import UniMath.Bicategories.Limits.PullbackEquivalences. Require Import UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits.