proposition: Proposition is_cartesian_indexed_cat {x y : C} {f : x --> y} {xx : Φ x} {yy : Φ y} (ff : xx --> (Φ $ f) yy) (Hff : is_z_isomorphism ff) : @is_cartesian _ indexed_cat_to_disp_cat y x f yy xx ff.
proof: Proof. intros w g ww hh ; cbn in *. use iscontraprop1. - exact (is_cartesian_indexed_cat_factorisation_unique Hff g hh). - simple refine (_ ,, _). + exact (is_cartesian_indexed_cat_factorisation Hff g hh). + exact (is_cartesian_indexed_cat_factorisation_commutes Hff g hh). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.IndexedCategories.IndexedCategory