Proposition disp_mono_codomain_functor_ess_surj (HF' : essentially_surjective F) (HF'' : fully_faithful F) : disp_functor_disp_ess_surj disp_mono_codomain_functor. Proof. intros x gy. pose proof (HF' (mono_cod_dom gy)) as H. revert H. use factor_through_squash_hProp. intros z. induction z as [ z f ]. simple refine (hinhpr (_ ,, _)). - use make_mono_cod_fib_ob. + exact z. + use make_Monic. * exact (fully_faithful_inv_hom HF'' z x (f · mono_cod_mor gy)). * abstract (intros w g h p ; use (invmaponpathsweq (make_weq _ (HF'' w z))) ; cbn ; use (cancel_z_iso _ _ f) ; use (MonicisMonic _ (mono_cod_mor gy)) ; rewrite !assoc' ; pose (maponpaths (λ z, #F z) p) as q ; cbn -[fully_faithful_inv_hom] in q ; rewrite !functor_comp in q ; refine (!_ @ q @ _) ; apply maponpaths ; apply (homotweqinvweq (make_weq _ (HF'' z x)))). - simple refine ((_ ,, tt) ,, _). + refine (pr1 f ,, _). abstract (cbn ; rewrite id_right ; refine (!_) ; apply (homotweqinvweq (make_weq _ (HF'' z x)))). + use is_z_iso_disp_mono_codomain'. apply f. Qed.
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.