proposition: Lemma bin_coproducts_in_full_subcategory {C : category} (C' : hsubtype (ob C)) (BPC : BinCoproducts C) (all : ∏ c1 c2 : ob C, C' c1 -> C' c2 -> C' (BinCoproductObject (BPC c1 c2))) : BinCoproducts (full_sub_precategory C').
proof: Proof. intros c1' c2'. pose (c1'_in_C := (precategory_object_from_sub_precategory_object _ _ c1')). pose (c2'_in_C := (precategory_object_from_sub_precategory_object _ _ c2')). use tpair; [use tpair|]; [|use make_dirprod|]. - use precategory_object_in_subcat. + apply (BinCoproductObject (BPC c1'_in_C c2'_in_C)). + apply all. * exact (pr2 c1'). * exact (pr2 c2'). - use morphism_in_full_subcat; apply BinCoproductIn1. - use morphism_in_full_subcat; apply BinCoproductIn2. - cbn. unfold isBinCoproduct. intros bp' f g. use tpair. + use tpair. * use precategory_morphisms_in_subcat; [apply BinCoproductArrow|exact tt]; apply (precategory_morphism_from_sub_precategory_morphism _ (full_sub_precategory C')); assumption. * cbn. use make_dirprod; apply eq_in_sub_precategory. { apply BinCoproductIn1Commutes. } { apply BinCoproductIn2Commutes. } + intros otherarrow. apply subtypePath. { intro. apply isapropdirprod; apply is_set_sub_precategory_morphisms. } { apply eq_in_sub_precategory. cbn. apply BinCoproductArrowUnique. - exact (maponpaths pr1 (dirprod_pr1 (pr2 otherarrow))). - exact (maponpaths pr1 (dirprod_pr2 (pr2 otherarrow))). } Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Subcategory.Full UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits