Definition issurjective_is_eso_essentially_surjective {X₁ X₂ : one_types} {f : X₁ --> X₂} (Hf : issurjective f) : is_eso_essentially_surjective f. Proof. intros Y₁ Y₂ m Hm' g₁ g₂ p. pose (Hm := one_types_fully_faithful_isInjective _ Hm'). simple refine (_ ,, _ ,, _ ,, _). - exact (issurjective_is_eso_lift_1 Hf Hm p). - use make_invertible_2cell. + exact (issurjective_is_eso_lift_1_left Hf Hm p). + apply one_type_2cell_iso. - use make_invertible_2cell. + exact (issurjective_is_eso_lift_1_right Hf Hm p). + apply one_type_2cell_iso. - exact (issurjective_is_eso_lift_1_eq Hf Hm p). 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.Core.Examples.OneTypes. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.Eso. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Examples.OneTypesLimits.