Definition isPullback_cartesian_in_mono_cod_disp {C : category} {x₁ x₂ : C } {f : x₁ --> x₂} {gy₁ : disp_mono_codomain _ x₁} {hy₂ : disp_mono_codomain _ x₂} (ff : gy₁ -->[ f ] hy₂) (H : isPullback (pr21 ff)) : is_cartesian ff. Proof. intros w φ vψ kp. use iscontraprop1. - exact (cartesian_mono_cod_disp_unique ff φ vψ kp). - simple refine (((_ ,, _) ,, tt) ,, _). + exact (cartesian_mono_cod_disp_map ff H φ vψ kp). + exact (cartesian_mono_cod_disp_comm_pr2 ff H φ vψ kp). + use subtypePath ; [ intro ; apply isapropunit | ]. use subtypePath ; [ intro ; apply homset_property | ]. exact (cartesian_mono_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.Monics. 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. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma.