Definition is_cartesian_comp_disp {C : category} {D : disp_cat C} {x : C} {xx : D x} {y : C} {yy : D y} {z : C} {zz : D z} {f : x --> y} {g : y --> z} {ff : xx -->[ f ] yy} {gg : yy -->[ g ] zz} (Hff : is_cartesian ff) (Hgg : is_cartesian gg) : is_cartesian (ff ;; gg)%mor_disp. Proof. intros w h ww hh'. use iscontraprop1. - abstract (use invproofirrelevance ; intros f₁ f₂ ; use subtypePath ; [ intro ; apply D | ] ; use (cartesian_factorisation_unique Hff) ; use (cartesian_factorisation_unique Hgg) ; rewrite !assoc_disp_var ; rewrite (pr2 f₁), (pr2 f₂) ; apply idpath). - simple refine (_ ,, _). + exact (cartesian_factorisation Hff h (cartesian_factorisation Hgg (h · f) (transportf (λ z, _ -->[ z ] _) (assoc _ _ _) hh'))). + abstract (simpl ; rewrite assoc_disp ; 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.