proposition: Lemma pointwise_Colim_is_isColimFunctor {A C : category} {g : graph} (d : diagram g [A,C]) (G : [A,C]) (ccG : cocone d G) (H : ∏ a, isColimCocone _ _ (cocone_pointwise d G ccG a)) : isColimCocone d G ccG.
proof: Proof. set (CC a := make_ColimCocone _ _ _ (H a)). set (D' := ColimFunctorCocone _ CC). use is_z_iso_isColim. - apply D'. - use tpair. + use make_nat_trans. * intros a; apply identity. * abstract (intros a b f; rewrite id_left, id_right; simpl; apply (colimArrowUnique (CC a)); intro u; cbn; now rewrite <- (nat_trans_ax (coconeIn ccG u))). + abstract (split; [ apply (nat_trans_eq C); intros x; simpl; rewrite id_right; apply pathsinv0, colimArrowUnique; intros v; now rewrite id_right | apply (nat_trans_eq C); intros x; simpl; rewrite id_left; apply pathsinv0, (colimArrowUnique (CC x)); intro u; now rewrite id_right]). 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