Definition isaprop_cartesian_lifts {C : category} {D : disp_cat C} (D_cat : is_univalent_disp D) {c} (d : D c) {c' : C} (f : c' --> c) : isaprop (cartesian_lift d f). Proof. apply invproofirrelevance; intros fd fd'. use total2_paths_f. { apply (isotoid_disp D_cat (idpath _)); cbn. apply cartesian_lifts_iso. } apply subtypePath. { intros ff. repeat (apply impred; intro). apply isapropiscontr. } etrans. { exact (! transport_map (λ x:D c', pr1) _ _). } cbn. etrans. apply transportf_precompose_disp. rewrite idtoiso_isotoid_disp. use (pathscomp0 (maponpaths _ _) (transportfbinv _ _ _)). apply (precomp_with_z_iso_disp_is_inj (cartesian_lifts_iso fd fd')). etrans. apply assoc_disp. etrans. eapply transportf_bind, cancel_postcomposition_disp. use inv_mor_after_z_iso_disp. etrans. eapply transportf_bind, id_left_disp. apply pathsinv0. etrans. apply mor_disp_transportf_prewhisker. etrans. eapply transportf_bind, cartesian_lifts_iso_commutes. apply maponpaths_2, 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.