Definition is_opcartesian_to_is_opcartesian_sopfib {e₁ e₂ : E} (f : e₁ --> e₂) (H : is_opcartesian (pr2 f)) : is_opcartesian_sopfib P f. Proof. intros z g h p. pose (lift := H (pr1 z) (pr2 z) h (transportf (λ z, _ -->[ z ] _) p (pr2 g))). use iscontraprop1. - exact (is_opcartesian_to_unique_sopfib _ H _ _ p). - simple refine ((h ,, pr11 lift) ,, (idpath _ ,, _)) ; cbn. abstract (pose (pr21 lift) as q ; cbn in q ; use total2_paths_f ; [ exact (!p) | cbn ; rewrite q ; 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.