Lemma is_left_adjoint_slicecat_to_cat (BPC : BinProducts C) : is_left_adjoint slicecat_to_cat. Proof. exists (cat_to_slicecat BPC). use make_are_adjoints. + use make_nat_trans. * simpl; intros F. exists (BinProductArrow _ _ (pr2 F) (identity _)); simpl. abstract (rewrite BinProductPr1Commutes; apply idpath). * intros Y Z F; apply eq_mor_slicecat; simpl. rewrite postcompWithBinProductArrow. apply BinProductArrowUnique. - rewrite <- assoc, BinProductPr1Commutes, id_right, (pr2 F); apply idpath. - rewrite <- assoc, BinProductPr2Commutes, id_left, id_right; apply idpath. + use make_nat_trans. * intros Y. apply BinProductPr2. * abstract ( intros Y Z f; apply BinProductOfArrowsPr2 ). + split. * intros Y; cbn. rewrite BinProductPr2Commutes; apply idpath. * intros Y; apply eq_mor_slicecat; cbn. rewrite postcompWithBinProductArrow. apply pathsinv0, BinProductArrowUnique; trivial. rewrite id_right, id_left; apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis.