Lemma is_left_adjoint_bincoproduct_functor : is_left_adjoint (bincoproduct_functor PC). Proof. apply (tpair _ (bindelta_functor _)). use tpair. - split. + use tpair. * simpl; intro p; set (x := pr1 p); set (y := pr2 p). split; [ apply (BinCoproductIn1 (PC x y)) | apply (BinCoproductIn2 (PC x y)) ]. * abstract (intros p q f; unfold catbinprodmor, compose; simpl; now rewrite BinCoproductOfArrowsIn1, BinCoproductOfArrowsIn2). + use tpair. * intro x; apply (BinCoproductArrow _ (identity x) (identity x)). * abstract (intros p q f; simpl; now rewrite precompWithBinCoproductArrow, postcompWithBinCoproductArrow, id_right, id_left). - abstract (split; simpl; intro x; [ cbn; rewrite precompWithBinCoproductArrow, !id_right; apply pathsinv0, BinCoproduct_endo_is_identity; [ apply BinCoproductIn1Commutes | apply BinCoproductIn2Commutes ] | unfold catbinprodmor, compose; simpl; now rewrite BinCoproductIn1Commutes, BinCoproductIn2Commutes ]). 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.