Lemma Coproducts_slice_precat (x : C) : Coproducts I (C / x). Proof. intros a. use make_Coproduct. + exists (CoproductObject _ _ (BC (λ i, pr1 (a i)))). apply CoproductArrow; intro i; apply (pr2 (a i)). + intro i; use tpair; simpl. - apply (CoproductIn I C (BC (λ i, pr1 (a i))) i). - abstract (rewrite (CoproductInCommutes I C _ (BC (λ i, pr1 (a i)))); apply idpath). + intros c f. use unique_exists. - exists (CoproductArrow _ _ _ (λ i, pr1 (f i))). abstract (simpl; apply pathsinv0, CoproductArrowUnique; intro i; rewrite assoc, (CoproductInCommutes _ _ _ (BC (λ i, pr1 (a i)))), (pr2 (f i)); apply idpath). - abstract (intros i; apply eq_mor_slicecat, (CoproductInCommutes _ _ _ (BC (λ i0 : I, pr1 (a i0))))). - abstract (intros y; apply impred; intro i; apply has_homsets_slice_precat). - abstract (simpl; intros y Hy; apply eq_mor_slicecat, CoproductArrowUnique; intros i; apply (maponpaths pr1 (Hy i))). 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.