Lemma ColimFunctor_unique (F : [A, C]) (cc : cocone D F) : iscontr (∑ x : [A, C] ⟦ ColimFunctor, F ⟧, ∏ v : vertex g, colim_nat_trans_in_data v · x = coconeIn cc v). Proof. use tpair. - use tpair. + apply (tpair _ (λ a, colimArrow (HCg a) _ (cocone_pointwise F cc a))). abstract (intros a a' f; simpl; eapply pathscomp0; [ now apply precompWithColimOfArrows | apply pathsinv0; eapply pathscomp0; [ now apply postcompWithColimArrow | apply colimArrowUnique; intro u; eapply pathscomp0; [ now apply colimArrowCommutes | apply pathsinv0; now use nat_trans_ax ]]]). + abstract (intro u; apply (nat_trans_eq C); simpl; intro a; now apply (colimArrowCommutes (HCg a))). - abstract (intro t; destruct t as [t1 t2]; apply subtypePath; simpl; [ intro; apply impred; intro u; apply functor_category_has_homsets | apply (nat_trans_eq C); simpl; intro a; apply colimArrowUnique; intro u; now apply (nat_trans_eq_pointwise (t2 u))]). 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.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.