Lemma is_left_adjoint_bindelta_functor : is_left_adjoint (bindelta_functor C). 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.
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.