proposition: Lemma cartesian_functor_from_cleaving {C C' : category} {F : functor C C'} {D : disp_cat C} {D' : disp_cat C'} {FF : disp_functor F D D'} (clD : cleaving D) (H : forall c c' f d, is_cartesian (♯ FF (clD c c' f d))) : is_cartesian_disp_functor FF.
proof: Proof. apply cartesian_functor_from_fibration. intros c c' f d. apply hinhpr. exists (clD c c' f d). apply H. 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