Library Coproduct


Require Import Utf8.
Require Import Setoid JMeq.
Require Export Category.
Require Import Common Notations CategoryIsomorphisms.

Set Implicit Arguments.

Generalizable All Variables.

Coproducts


Local Open Scope category_scope.
Local Open Scope morphism_scope.

Section category_coproduct.
  Context `(C : @Category objC).

  Variables X Y : C.

Define coproducts by the universal property
  Class is_coproduct (coproductXY : C) :=
    {
      coproduct_inl : Morphism C X coproductXY;
      coproduct_inr : Morphism C Y coproductXY;
      coproduct_map : A (f : X ~> A) (g : Y ~> A), coproductXY ~> A;
      coproduct_inl_commutes_prop := (fun A f g coproduct_map
                                      coproduct_map coproduct_inl = f);
      coproduct_inr_commutes_prop := (fun A f g coproduct_map
                                      coproduct_map coproduct_inr = g);
      coproduct_inl_commutes : A f g,
                               coproduct_inl_commutes_prop A f g (@coproduct_map A f g);
      coproduct_inr_commutes : A f g,
                               coproduct_inr_commutes_prop A f g (@coproduct_map A f g);
      coproduct_map_unique : A f g coproduct_map',
                             coproduct_inl_commutes_prop A f g coproduct_map'
                             → coproduct_inr_commutes_prop A f g coproduct_map'
                             → coproduct_map' = coproduct_map _ f g
    }.

  Class > coproduct :=
    {
      coproduct_element :> C;
      coproduct_is_coproduct :> is_coproduct coproduct_element

    }.

  Global Existing Instance coproduct_is_coproduct.
End category_coproduct.

Arguments coproduct_inl_commutes_prop _ _ _ _ _ _ _ _ _ _ / .
Arguments coproduct_inr_commutes_prop _ _ _ _ _ _ _ _ _ _ / .

Infix "⊔" := (@coproduct _ _) : object_scope.
Infix "⊔" := (@coproduct _ _) : object_type_scope.
Notation "'i₁'" := (@coproduct_inl _ _ _ _ _ _) : morphism_scope.
Notation "'i₁'" := (@coproduct_inl _ _ _ _ _ _) : object_scope.
Notation "'i₂'" := (@coproduct_inr _ _ _ _ _ _) : morphism_scope.
Notation "'i₂'" := (@coproduct_inr _ _ _ _ _ _) : object_scope.

Section swap_coproduct.
  Context `(C : @Category objC).
Define swap via the universal property; note that the object type doesn't change, but the projection maps are switched. This is because the objects are truely opaque.

  Definition swap_coproduct (X Y : C) : (X Y)%object → (Y X)%object :=
    fun xy
      @Build_coproduct objC C
                     Y X
                     (@coproduct_element _ C _ _ xy)
                     {|
                       
                       coproduct_inl := i₂;
                       coproduct_inr := i₁;
                       coproduct_map := (fun _ f g coproduct_map _ g f);
                       coproduct_inl_commutes := (fun _ f g coproduct_inr_commutes _ g f);
                       coproduct_inr_commutes := (fun _ f g coproduct_inl_commutes _ g f);
                       coproduct_map_unique := (fun _ _ _ _ Hfst Hsnd coproduct_map_unique Hsnd Hfst)
                     |}.
End swap_coproduct.