Definition prefibration_w_precart_closed_implies_fibration {C : category} {D : disp_cat C} (lift : precleaving D) : precleaving_comp_is_precart lift -> precleaving_is_cleaving lift. Proof. unfold precleaving_comp_is_precart, precleaving_is_cleaving. intros liftclosed c c' f d. unfold is_cartesian. intros c'' g d'' hh. apply iscontraprop1. - apply invproofirrelevance. unfold isProofIrrelevant. intros [gg0 comm0] [gg1 comm1]. apply subtypePairEquality. + intro gg. apply homsets_disp. + eapply transportf_cancel. eapply pathscomp0. * apply pathsinv0. use precartesian_factorisation_commutes. 3: { use precartesian_lift_is_precartesian. apply lift. } * eapply pathscomp0. 2: { use precartesian_factorisation_commutes. 3: { use precartesian_lift_is_precartesian. apply lift. } } -- apply maponpaths_2. eapply precartesian_factorisation_unique. ++ apply liftclosed. ++ apply assoc_eq_var. eapply pathscomp0. ** apply maponpaths_2. apply precartesian_factorisation_commutes. ** eapply pathscomp0. --- eapply pathscomp0. +++ apply mor_disp_transportf_postwhisker. +++ eapply pathscomp0. *** apply maponpaths. exact (comm0 @ ! comm1). *** apply pathsinv0. apply mor_disp_transportf_postwhisker. --- apply pathsinv0. apply maponpaths_2. apply precartesian_factorisation_commutes. - use tpair. + apply (transportf _ (id_left _)). eapply comp_disp. 2: { apply lift. } eapply precartesian_factorisation. * apply liftclosed. * exact hh. + simpl. eapply pathscomp0. * eapply pathscomp0. -- apply mor_disp_transportf_postwhisker. -- eapply pathscomp0. ++ apply maponpaths. apply assoc_disp_var. ++ eapply pathscomp0. ** apply transport_f_f. ** apply maponpaths_2. apply homset_property. * apply transportf_transpose_left. apply precartesian_factorisation_commutes. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. 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.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.DisplayedCats.MoreFibrations.Prefibrations. Require Import UniMath.CategoryTheory.DisplayedCats.MoreFibrations.CartesiannessOfComposites.