Definition one_types_universal_coprod_map (W : @bincoprod_cocone ∁ (hfp_HLevel 3 ι₁ h) (hfp_HLevel 3 ι₂ h)) : ∏ (z : pr1 Z) (q : pr1 X ⨿ pr1 Y) (p : h z = q), pr11 W. Proof. intros z q. induction q as [ x | y ]. - intro p. refine (bincoprod_cocone_inl W _). exact ((x ,, z) ,, p). - intro p. refine (bincoprod_cocone_inr W _). exact ((y ,, z) ,, 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.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.