Proposition disp_mono_codomain_functor_ff (HF' : fully_faithful F) : disp_functor_ff disp_mono_codomain_functor. Proof. intros x₁ x₂ gy₁ gy₂ f. use isweqimplimpl. - intros ff. simple refine ((_ ,, _) ,, tt). + exact (fully_faithful_inv_hom HF' _ _ (pr11 ff)). + use (invmaponpathsweq (make_weq _ (HF' _ _))). cbn -[fully_faithful_inv_hom]. rewrite !functor_comp. refine (_ @ pr21 ff). apply maponpaths_2. apply (homotweqinvweq (make_weq _ (HF' _ _))). - apply locally_propositional_mono_cod_disp_cat. - apply locally_propositional_mono_cod_disp_cat. 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.