Lemma isLim_is_z_iso {C : precategory} {g : graph} (D : diagram g C) (CC : LimCone D) (d : C) (cd : cone D d) : isLimCone D d cd -> is_z_isomorphism (limArrow CC d cd). Proof. intro H. set (CD := make_LimCone D d cd H). apply (tpair _ (limArrow (make_LimCone D d cd H) (lim CC) (limCone CC))). split. apply pathsinv0. change d with (lim CD). apply lim_endo_is_identity. simpl; intro u; rewrite <- assoc. eapply pathscomp0; [eapply maponpaths; apply limArrowCommutes|]. apply (limArrowCommutes CC). apply pathsinv0, (lim_endo_is_identity _ CC); simpl; intro u; rewrite <- assoc. eapply pathscomp0; [eapply maponpaths; apply (limArrowCommutes CC)|]. apply (limArrowCommutes CD). 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Import UniMath.CategoryTheory.opp_precat.