Definition is_eso_closed_under_pb_one_types : is_eso_closed_under_pb (_ ,, one_types_has_pb). Proof. intros X Y Z f Hf' g ; cbn in *. use issurjective_is_eso. pose (Hf := is_eso_issurjective Hf'). intros y. use (factor_through_squash _ _ (Hf (g y))). { apply ishinh. } intros x. apply hinhpr. exact (((pr1 x ,, y) ,, !(pr2 x)) ,, idpath _). 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.