proposition: Lemma cartesian_functor_from_fibration {C C' : category} {F : functor C C'} {D : disp_cat C} {D' : disp_cat C'} {FF : disp_functor F D D'} (H : forall (c c' : C) (f : c' --> c) (d : D c), ∥ total2 (fun ff : cartesian_lift d f => is_cartesian (♯ FF ff)) ∥) : is_cartesian_disp_functor FF.
proof: Proof. intros c c' f d d' ff ff_cart. use (squash_to_prop (H _ _ f d)). - apply isaprop_is_cartesian. - intros [ff' ff'_cart]. use (is_cartesian_from_z_iso_to_cartesian ff'_cart). + refine (transportf (fun i => z_iso_disp i _ _) _ (@disp_functor_on_z_iso_disp _ _ _ _ _ FF _ _ _ _ (identity_z_iso _) _)). apply (z_iso_eq _ _), functor_id. refine (cartesian_lifts_iso ff' (_,,_)). exact (_,,ff_cart). + etrans. { apply maponpaths_2. refine (@pr1_transportf _ _ (fun i ff => is_z_iso_disp i ff) _ _ _ _). } etrans. { apply maponpaths_2. apply functtransportf. } etrans. { apply mor_disp_transportf_postwhisker. } etrans. { eapply maponpaths. simpl. etrans. { eapply pathsinv0, disp_functor_comp_var. } eapply transportf_bind. etrans. { apply maponpaths, cartesian_factorisation_commutes'. } apply disp_functor_transportf. } etrans. apply transport_f_f. unfold transportb. apply maponpaths_2, homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.Fibrations