Definition is_monic_cod_fib_weq {C : category} {y : C} {xf xg : C/y} (h : xf --> xg) : isMonic h ≃ isMonic (dom_mor h). Proof. use weqimplimpl. - exact (from_is_monic_cod_fib h). - exact (is_monic_cod_fib h). - apply isapropisMonic. - apply isapropisMonic. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.