Definition mor_to_pb_obj_pr1 {a b₁ b₂ b₃ : B} {f : b₁ --> b₃} {g : b₂ --> b₃} (h₁ : a --> b₁) (h₂ : a --> b₂) (γ : invertible_2cell (h₁ · f) (h₂ · g)) : invertible_2cell (h₁ ⊗[ γ ] h₂ · π₁) h₁. Proof. pose (q := make_pb_cone a h₁ h₂ γ : pb_cone f g). exact (pb_ump_mor_pr1 (pr2 (pr2 B _ _ _ f g)) q). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Limits.Pullbacks.