Definition project_colimcocone11 (CC : Colims C) {g : graph} {d : diagram g (arrow C)} {f : arrow C} {ccf : cocone d f} (isclCC : isColimCocone d f ccf) : isColimCocone _ _ (project_cocone11 ccf). Proof. set (dbase := project_diagram11 d). set (base_mor := isColim_is_z_iso _ (arrow_colims CC _ d) _ _ isclCC). use (is_z_iso_isColim _ (CC _ dbase)). exists (arrow_mor11 (pr1 base_mor)). abstract ( split; [ etrans; [|exact (arrow_mor11_eq (pr12 base_mor))]; apply cancel_postcomposition | etrans; [|exact (arrow_mor11_eq (pr22 base_mor))]; apply cancel_precomposition ]; ( use colimArrowUnique'; intro v; etrans; [apply colimArrowCommutes|]; apply pathsinv0; etrans; [apply colimArrowCommutes|]; reflexivity ) ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.