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. 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.
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.