Definition mono_cod_disp_cleaving {C : category} (H : Pullbacks C) : cleaving (disp_mono_codomain C). Proof. intros x₁ x₂ f yg. pose (y := pr11 yg). pose (g := pr21 yg). pose (P := H _ _ _ g f). simple refine (_ ,, ((_ ,, _) ,, tt) ,, _). - refine ((PullbackObject P ,, PullbackPr2 P) ,, _). use (MonicPullbackisMonic _ (make_Monic _ _ _) _ P). exact (pr2 yg). - exact (PullbackPr1 P). - exact (PullbackSqrCommutes P). - use isPullback_cartesian_in_mono_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.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.