Definition disp_mono_codomain_functor_data : disp_functor_data F (disp_mono_codomain C₁) (disp_mono_codomain C₂). Proof. simple refine (_ ,, _). - refine (λ x gy, make_mono_cod_fib_ob (make_Monic _ (#F (mono_cod_mor gy)) _)). abstract (apply HF ; apply MonicisMonic). - simple refine (λ x₁ x₂ gy₁ gy₂ f p, (#F (pr11 p) ,, _) ,, tt). abstract (cbn ; rewrite <- !functor_comp ; apply maponpaths ; exact (pr21 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod.