proposition: Lemma is_split_fibration_from_discrete_fibration {C : category} {D : disp_cat C} (X : is_discrete_fibration D) : is_split (fibration_from_discrete_fibration _ (D,,X)).
proof: Proof. repeat split. - intros c d. cbn. use tpair. + apply pathsinv0. apply path_to_ctr. apply id_disp. + cbn. apply (disp_mor_unique_disc_fib _ (D,,X)). - intros c c' c'' f g d. cbn. use tpair. + set (XR := unique_lift f d). set (d' := pr1 (iscontrpr1 XR)). set (f' := pr2 (iscontrpr1 XR)). cbn in f'. set (g' := pr2 (iscontrpr1 (unique_lift g d'))). cbn in g'. set (gf' := g' ;; f'). match goal with |[ |- ?a = ?b ] => assert (X0 : (a,,pr2 (iscontrpr1 (unique_lift (g · f) d))) = (b,,gf')) end. { apply proofirrelevancecontr. apply X. } apply (maponpaths pr1 X0). + apply (disp_mor_unique_disc_fib _ (D,,X)). - apply isaset_fiber_discrete_fibration. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Presheaf UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Examples.Opposite