proposition: Lemma is_left_adjoint_delta_functor : is_left_adjoint (delta_functor I C).
proof: Proof. apply (tpair _ (product_functor _ PC)). use tpair. - split. + use tpair. * simpl; intro x. apply (ProductArrow _ _ _ (λ _, identity x)). * abstract (intros p q f; simpl; now rewrite precompWithProductArrow, id_right, postcompWithProductArrow, id_left). + use tpair. * intros x i; apply ProductPr. * abstract (intros p q f; apply funextsec; intro i; unfold compose; simpl; now rewrite ProductOfArrowsPr). - abstract (split; simpl; intro x; [ apply funextsec; intro i; apply (ProductPrCommutes _ _ (λ _, x)) | cbn; rewrite postcompWithProductArrow; apply pathsinv0, Product_endo_is_identity; intro i; eapply pathscomp0; [|apply (ProductPrCommutes I C _ (PC x))]; apply cancel_postcomposition, maponpaths, funextsec; intro j; apply id_left]). 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