proposition: Lemma slice_precat_ColimCocone (d : diagram g (C / x)) (H : ColimCocone (mapdiagram U d)) : ColimCocone d.
proof: Proof. use make_ColimCocone. - use tpair. + apply (colim H). + apply colimArrow. use make_cocone. * intro v; apply (pr2 (dob d v)). * abstract (intros u v e; apply (! pr2 (dmor d e))). - use make_cocone. + intro v; simpl. use tpair; simpl. * apply (colimIn H v). * abstract (apply pathsinv0, (colimArrowCommutes H)). + abstract (intros u v e; apply eq_mor_slicecat, (coconeInCommutes (colimCocone H))). - intros y ccy. use unique_exists. + use tpair; simpl. * apply colimArrow, (mapcocone U _ ccy). * abstract (apply pathsinv0, colimArrowUnique; intros v; simpl; rewrite assoc; eapply pathscomp0; [apply cancel_postcomposition, (colimArrowCommutes H _ (mapcocone U _ ccy) v)|]; induction ccy as [f Hf]; simpl; apply (! pr2 (f v))). + abstract (intro v; apply eq_mor_slicecat; simpl; apply (colimArrowCommutes _ _ (mapcocone U d ccy))). + abstract (simpl; intros f; apply impred; intro v; apply has_homsets_slice_precat). + abstract (intros f Hf; apply eq_mor_slicecat; simpl in *; apply colimArrowUnique; intros v; apply (maponpaths pr1 (Hf v))). 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