Lemma isColim_weq_subproof2 {C : precategory} (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) : is_cocone_mor cc cd (invmap (make_weq _ (H d)) cd). Proof. intro u. 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.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.