Definition to_eso_faithful_slice (Hα : is_eso (pr1 α)) : is_eso_faithful α. Proof. intros h₁ h₂ μ Hμ β₁ β₂ p₁ p₂ r₁ r₂. use eq_2cell_slice. use (is_eso_lift_eq _ Hα (from_fully_faithful_slice inv_B _ Hμ)). - exact (maponpaths pr1 r₁). - exact (maponpaths pr1 r₂). Qed. Section ToSliceEsoEssentiallySurjective. Context (Hα : is_eso (pr1 α)) {g₁ g₂ : slice_bicat b} {μ : g₁ --> g₂} (Hμ : fully_faithful_1cell μ) {β₁ : f₁ --> g₁} {β₂ : f₂ --> g₂} (p : invertible_2cell (β₁ · μ) (α · β₂)). Let γ : invertible_2cell (pr1 β₁ · pr1 μ) (pr1 α · pr1 β₂). Proof. use make_invertible_2cell. - exact (pr11 p). - 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.