proposition: Lemma is_left_adjoint_bindelta_functor : is_left_adjoint (bindelta_functor C).
proof: Proof. apply (tpair _ (binproduct_functor PC)). use tpair. - split. + use tpair. * simpl; intro x. apply (BinProductArrow _ _ (identity x) (identity x)). * abstract (intros p q f; simpl; now rewrite precompWithBinProductArrow, id_right, postcompWithBinProductArrow, id_left). + use tpair. * simpl; intro x; split; [ apply BinProductPr1 | apply BinProductPr2 ]. * abstract (intros p q f; unfold catbinprodmor, compose; simpl; now rewrite BinProductOfArrowsPr1, BinProductOfArrowsPr2). - abstract (split; simpl; intro x; [ unfold catbinprodmor, compose; simpl; now rewrite BinProductPr1Commutes, BinProductPr2Commutes | cbn; rewrite postcompWithBinProductArrow, !id_left; apply pathsinv0, BinProduct_endo_is_identity; [ apply BinProductPr1Commutes | apply BinProductPr2Commutes ]]). 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