# Definition of indexed coproducts of objects in a precategory

Section coproduct_def.

Variables (I : UU) (C : precategory).

Definition isCoproduct (a : I C) (co : C)
(ia : i, a i --> co) :=
(c : C) (f : i, a i --> c),
∃! (g : co --> c), i, ia i · g = f i.

Definition Coproduct (a : I C) :=
coia : ( co : C, i, a i --> co),
isCoproduct a (pr1 coia) (pr2 coia).

Definition Coproducts := (a : I C), Coproduct a.
Definition hasCoproducts := (a : I C), Coproduct a .

Definition CoproductObject {a : I C} (CC : Coproduct a) : C := pr1 (pr1 CC).
Definition CoproductIn {a : I C} (CC : Coproduct a): i, a i --> CoproductObject CC :=
pr2 (pr1 CC).

Definition isCoproduct_Coproduct {a : I C} (CC : Coproduct a) :
isCoproduct a (CoproductObject CC) (CoproductIn CC).
Proof.
exact (pr2 CC).
Defined.

Definition CoproductArrow {a : I C} (CC : Coproduct a) {c : C} (f : i, a i --> c) :
CoproductObject CC --> c.
Proof.
exact (pr1 (pr1 (isCoproduct_Coproduct CC _ f))).
Defined.

Lemma CoproductInCommutes (a : I C) (CC : Coproduct a) :
(c : C) (f : i, a i --> c) i, CoproductIn CC i · CoproductArrow CC f = f i.
Proof.
intros c f i.
exact (pr2 (pr1 (isCoproduct_Coproduct CC _ f)) i).
Qed.

Lemma CoproductIn_idtoiso {i1 i2 : I} (a : I C) (CC : Coproduct a)
(e : i1 = i2) :
idtoiso (maponpaths a e) · CoproductIn CC i2 = CoproductIn CC i1.
Proof.
induction e.
apply id_left.
Qed.

