Lemma is_left_adjoint_delta_functor : is_left_adjoint (delta_functor I C). 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.
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.