Lemma isColim_weq_subproof2 (g : graph) (D : diagram g C) (c : C) (cc : cocone D c) (H : ∏ d, isweq (Cocone_by_postcompose D c cc d)) (d : C) (cd : cocone D d) (u : vertex g) : coconeIn cc u · invmap (make_weq _ (H d)) cd = coconeIn cd u. Proof. rewrite (isColim_weq_subproof1 D c cc d (invmap (make_weq _ (H d)) _) u). set (p := homotweqinvweq (make_weq _ (H d)) cd); simpl in p. now rewrite p. Qed.
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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory.