proposition: Lemma BinCoproducts_slice_precat (x : C) : BinCoproducts (C / x).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis