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. apply cartesian_functor_from_fibration. intros c c' f d. apply hinhpr. exists (clD c c' f d). apply H. 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.