Definition is_cartesian_transportf {C : category} {D : disp_cat C} {x y : C} {f f' : x --> y} (p : f = f') {xx : D x} {yy : D y} {ff : xx -->[ f ] yy} (Hff : is_cartesian ff) : is_cartesian (transportf (λ z, _ -->[ z ] _) p ff). Proof. intros c g cc gg. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply D | ] ; use (cartesian_factorisation_unique Hff) ; pose (p₁ := pr2 φ₁) ; pose (p₂ := pr2 φ₂) ; cbn in p₁, p₂ ; rewrite mor_disp_transportf_prewhisker in p₁ ; rewrite mor_disp_transportf_prewhisker in p₂ ; pose (transportb_transpose_right p₁) as r₁ ; pose (transportb_transpose_right p₂) as r₂ ; exact (r₁ @ !r₂)). - simple refine (_ ,, _). + exact (cartesian_factorisation Hff g (transportb (λ z, _ -->[ z ] _) (maponpaths (λ z, g · z) p) gg)). + abstract (cbn ; rewrite mor_disp_transportf_prewhisker ; rewrite cartesian_factorisation_commutes ; unfold transportb ; rewrite transport_f_f ; apply transportf_set ; apply homset_property). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite. Section IsoCleavingFromOpcleaving. End IsoCleavingFromOpcleaving.