Definition disp_codomain_cleaving {C : category} (H : Pullbacks C) : cleaving (disp_codomain C). Proof. intros x₁ x₂ f yg. pose (y := pr1 yg). pose (g := pr2 yg). pose (P := H _ _ _ g f). simple refine (_ ,, (_ ,, _) ,, _). - exact (PullbackObject P ,, PullbackPr2 P). - exact (PullbackPr1 P). - exact (PullbackSqrCommutes P). - use isPullback_cartesian_in_cod_disp. apply P. 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.