Library UniMath.CategoryTheory.Limits.Coproducts

Definition of indexed coproducts of objects in a precategory

Section coproduct_def.

Context (I : UU) (C : category).

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).
Coercion CoproductObject : Coproduct >-> ob.

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).
Show proof.
  exact (pr2 CC).

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

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

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.
Show proof.
  induction e.
  apply id_left.

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.
Show proof.
  set (H' := pr2 (isCoproduct_Coproduct CC _ f) (k,,Hk)).
  apply (base_paths _ _ H').

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

Proposition CoproductArrow_eq
            {d : I C}
            (z : C)
            (x : Coproduct d)
            (f g : x --> z)
            (p : (i : I), CoproductIn x i · f = CoproductIn x i · g)
  : f = g.
Show proof.
  refine (CoproductArrowEta _ _ _ _ @ _ @ !(CoproductArrowEta _ _ _ _)).
  apply maponpaths.
  use funextsec.
  exact p.

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.
Show proof.
  unfold CoproductOfArrows; intro i.
  apply CoproductInCommutes.

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

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.
Show proof.
  intros H c cc.
  apply H.

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).
Show proof.

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).
Show proof.
apply CoproductArrowUnique; intro i.
now rewrite assoc, CoproductInCommutes.

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.
Show proof.
apply pathsinv0.
eapply pathscomp0; [apply CoproductArrowEta|].
apply pathsinv0, CoproductArrowUnique; intro i; apply pathsinv0.
now rewrite id_right, H1.

End coproduct_def.

Section Coproducts.

Context (I : UU) (C : category) (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).
Show proof.
apply CoproductArrowUnique; intro i.
rewrite assoc, CoproductOfArrowsIn.
now rewrite <- assoc, CoproductOfArrowsIn, assoc.

End Coproducts.

Section functors.

Definition coproduct_functor_data (I : UU) {C : category}
  (PC : Coproducts I C) : functor_data (power_category I C) C.
Show proof.
use tpair.
- intros p.
  apply (CoproductObject _ _ (PC p)).
- simpl; intros p q f.
  apply (CoproductOfArrows _ _ _ _ f).

The coproduct functor: C^I -> C

Definition coproduct_functor (I : UU) {C : category}
  (PC : Coproducts I C) : functor (power_category I C) C.
Show proof.
apply (tpair _ (coproduct_functor_data _ PC)).
abstract (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]).

End functors.

Definition coproduct_of_functors_alt_old (I : UU) {C D : category}
  (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 coproduct of a family of functors

Coproducts lift to functor categories

Section def_functor_pointwise_coprod.

Context (I : UU) (C D : category) (HD : Coproducts I D).

Section coproduct_of_functors.

Context (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.
Show proof.

Lemma is_functor_coproduct_of_functors_data :
  is_functor coproduct_of_functors_data.
Show 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.

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.
Show proof.
now apply (functor_eq _ _ D).

Lemma coproduct_of_functors_alt_eq_coproduct_of_functors :
  coproduct_of_functors_alt _ HD F = coproduct_of_functors.
Show proof.
now apply (functor_eq _ _ D).

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).
Show proof.
intros c c' f; apply pathsinv0.
now eapply pathscomp0;[apply (CoproductOfArrowsIn I _ (HD (λ i, (F i) c)))|].

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.

Context (A : functor C D) (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.
Show 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)).

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] F.
Show 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 D); 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 D)|];
        apply (nat_trans_eq D); intro c;
        apply CoproductArrowUnique; intro i;
        apply (nat_trans_eq_pointwise (pr2 t i))).

End coproduct_of_functors.

Definition Coproducts_functor_precat : Coproducts I [C, D].
Show proof.
  intros F.
  apply functor_precat_coproduct_cocone.

End def_functor_pointwise_coprod.

Coproducts from colimits

Section coproducts_from_colimits.

Context (I : UU) (C : category).

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

Definition coproducts_diagram (F : I C) : diagram I_graph C.
Show proof.
exists F.
abstract (intros u v e; induction e).

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

Lemma Coproducts_from_Colims : Colims_of_shape I_graph C -> Coproducts I C.
Show proof.
intros H F.
set (HF := H (coproducts_diagram F)).
use make_Coproduct.
+ apply (colim HF).
+ intros i; apply (colimIn HF).
+ apply (make_isCoproduct _ _ C); 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 C).
  - abstract (intros f Hf; apply colimArrowUnique; simpl in *; intros i; apply Hf).

End coproducts_from_colimits.

