Definition psfunctor_equifier_cone {x y : B₁} {f g : x --> y} {α β : f ==> g} (p : equifier_cone f g α β) : equifier_cone (#F f) (#F g) (##F α) (##F β). Proof. refine (make_equifier_cone (F p) (#F (equifier_cone_pr1 p)) _). abstract (pose (maponpaths (λ z, psfunctor_comp F (equifier_cone_pr1 p) f • ##F z • (psfunctor_comp F (equifier_cone_pr1 p) g)^-1) (equifier_cone_eq p)) as q ; cbn -[psfunctor_comp] in q ; rewrite !psfunctor_lwhisker in q ; rewrite !vassocl in q ; rewrite !vcomp_rinv in q ; rewrite !id2_right in q ; exact q). 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.Morphisms.Adjunctions. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers. Require Import UniMath.Bicategories.Colimits.Initial. Require Import UniMath.Bicategories.Colimits.Coproducts.