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. 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.
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.