Definition mor_preserves_cartesian_pb_ump_mor_alt {e₀ : B} (p₀ : e₀ --> b₁) (h₁ : e₀ --> e₂) (δ : invertible_2cell (h₁ · p₂) (p₀ · fb)) (cone := make_pb_cone e₀ h₁ p₀ δ) (Hh₁ : mor_preserves_cartesian p₀ p₂ h₁) : mor_preserves_cartesian p₀ p₁ (pb_ump_mor H cone). Proof. intros x f g ζ Hζ. apply to_pb_cartesian. assert (H₁ : is_cartesian_2cell_sfib p₂ (rassociator g (pb_ump_mor H cone) fe)) . { apply invertible_is_cartesian_2cell_sfib. is_iso. } assert (H₂ : is_cartesian_2cell_sfib p₂ ((g ◃ pb_ump_mor_pr1 H cone))). { apply invertible_is_cartesian_2cell_sfib. is_iso. apply property_from_invertible_2cell. } assert (H₃ : is_cartesian_2cell_sfib p₂ (rassociator f (pb_ump_mor H cone) fe • ((f ◃ pb_ump_mor_pr1 H cone) • (ζ ▹ pb_cone_pr1 cone)))). { use vcomp_is_cartesian_2cell_sfib. - apply invertible_is_cartesian_2cell_sfib. is_iso. - use vcomp_is_cartesian_2cell_sfib. + apply invertible_is_cartesian_2cell_sfib. is_iso. apply property_from_invertible_2cell. + apply Hh₁. exact Hζ. } use (is_cartesian_2cell_sfib_postcomp p₂ _ (vcomp_is_cartesian_2cell_sfib _ H₁ H₂) H₃). abstract (rewrite vassocr ; rewrite rwhisker_rwhisker_alt ; rewrite vassocl ; rewrite vcomp_whisker ; apply idpath). 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.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Morphisms.Properties.Composition. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. Section FromPBCartesian. End FromPBCartesian.