Definition lift_unique_sfib_map {E B : category} (F : E ⟶ B) {e : E} {b : B} (f : b --> F e) (bb₁ bb₂ : E) (ff₁ : bb₁ --> e) (β₁ : z_iso (F bb₁) b) (ff₂ : bb₂ --> e) (β₂ : z_iso (F bb₂) b) (over₁ : # F (ff₁) = β₁ · f) (over₂ : # F (ff₂) = β₂ · f) (cart₁ : is_cartesian_sfib F ff₁) (cart₂ : is_cartesian_sfib F ff₂) : bb₁ --> bb₂. Proof. refine (cartesian_factorization_sfib F cart₂ ff₁ (β₁ · inv_from_z_iso β₂) _). abstract (rewrite over₁, over₂ ; rewrite !assoc' ; apply maponpaths ; rewrite !assoc ; rewrite z_iso_after_z_iso_inv ; rewrite id_left ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.