Definition make_mono_cod_fib_mor {x : C} {f₁ f₂ : C /m x} (g : mono_cod_dom f₁ --> mono_cod_dom f₂) (p : g · mono_cod_mor f₂ = mono_cod_mor f₁) : f₁ --> f₂. Proof. refine ((g ,, _) ,, tt). exact (p @ !(id_right _)). 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.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.