Definition cartesian_1cell_pb_2cell_pr2 : cartesian_1cell_pb_2cell ▹ pb_cone_pr2 pb = β. Proof. pose (maponpaths pr1 (cartesian_1cell_lift_2cell_commutes _ _ Hp σσ φ_lift ψ_lift)) as d'. assert (d : (pr1 (cartesian_1cell_lift_2cell (cod_disp_bicat B) (π,, p) Hp σσ φ_lift ψ_lift) ▹ π) • id₂ (ψ · π) = id₂ (φ · π) • β). { etrans; [| exact d']. refine (!_). etrans; [refine (pr1_transportf (id2_right (id₂ (pr2 hx) ▹ f) @ ! id2_left (id₂ (pr2 hx) ▹ f)) _) |]. cbn. rewrite transportf_const. apply idpath. } rewrite id2_right, id2_left in d. exact d. Qed. Section Uniqueness. Context (τ₁ τ₂ : φ ==> ψ) (pr1τ₁ : τ₁ ▹ pb_cone_pr1 pb = α) (pr2τ₁ : τ₁ ▹ pb_cone_pr2 pb = β) (pr1τ₂ : τ₂ ▹ pb_cone_pr1 pb = α) (pr2τ₂ : τ₂ ▹ pb_cone_pr2 pb = β). Let lift_τ₁ : φ_lift ==>[ id₂ (pr2 hx)] ψ_lift. Proof. use make_disp_2cell_cod. - exact τ₁. - abstract (unfold coherent_homot ; cbn ; rewrite lwhisker_id2, !id2_left ; exact pr1τ₁). 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. 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.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Codomain. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OneTypesLimits.