Lemma CoproductArrowUnique (a : I C) (CC : Coproduct a) (x : C)
(f : i, a i --> x) (k : CoproductObject CC --> x)
(Hk : i, CoproductIn CC i · k = f i) :
k = CoproductArrow CC f.
Proof.
set (H' := pr2 (isCoproduct_Coproduct CC _ f) (k,,Hk)).
apply (base_paths _ _ H').
Qed.

Lemma CoproductArrowEta (a : I C) (CC : Coproduct a) (x : C)
(f : CoproductObject CC --> x) :
f = CoproductArrow CC (λ i, CoproductIn CC i · f).
Proof.
now apply CoproductArrowUnique.
Qed.

Definition CoproductOfArrows {a : I C} (CCab : Coproduct a) {c : I C}
(CCcd : Coproduct c) (f : i, a i --> c i) :
CoproductObject CCab --> CoproductObject CCcd :=
CoproductArrow CCab (λ i, f i · CoproductIn CCcd i).

Lemma CoproductOfArrowsIn {a : I C} (CCab : Coproduct a) {c : I C}
(CCcd : Coproduct c) (f : i, a i --> c i) :
i, CoproductIn CCab i · CoproductOfArrows CCab CCcd f = f i · CoproductIn CCcd i.
Proof.
unfold CoproductOfArrows; intro i.
apply CoproductInCommutes.
Qed.

Definition make_Coproduct (a : I C) (c : C) (f : i, a i --> c) :
isCoproduct _ _ f Coproduct a.
Proof.
intro H.
use tpair.
- apply (tpair _ c f).
- apply H.
Defined.

Definition make_isCoproduct (hsC : has_homsets C) (a : I C) (co : C)
(f : i, a i --> co) : ( (c : C) (g : i, a i --> c),
∃! k : C co, c, i, f i · k = g i)
isCoproduct a co f.
Proof.
intros H c cc.
apply H.
Defined.

Lemma precompWithCoproductArrow {a : I C} (CCab : Coproduct a) {c : I C}
(CCcd : Coproduct c) (f : i, a i --> c i)
{x : C} (k : i, c i --> x) :
CoproductOfArrows CCab CCcd f · CoproductArrow CCcd k =
CoproductArrow CCab (λ i, f i · k i).
Proof.
apply CoproductArrowUnique; intro i.
now rewrite assoc, CoproductOfArrowsIn, <- assoc, CoproductInCommutes.
Qed.

Lemma postcompWithCoproductArrow {a : I C} (CCab : Coproduct a) {c : C}
(f : i, a i --> c) {x : C} (k : c --> x) :
CoproductArrow CCab f · k = CoproductArrow CCab (λ i, f i · k).
Proof.
apply CoproductArrowUnique; intro i.
now rewrite assoc, CoproductInCommutes.
Qed.

Lemma Coproduct_endo_is_identity (a : I C) (CC : Coproduct a)
(k : CoproductObject CC --> CoproductObject CC)
(H1 : i, CoproductIn CC i · k = CoproductIn CC i)
: identity _ = k.
Proof.
apply pathsinv0.
eapply pathscomp0; [apply CoproductArrowEta|].
apply pathsinv0, CoproductArrowUnique; intro i; apply pathsinv0.
now rewrite id_right, H1.
Defined.

End coproduct_def.

Section Coproducts.

Variables (I : UU) (C : precategory) (CC : Coproducts I C).

Definition CoproductOfArrows_comp (a b c : I C)
(f : i, a i --> b i) (g : i, b i --> c i) :
CoproductOfArrows _ _ _ _ f · CoproductOfArrows _ _ (CC _) (CC _) g
= CoproductOfArrows _ _ (CC _) (CC _)(λ i, f i · g i).
Proof.
apply CoproductArrowUnique; intro i.
rewrite assoc, CoproductOfArrowsIn.
now rewrite <- assoc, CoproductOfArrowsIn, assoc.
Qed.

Definition CoproductOfArrows_eq (a c : I C) (f f' : i, a i --> c i) : f = f'
CoproductOfArrows _ _ _ _ f = CoproductOfArrows _ _ (CC _) (CC _) f'.
Proof.
now induction 1.
Qed.

End Coproducts.

Section functors.

Definition coproduct_functor_data (I : UU) {C : precategory}
(PC : Coproducts I C) : functor_data (power_precategory I C) C.
Proof.
use tpair.
- intros p.
apply (CoproductObject _ _ (PC p)).
- simpl; intros p q f.
apply (CoproductOfArrows _ _ _ _ f).
Defined.

# The coproduct functor: C^I -> C

Definition coproduct_functor (I : UU) {C : precategory}
(PC : Coproducts I C) : functor (power_precategory I C) C.
Proof.
apply (tpair _ (coproduct_functor_data _ PC)).
split.
- intro x; simpl; apply pathsinv0, Coproduct_endo_is_identity.
now intro i; rewrite CoproductOfArrowsIn, id_left.
- now intros x y z f g; simpl; rewrite CoproductOfArrows_comp .
Defined.

End functors.

Definition coproduct_of_functors_alt_old (I : UU) {C D : precategory}
(HD : Coproducts I D) (F : I functor C D) : functor C D :=
functor_composite (delta_functor I C)
(functor_composite (family_functor _ F)
(coproduct_functor _ HD)).

The copropuct of a family of functors

# Coproducts lift to functor categories

Section def_functor_pointwise_coprod.

Variables (I : UU) (C D : precategory).
Variable HD : Coproducts I D.
Variable hsD : has_homsets D.

Section coproduct_of_functors.

Variables (F : I functor C D).

Definition coproduct_of_functors_ob (c : C) : D
:= CoproductObject _ _ (HD (λ i, F i c)).

Definition coproduct_of_functors_mor (c c' : C) (f : c --> c')
: coproduct_of_functors_ob c --> coproduct_of_functors_ob c' :=
CoproductOfArrows _ _ _ _ (λ i, # (F i) f).

Definition coproduct_of_functors_data : functor_data C D.
Proof.
coproduct_of_functors_ob.
exact coproduct_of_functors_mor.
Defined.

Lemma is_functor_coproduct_of_functors_data :
is_functor coproduct_of_functors_data.
Proof.
split; simpl; intros.
- unfold functor_idax; intros; simpl in ×.
apply pathsinv0.
apply Coproduct_endo_is_identity; intro i.
unfold coproduct_of_functors_mor.
eapply pathscomp0; [apply (CoproductOfArrowsIn _ _ (HD (λ i, (F i) a)))|].
now simpl; rewrite functor_id, id_left.
- unfold functor_compax; simpl; unfold coproduct_of_functors_mor.
intros; simpl in ×.
apply pathsinv0.
eapply pathscomp0.
apply CoproductOfArrows_comp.
apply maponpaths, funextsec; intro i.
now rewrite functor_comp.
Qed.

Definition coproduct_of_functors : functor C D :=
tpair _ _ is_functor_coproduct_of_functors_data.

Lemma coproduct_of_functors_alt_old_eq_coproduct_of_functors :
coproduct_of_functors_alt_old _ HD F = coproduct_of_functors.
Proof.
now apply (functor_eq _ _ hsD).
Defined.

Lemma coproduct_of_functors_alt_eq_coproduct_of_functors :
coproduct_of_functors_alt _ HD F = coproduct_of_functors.
Proof.
now apply (functor_eq _ _ hsD).
Defined.

Definition coproduct_nat_trans_in_data i (c : C) :
D (F i) c, coproduct_of_functors c :=
CoproductIn _ _ (HD (λ j, (F j) c)) i.

Lemma is_nat_trans_coproduct_nat_trans_in_data i :
is_nat_trans _ _ (coproduct_nat_trans_in_data i).
Proof.
intros c c' f; apply pathsinv0.
now eapply pathscomp0;[apply (CoproductOfArrowsIn I _ (HD (λ i, (F i) c)))|].
Qed.

Definition coproduct_nat_trans_in i : nat_trans (F i) coproduct_of_functors :=
tpair _ _ (is_nat_trans_coproduct_nat_trans_in_data i).

Section vertex.

Variable A : functor C D.
Variable f : i, nat_trans (F i) A.

Definition coproduct_nat_trans_data c :
coproduct_of_functors c --> A c :=
CoproductArrow _ _ _ (λ i, f i c).

Lemma is_nat_trans_coproduct_nat_trans_data :
is_nat_trans _ _ coproduct_nat_trans_data.
Proof.
intros a b k; simpl.
eapply pathscomp0.
apply (precompWithCoproductArrow I D (HD (λ i : I, (F i) a)) (HD (λ i : I, (F i) b))).
apply pathsinv0.
eapply pathscomp0; [apply postcompWithCoproductArrow|].
apply maponpaths, funextsec; intro i.
now rewrite (nat_trans_ax (f i)).
Qed.

Definition coproduct_nat_trans : nat_trans coproduct_of_functors A
:= tpair _ _ is_nat_trans_coproduct_nat_trans_data.

End vertex.

Definition functor_precat_coproduct_cocone
: Coproduct I [C, D, hsD] F.
Proof.
use make_Coproduct.
- apply coproduct_of_functors.
- apply coproduct_nat_trans_in.
- use make_isCoproduct.
+ apply functor_category_has_homsets.
+ intros A f.
use tpair.
× apply (tpair _ (coproduct_nat_trans A f)).
abstract (intro i; apply (nat_trans_eq hsD); intro c;
apply (CoproductInCommutes I D _ (HD (λ j, (F j) c)))).
× abstract (
intro t; apply subtypePath; simpl;
[intro; apply impred; intro; apply (isaset_nat_trans hsD)|];
apply (nat_trans_eq hsD); intro c;
apply CoproductArrowUnique; intro i;
apply (nat_trans_eq_pointwise (pr2 t i))).
Defined.

End coproduct_of_functors.

Definition Coproducts_functor_precat : Coproducts I [C, D, hsD].
Proof.
intros F.
apply functor_precat_coproduct_cocone.
Defined.

End def_functor_pointwise_coprod.

# Coproducts from colimits

Section coproducts_from_colimits.

Variables (I : UU) (C : precategory) (hsC : has_homsets C).

Definition I_graph : graph := (I,,λ _ _,empty).

Definition coproducts_diagram (F : I C) : diagram I_graph C.
Proof.
F.
abstract (intros u v e; induction e).
Defined.

Definition Coproducts_cocone c (F : I C) (H : i, F i --> c) :
cocone (coproducts_diagram F) c.
Proof.
use tpair.
+ intro v; apply H.
+ abstract (intros u v e; induction e).
Defined.

Lemma Coproducts_from_Colims : Colims_of_shape I_graph C Coproducts I C.
Proof.
intros H F.
set (HF := H (coproducts_diagram F)).
use make_Coproduct.
+ apply (colim HF).
+ intros i; apply (colimIn HF).
+ apply (make_isCoproduct _ _ hsC); intros c Fic.
use unique_exists.
- now apply colimArrow, Coproducts_cocone.
- abstract (simpl; intro i; apply (colimArrowCommutes HF)).
- abstract (intros y; apply impred; intro i; apply hsC).
- abstract (intros f Hf; apply colimArrowUnique; simpl in *; intros i; apply Hf).
Defined.

End coproducts_from_colimits.