Lemma isColim_weq_subproof1 {g : graph} (D : diagram g C) (c : C) (cc : cocone D c) (d : C) (k : C⟦c,d⟧) : ∏ u, coconeIn cc u · k = pr1 (Cocone_by_postcompose D c cc d k) u. Proof. now intro u. 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.