Library UniMath.CategoryTheory.Limits.Graphs.Coproducts
****************************************************************
Coproducts from colimits
We show that coproducts can be constructed from colimits.
Contents
1. The graph
2. The construction
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Local Open Scope cat.
Section CoproductGraph.
Context (I : UU).
Definition type_graph : graph := I ,, λ _ _, empty.
Definition coproduct_diagram {C : category} (f : I → C) : diagram type_graph C.
Show proof.
Definition coproduct_diagram {C : category} (f : I → C) : diagram type_graph C.
Show proof.
Section CoproductsFromColims.
Context {C : category}
(HC : Colims_of_shape type_graph C).
Section CoproductsFromColim.
Context (f : I → C).
Let D : diagram type_graph C := coproduct_diagram f.
Let L : ColimCocone D := HC D.
Let x : C := colim L.
Let fs : ∏ (i : I), f i --> x := λ i, colimIn L i.
Proposition isCoproduct_from_colims_unique
{y : C}
(gs : ∏ (i : I), f i --> y)
: isaprop (∑ g, ∏ (i : I), fs i · g = gs i).
Show proof.
Definition isCoproduct_from_colims
: isCoproduct I C f x fs.
Show proof.
Theorem Coproducts_from_Colims
: Coproducts I C.
Show proof.
End CoproductsFromColims.
End CoproductGraph.
Context {C : category}
(HC : Colims_of_shape type_graph C).
Section CoproductsFromColim.
Context (f : I → C).
Let D : diagram type_graph C := coproduct_diagram f.
Let L : ColimCocone D := HC D.
Let x : C := colim L.
Let fs : ∏ (i : I), f i --> x := λ i, colimIn L i.
Proposition isCoproduct_from_colims_unique
{y : C}
(gs : ∏ (i : I), f i --> y)
: isaprop (∑ g, ∏ (i : I), fs i · g = gs i).
Show proof.
use invproofirrelevance.
intros φ₁ φ₂.
use subtypePath.
{
intro.
use impred ; intro.
apply homset_property.
}
use colimArrowUnique' ; cbn.
intro i.
exact (pr2 φ₁ i @ !(pr2 φ₂ i)).
intros φ₁ φ₂.
use subtypePath.
{
intro.
use impred ; intro.
apply homset_property.
}
use colimArrowUnique' ; cbn.
intro i.
exact (pr2 φ₁ i @ !(pr2 φ₂ i)).
Definition isCoproduct_from_colims
: isCoproduct I C f x fs.
Show proof.
intros y gs.
use iscontraprop1.
- apply isCoproduct_from_colims_unique.
- simple refine (_ ,, _).
+ use colimArrow.
use make_cocone.
* exact gs.
* intros u v F.
induction F.
+ intro i.
exact (colimArrowCommutes L _ _ i).
End CoproductsFromColim.use iscontraprop1.
- apply isCoproduct_from_colims_unique.
- simple refine (_ ,, _).
+ use colimArrow.
use make_cocone.
* exact gs.
* intros u v F.
induction F.
+ intro i.
exact (colimArrowCommutes L _ _ i).
Theorem Coproducts_from_Colims
: Coproducts I C.
Show proof.
End CoproductsFromColims.
End CoproductGraph.