Definition lift_unique_sopfib_map {E B : category} (F : E ⟶ B) {e : E} {b : B} (f : F e --> b) (bb₁ bb₂ : E) (ff₁ : e --> bb₁) (β₁ : z_iso b (F bb₁)) (ff₂ : e --> bb₂) (β₂ : z_iso b (F bb₂)) (over₁ : # F (ff₁) = f · β₁) (over₂ : # F (ff₂) = f · β₂) (cart₁ : is_opcartesian_sopfib F ff₁) (cart₂ : is_opcartesian_sopfib F ff₂) : bb₁ --> bb₂. Proof. use (opcartesian_factorization_sopfib F cart₁ ff₂ (inv_from_z_iso β₁ · β₂) _). abstract (rewrite over₁, over₂ ; rewrite !assoc' ; apply maponpaths ; rewrite !assoc ; rewrite z_iso_inv_after_z_iso ; 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.