Definition is_opcartesian_sopfib_to_is_opcartesian {e₁ e₂ : E} (f : e₁ --> e₂) (H : is_opcartesian_sopfib P f) : is_opcartesian (pr2 f). Proof. intros z zz g gf. pose (lift := H (z ,, zz) (pr1 f · g ,, gf) g (idpath _)). use iscontraprop1. - apply is_opcartesian_sopfib_to_unique_opcartesian. exact H. - simple refine (_ ,, _). + exact (transportf (λ z, _ -->[ z ] _) (pr121 lift) (pr211 lift)). + abstract (simpl ; pose (transportb_transpose_right (fiber_paths (pr221 lift))) as p ; rewrite mor_disp_transportf_prewhisker ; cbn in p ; refine (maponpaths _ p @ _) ; unfold transportb ; rewrite transport_f_f ; apply transportf_set ; apply homset_property). 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.