Lemma is_left_adjoint_coproduct_functor : is_left_adjoint (coproduct_functor I PC). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.whiskering.