Definition one_types_inl_inr : has_comma_ump (@biinitial_comma_cone ∁ _ _ _ ι₁ ι₂). Proof. split. - intro Z. use make_comma_1cell. + intro z. exact (fromempty (negpathsii1ii2 _ _ (comma_cone_cell Z z))). + use make_invertible_2cell. * intro z. exact (fromempty (negpathsii1ii2 _ _ (comma_cone_cell Z z))). * apply one_type_2cell_iso. + use make_invertible_2cell. * intro z. exact (fromempty (negpathsii1ii2 _ _ (comma_cone_cell Z z))). * apply one_type_2cell_iso. + abstract (use funextsec ; intro z ; exact (fromempty (negpathsii1ii2 _ _ (comma_cone_cell Z z)))). - intros Z φ ψ α β p. use iscontraprop1. + abstract (use invproofirrelevance ; intros τ₁ τ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; use funextsec ; intro z ; exact (fromempty (φ z))). + simple refine (_ ,, _ ,, _). * intro z. exact (fromempty (φ z)). * abstract (use funextsec ; intro z ; exact (fromempty (φ z))). * abstract (use funextsec ; intro z ; exact (fromempty (φ z))). 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.Examples.OneTypes. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInOneTypes. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Require Import UniMath.Bicategories.Limits.Examples.OneTypesLimits. Require Import UniMath.Bicategories.Colimits.Initial. Require Import UniMath.Bicategories.Colimits.Coproducts. Require Import UniMath.Bicategories.Colimits.Extensive.