Definition z_iso_from_colim_to_colim {C : precategory} {g : graph} {d : diagram g C} (CC CC' : ColimCocone d) : z_iso (colim CC) (colim CC'). Proof. use make_z_iso. - apply colimArrow, colimCocone. - apply colimArrow, colimCocone. - abstract (now split; apply pathsinv0, colim_endo_is_identity; intro u; rewrite assoc, colimArrowCommutes; eapply pathscomp0; try apply colimArrowCommutes). 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.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. 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.Adjunctions.Core.