proposition: Lemma is_left_adjoint_bincoproduct_functor : is_left_adjoint (bincoproduct_functor PC).
proof: Proof. apply (tpair _ (bindelta_functor _)). use tpair. - split. + use tpair. * simpl; intro p; set (x := pr1 p); set (y := pr2 p). split; [ apply (BinCoproductIn1 (PC x y)) | apply (BinCoproductIn2 (PC x y)) ]. * abstract (intros p q f; unfold catbinprodmor, compose; simpl; now rewrite BinCoproductOfArrowsIn1, BinCoproductOfArrowsIn2). + use tpair. * intro x; apply (BinCoproductArrow _ (identity x) (identity x)). * abstract (intros p q f; simpl; now rewrite precompWithBinCoproductArrow, postcompWithBinCoproductArrow, id_right, id_left). - abstract (split; simpl; intro x; [ cbn; rewrite precompWithBinCoproductArrow, !id_right; apply pathsinv0, BinCoproduct_endo_is_identity; [ apply BinCoproductIn1Commutes | apply BinCoproductIn2Commutes ] | unfold catbinprodmor, compose; simpl; now rewrite BinCoproductIn1Commutes, BinCoproductIn2Commutes ]). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Adjunctions.Core