Definition isPullback_cartesian_in_cod_disp {x₁ x₂ : C } {f : x₁ --> x₂} {gy₁ : disp_codomain _ x₁} {hy₂ : disp_codomain _ x₂} (ff : gy₁ -->[ f ] hy₂) (H : isPullback (pr2 ff)) : is_cartesian ff. Proof. intros w φ vψ kp. use iscontraprop1. - exact (cartesian_cod_disp_unique ff H φ vψ kp). - simple refine ((_ ,, _) ,, _). + exact (cartesian_cod_disp_map ff H φ vψ kp). + exact (cartesian_cod_disp_comm_pr2 ff H φ vψ kp). + use subtypePath ; [ intro ; apply homset_property | ]. exact (cartesian_cod_disp_comm_pr1 ff H φ vψ kp). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.