Lemma colimArrowEta {C : precategory} {g : graph} {d : diagram g C} (CC : ColimCocone d) (c : C) (f : C⟦colim CC,c⟧) : f = colimArrow CC c (tpair _ (λ u, colimIn CC u · f) (Cocone_postcompose (colimCocone CC) c f)). Proof. now apply colimArrowUnique. 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.