proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Adjunctions.Core