Lemma is_z_iso_isLim {C : category} {g : graph} (D : diagram g C) (CC : LimCone D) (d : C) (cd : cone D d) : is_z_isomorphism (limArrow CC d cd) -> isLimCone D d cd. Proof. intro H. set (iinv := z_iso_inv_from_is_z_iso _ H). intros x cx. use tpair. - use tpair. + exact (limArrow CC x cx·iinv). + simpl; intro u. assert (XR:=limArrowCommutes CC x cx u). eapply pathscomp0; [| apply XR]. eapply pathscomp0; [ apply (!assoc _ _ _ ) |]. apply maponpaths. apply z_iso_inv_on_right. apply pathsinv0, limArrowCommutes. - intros p; destruct p as [f Hf]. apply subtypePath. + intro a; apply impred; intro u; apply C. + simpl; apply z_iso_inv_on_left; simpl. apply pathsinv0, limArrowUnique; intro u. cbn in *. eapply pathscomp0; [| apply Hf]. eapply pathscomp0. apply (!assoc _ _ _ ). apply maponpaths. apply limArrowCommutes. 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.