Definition to_fully_faithful_slice (Hα : fully_faithful_1cell (pr1 α)) : fully_faithful_1cell α. Proof. use make_fully_faithful. - apply to_faithful_slice. exact (pr1 Hα). - intros g β₁ β₂ pf. simple refine ((_ ,, _) ,, _). + exact (fully_faithful_1cell_inv_map Hα (pr1 pf)). + abstract (cbn ; use (vcomp_rcancel (_ ◃ pr12 α)) ; [ is_iso ; apply property_from_invertible_2cell | ] ; rewrite !vassocl ; rewrite vcomp_whisker ; use (vcomp_rcancel (lassociator _ _ _)) ; [ is_iso | ] ; rewrite !vassocl ; rewrite <- rwhisker_rwhisker ; rewrite (fully_faithful_1cell_inv_map_eq Hα (pr1 pf)) ; refine (_ @ pr2 pf) ; cbn ; rewrite !vassocl ; apply idpath). + abstract (use eq_2cell_slice ; cbn ; apply (fully_faithful_1cell_inv_map_eq Hα (pr1 pf))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.Eso. Section FromMorphismInSlice. Section FromFullyFaithfulSlice. End FromFullyFaithfulSlice. End FromMorphismInSlice.