Definition arrow_colims (CC : Colims C) : Colims (arrow C). Proof. intros g d. set (dbase := mapdiagram (pr1_category _) d). set (clbase := arrow_base_colims CC _ dbase). use tpair. - exists (arrow_colimit CC d). use tpair. * intro v. exists (colimIn clbase v). abstract ( use (colimOfArrowsIn _ _ (CC g (mapdiagram (pr1_functor C C) dbase))) ). * abstract ( intros u v e; apply subtypePath; [intro; apply homset_property|]; apply (colimInCommutes clbase) ). - intros c cc. transparent assert (ccbase : (cocone dbase (pr1 c))). { exists (λ v, pr1 (coconeIn cc v)). abstract ( intros u v e; exact (base_paths _ _ (coconeInCommutes cc _ _ e)) ). } use unique_exists. * exists (colimArrow clbase _ ccbase). abstract ( etrans; [use postcompWithColimArrow|]; apply pathsinv0; etrans; [use precompWithColimOfArrows|]; apply maponpaths; (apply subtypePath; [intro; do 3 (apply impred; intro); apply homset_property|]); apply funextsec; intro v; exact (pathsinv0 (arrow_mor_comm (coconeIn cc v))) ). * abstract ( intro; apply subtypePath; [intro; apply homset_property|]; exact (colimArrowCommutes clbase _ ccbase v) ). * abstract ( intro; apply impred; intro; apply homset_property ). * abstract ( intros y H; apply subtypePath; [intro; apply homset_property|]; apply colimArrowUnique; intro v; exact (base_paths _ _ (H v)) ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.