Lemma BinCoproducts_slice_precat (x : C) : BinCoproducts (C / x). Proof. intros a b. use make_BinCoproduct. + exists (BinCoproductObject (BC (pr1 a) (pr1 b))). apply (BinCoproductArrow _ (pr2 a) (pr2 b)). + use tpair. - apply BinCoproductIn1. - abstract (cbn; rewrite BinCoproductIn1Commutes; apply idpath). + use tpair. - apply BinCoproductIn2. - abstract (cbn; rewrite BinCoproductIn2Commutes; apply idpath). + intros c f g. use unique_exists. - exists (BinCoproductArrow _ (pr1 f) (pr1 g)). abstract (apply pathsinv0, BinCoproductArrowUnique; [ rewrite assoc, (BinCoproductIn1Commutes C _ _ (BC (pr1 a) (pr1 b))), (pr2 f); apply idpath | rewrite assoc, (BinCoproductIn2Commutes C _ _ (BC (pr1 a) (pr1 b))), (pr2 g)]; apply idpath). - abstract (split; apply eq_mor_slicecat; simpl; [ apply BinCoproductIn1Commutes | apply BinCoproductIn2Commutes ]). - abstract (intros y; apply isapropdirprod; apply has_homsets_slice_precat). - abstract (intros y [<- <-]; apply eq_mor_slicecat, BinCoproductArrowUnique; 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.