Definition arrow_base_colims (CC : Colims C) : Colims (arrow_base C). Proof. intros g d. set (d1 := mapdiagram (pr1_functor _ _) d). set (d2 := mapdiagram (pr2_functor _ _) d). set (cc1 := CC _ d1). set (cc2 := CC _ d2). use tpair. - exists (make_dirprod (colim cc1) (colim cc2)). use tpair. * intro v. split. + exact (colimIn cc1 v). + exact (colimIn cc2 v). * abstract ( intros u v e; use pathsdirprod; [ exact (colimInCommutes cc1 _ _ e)| exact (colimInCommutes cc2 _ _ e) ] ). - intros c cc. destruct cc as [f ccf]. use unique_exists. * split. + use colimArrow. exists (λ v, pr1 (f v)). abstract ( intros u v e; exact (pr1 (pathsdirprodweq (ccf _ _ e))) ). + use colimArrow. exists (λ v, pr2 (f v)). abstract ( intros u v e; exact (pr2 (pathsdirprodweq (ccf _ _ e))) ). * abstract ( intro; apply pathsdirprod; [ apply (colimArrowCommutes cc1)|apply (colimArrowCommutes cc2) ] ). * abstract ( intro; apply impred; intro; apply homset_property ). * abstract ( intros y H; apply pathsdirprod; apply colimArrowUnique; intro v; [ exact (pr1 (pathsdirprodweq (H v)))|exact (pr2 (pathsdirprodweq (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.