proposition: Lemma is_left_adjoint_coproduct_functor : is_left_adjoint (coproduct_functor I PC).
proof: Proof. apply (tpair _ (delta_functor _ _)). use tpair. - split. + use tpair. * intros p i; apply CoproductIn. * abstract (intros p q f; apply funextsec; intro i; unfold compose; simpl; now rewrite CoproductOfArrowsIn). + use tpair. * intro x; apply (CoproductArrow _ _ _ (λ _, identity x)). * abstract (intros p q f; simpl; now rewrite precompWithCoproductArrow, postcompWithCoproductArrow, id_right, id_left). - abstract (split; simpl; intro x; [ cbn; rewrite precompWithCoproductArrow; apply pathsinv0, Coproduct_endo_is_identity; intro i; eapply pathscomp0; [|apply CoproductInCommutes]; apply maponpaths, maponpaths, funextsec; intro j; apply id_right | apply funextsec; intro i; apply (CoproductInCommutes _ _ (λ _, x))]). 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