Lemma slice_precat_isColimCocone (d : diagram g (C / x)) (a : C / x) (cc : cocone d a) (H : isColimCocone (mapdiagram U d) (U a) (mapcocone U d cc)) : isColimCocone d a cc. Proof. set (CC := make_ColimCocone _ _ _ H). intros y ccy. use unique_exists. + use tpair; simpl. * apply (colimArrow CC), (mapcocone U _ ccy). * abstract (apply pathsinv0; eapply pathscomp0; [apply (postcompWithColimArrow _ CC (pr1 y) (mapcocone U d ccy))|]; apply pathsinv0, (colimArrowUnique CC); intros u; simpl; eapply pathscomp0; [apply (!(pr2 (coconeIn cc u)))|]; apply (pr2 (coconeIn ccy u))). + abstract (intros u; apply subtypePath; [intros xx; apply C|]; simpl; apply (colimArrowCommutes CC)). + abstract (intros f; simpl; apply impred; intro u; apply has_homsets_slice_precat). + abstract (intros f; simpl; intros Hf; apply eq_mor_slicecat; simpl; apply (colimArrowUnique CC); intro u; cbn; rewrite <- (Hf u); 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.