Definition faithful_weq_slice : faithful_1cell (pr1 α) ≃ faithful_1cell α. Proof. use weqimplimpl. - apply to_faithful_slice. - apply from_faithful_slice. - apply isaprop_faithful_1cell. - apply isaprop_faithful_1cell. Qed. Section FromFullyFaithfulSlice. Context (Hα : fully_faithful_1cell α) {x : B} {g₁ g₂ : x --> pr1 f₁} (βf : g₁ · pr1 α ==> g₂ · pr1 α). Let h : slice_bicat b := make_ob_slice (g₁ · pr2 f₁). Let β₁ : h --> f₁ := @make_1cell_slice _ _ h f₁ g₁ (id2_invertible_2cell _). Let γ : invertible_2cell (g₁ · pr2 f₁) (g₂ · pr2 f₁). Proof. use make_invertible_2cell. - exact ((_ ◃ pr12 α) • lassociator _ _ _ • (βf ▹ _) • rassociator _ _ _ • (_ ◃ (pr22 α)^-1)). - apply inv_B. 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.