Lemma slice_precat_ColimCocone (d : diagram g (C / x)) (H : ColimCocone (mapdiagram U d)) : ColimCocone d. 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.
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.