Section DistributionThroughFunctor.

  Context {I : UU} {C D : category}
    (CPC : Coproducts I C) (CPD : Coproducts I D) (F : functor C D).

  Definition coprod_antidistributor (cs : power_category I C):
    CPD (fun i => F (cs i)) --> F (CPC cs).
  Show proof.
    use CoproductArrow; intro i; apply (#F). apply CoproductIn.

  Lemma coprod_antidistributor_nat (cs1 cs2 : power_category I C) (g : power_category I C cs1, cs2 ) :
    coprod_antidistributor cs1 · #F (#(coproduct_functor I CPC) g) =
    #(coproduct_functor I CPD) (#(family_functor I (fun _ => F)) g) · coprod_antidistributor cs2.
  Show proof.
    etrans.
    { apply postcompWithCoproductArrow. }
    etrans.
    2: { apply pathsinv0, precompWithCoproductArrow. }
    apply maponpaths.
    apply funextsec; intro i.
    etrans.
    { apply pathsinv0, functor_comp. }
    etrans.
    2: { cbn. apply functor_comp. }
    apply maponpaths.
    apply CoproductInCommutes.

axiomatize extra requirements

  Definition coprod_distributor_data : UU := (cs : power_category I C),
     F (CPC cs) --> CPD (fun i => F (cs i)).

  Identity Coercion coprod_distributor_data_funclass: coprod_distributor_data >-> Funclass.

  Definition coprod_distributor_iso_law (δ : coprod_distributor_data) : UU :=
     (cs : power_category I C), is_inverse_in_precat (δ cs) (coprod_antidistributor cs).

  Definition coprod_distributor : UU := δ : coprod_distributor_data, coprod_distributor_iso_law δ.

  Definition coprod_distributor_to_data (δ : coprod_distributor) : coprod_distributor_data := pr1 δ.
  Coercion coprod_distributor_to_data : coprod_distributor >-> coprod_distributor_data.

End DistributionThroughFunctor.

Section DistributionForPrecompositionFunctor.

  Context {I : UU} {A B C : category} (CPC : Coproducts I C) (H : functor A B).

  Let CPAC : Coproducts I [A,C] := Coproducts_functor_precat I A C CPC.
  Let CPBC : Coproducts I [B,C] := Coproducts_functor_precat I B C CPC.
  Let precomp : functor [B,C] [A,C] := pre_composition_functor A B C H.

  Definition precomp_coprod_distributor_data : coprod_distributor_data CPBC CPAC precomp.
  Show proof.
    intro Gs.
    apply nat_trans_id.

  Lemma precomp_coprod_distributor_law :
    coprod_distributor_iso_law _ _ _ precomp_coprod_distributor_data.
  Show proof.
    intros Gs.
    split.
    - apply (nat_trans_eq C).
      intro c.
      cbn.
      rewrite id_left.
      apply pathsinv0, Coproduct_endo_is_identity.
      intro i.
      unfold coproduct_nat_trans_data.
      cbn in Gs.
      apply (CoproductInCommutes I C (λ i0 : I, Gs i0 (H c)) (CPC _) _
               (λ i0 : I, coproduct_nat_trans_in_data I B C CPC Gs i0 (H c)) i).
    - etrans.
      { apply postcompWithCoproductArrow. }
      etrans.
      2: { apply pathsinv0, CoproductArrowEta. }
      apply maponpaths; apply funextsec; intro i;
        (rewrite id_right; apply (nat_trans_eq C); intro c; apply id_right).

  Definition precomp_coprod_distributor : coprod_distributor CPBC CPAC precomp :=
    _,,precomp_coprod_distributor_law.

End DistributionForPrecompositionFunctor.

Coproducts are unique
Definition eq_Coproduct
           {C : category}
           {J : UU}
           {D : J C}
           (coprod₁ coprod₂ : Coproduct J C D)
           (q : CoproductObject _ _ coprod₁ = CoproductObject _ _ coprod₂)
           (e : (j : J),
                CoproductIn _ _ coprod₁ j
                =
                CoproductIn _ _ coprod₂ j · idtoiso (!q))
  : coprod₁ = coprod₂.
Show proof.
  use subtypePath.
  {
    intro.
    repeat (use impred ; intro).
    use isapropiscontr.
  }
  use total2_paths_f.
  - exact q.
  - rewrite transportf_sec_constant.
    use funextsec.
    intro j.
    rewrite <- !idtoiso_postcompose.
    pose (p := e j).
    rewrite !idtoiso_inv in p.
    refine (maponpaths (λ z, z · _) p @ _).
    rewrite !assoc'.
    refine (_ @ id_right _).
    apply maponpaths.
    apply z_iso_after_z_iso_inv.

Definition z_iso_between_Coproduct
           {C : category}
           {J : UU}
           {D : J C}
           (coprod₁ coprod₂ : Coproduct J C D)
  : z_iso coprod₁ coprod₂.
Show proof.
  use make_z_iso.
  - exact (CoproductArrow _ _ coprod₁ (CoproductIn _ _ coprod₂)).
  - exact (CoproductArrow _ _ coprod₂ (CoproductIn _ _ coprod₁)).
  - split.
    + abstract
        (use CoproductArrow_eq ;
         intro j ;
         rewrite !assoc ;
         rewrite !CoproductInCommutes ;
         rewrite id_right ;
         apply idpath).
    + abstract
        (use CoproductArrow_eq ;
         intro j ;
         rewrite !assoc ;
         rewrite !CoproductInCommutes ;
         rewrite id_right ;
         apply idpath).

Definition isaprop_Coproduct
           {C : category}
           (HC : is_univalent C)
           (J : UU)
           (D : J C)
  : isaprop (Coproduct J C D).
Show proof.
  use invproofirrelevance.
  intros p₁ p₂.
  use eq_Coproduct.
  - refine (isotoid _ HC _).
    apply z_iso_between_Coproduct.
  - intro j.
    rewrite idtoiso_inv.
    rewrite idtoiso_isotoid ; cbn.
    rewrite CoproductInCommutes.
    apply idpath.

Section Coproduct_different_indexers.

Definition CoproductOfArrowsInclusion {I J : UU} {C : category}
    (incl : I -> J) {a : I -> C} (CCab : Coproduct _ _ a) {c : J -> C}
    (CCcd : Coproduct _ _ c) (f : i, a i --> c (incl i)) :
          CoproductObject _ _ CCab --> CoproductObject _ _ CCcd :=
  CoproductArrow _ _ CCab (λ i, f i · CoproductIn _ _ CCcd (incl i)).


Definition CoproductOfArrows' (I : UU) (C : category)
    {a : I -> C} (CCab : Coproduct _ _ a) {c : I -> C}
    (CCcd : Coproduct _ _ c) (f : i, a i --> c i) :
        CoproductObject _ _ CCab --> CoproductObject _ _ CCcd :=
  CoproductOfArrowsInclusion (idfun I) CCab CCcd f.

Lemma CoproductOfArrowsInclusionIn {I J : UU} {C : category}
    (incl : I -> J) {a : I -> C} (CCab : Coproduct _ _ a) {c : J -> C}
    (CCcd : Coproduct _ _ c) (f : i, a i --> c (incl i)) :
   i, CoproductIn _ _ CCab i · CoproductOfArrowsInclusion incl CCab CCcd f = f i · CoproductIn _ _ CCcd (incl i).
Show proof.
  unfold CoproductOfArrows; intro i.
  apply CoproductInCommutes.

Lemma CoproductOfArrows'In (I : UU) (C : category)
    {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.
Show proof.

Lemma precompWithCoproductArrowInclusion {I J : UU} {C : category}
  (incl : I -> J) {a : I -> C} (CCab : Coproduct _ _ a) {c : J -> C}
  (CCcd : Coproduct _ _ c) (f : i, a i --> c (incl i))
  {x : C} (k : i, c i --> x) :
      CoproductOfArrowsInclusion incl CCab CCcd f · CoproductArrow _ _ CCcd k =
       CoproductArrow _ _ CCab (λ i, f i · k (incl i)).
Show proof.

Lemma precompWithCoproductArrow' (I : UU) (C : category)
  {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).
Show proof.

Definition CoproductOfArrowsInclusion_comp {I J K: UU} {C : category}
    {a : I -> C} {b : J -> C} {c : K -> C}
    (CCI : Coproducts I C) (CCJ : Coproducts J C) (CCK : Coproducts K C)
    {inclI : I -> J} {inclJ : J -> K}
    (f : i, a i --> b (inclI i)) (g : j, b j --> c (inclJ j)) :
    CoproductOfArrowsInclusion inclI (CCI _) (CCJ _) f ·
        CoproductOfArrowsInclusion inclJ (CCJ _) (CCK _) g
    = CoproductOfArrowsInclusion (λ i, inclJ (inclI i)) (CCI _) (CCK _) (λ i, f i · g (inclI i)).
Show proof.
  apply CoproductArrowUnique; intro i.
  rewrite assoc, CoproductOfArrowsInclusionIn.
  now rewrite <- assoc, CoproductOfArrowsInclusionIn, assoc.

Definition CoproductOfArrows'_comp (I : UU) (C : category) (CC : Coproducts I C)
  (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).
Show proof.

End Coproduct_different_indexers.