Definition op2_bicat_is_extensive (B : bicat_with_biinitial_bincoprod) (HB : is_extensive B) : is_extensive (op2_bicat_biinitial_coproduct B). Proof. intros x y. split. - simple refine (_ ,, _ ,, _ ,, _). + apply fully_faithful_op2_bicat. exact (pr1 (pr1 (HB x y))). + apply fully_faithful_op2_bicat. exact (pr12 (pr1 (HB x y))). + exact (op2_comma_has_comma_ump (pr222 (pr1 (HB x y)))). + exact (op2_comma_has_comma_ump (pr122 (pr1 (HB x y)))). - intros z h. pose (H := pr2 (HB x y) z h). refine (pr1 H ,, pr12 H ,, pr122 H ,, _). refine (pr1 (pr222 H) ,, pr12 (pr222 H) ,, pr122 (pr222 H) ,, _). refine (weq_op2_invertible_2cell _ _ (inv_of_invertible_2cell (pr1 (pr222 (pr222 H)))) ,, _). refine (weq_op2_invertible_2cell _ _ (inv_of_invertible_2cell (pr12 (pr222 (pr222 H)))) ,, _). simple refine (_ ,, _ ,, _). + exact (to_op2_has_pb_ump _ (pr122 (pr222 (pr222 H)))). + exact (to_op2_has_pb_ump _ (pr1 (pr222 (pr222 (pr222 H))))). + exact (has_bincoprod_ump_op_cell _ _ (pr2 (pr222 (pr222 (pr222 H))))). 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.Examples.OpCellBicat. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInOp2Bicat. Require Import UniMath.Bicategories.Colimits.Initial. Require Import UniMath.Bicategories.Colimits.Coproducts. Require Import UniMath.Bicategories.Colimits.Extensive. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits.