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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.