Lemma bin_products_in_full_subcategory {C : category} (C' : hsubtype (ob C)) (BPC : BinProducts C) (all : ∏ c1 c2 : ob C, C' c1 -> C' c2 -> C' (BinProductObject _ (BPC c1 c2))) : BinProducts (full_sub_precategory C'). 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 (BinProductObject _ (BPC c1'_in_C c2'_in_C)). + apply all. * exact (pr2 c1'). * exact (pr2 c2'). - use morphism_in_full_subcat; apply BinProductPr1. - use morphism_in_full_subcat; apply BinProductPr2. - cbn. unfold isBinProduct. intros bp' f g. use tpair. + use tpair. * use precategory_morphisms_in_subcat; [apply BinProductArrow|exact tt]; apply (precategory_morphism_from_sub_precategory_morphism _ (full_sub_precategory C')); assumption. * cbn. use make_dirprod; apply eq_in_sub_precategory. { apply BinProductPr1Commutes. } { apply BinProductPr2Commutes. } + intros otherarrow. apply subtypePath. { intro. apply isapropdirprod; apply is_set_sub_precategory_morphisms. } { apply eq_in_sub_precategory. cbn. apply BinProductArrowUnique. - exact (maponpaths pr1 (dirprod_pr1 (pr2 otherarrow))). - exact (maponpaths pr1 (dirprod_pr2 (pr2 otherarrow))). } Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.