module Cat.Diagram.Coproduct where

CoproductsπŸ”—

The coproduct of two objects and (if it exists), is the smallest object equipped with β€œinjection” maps It is dual to the product.

We witness this notion of β€œsmallest object” with a universal property; Given any other that also admits injection maps from and we must have a unique map that factors the injections into This is best explained by a commutative diagram:

  record is-coproduct {A B P} (ι₁ : Hom A P) (ΞΉβ‚‚ : Hom B P) : Type (o βŠ” β„“) where
    field
      [_,_] : βˆ€ {Q} (inj0 : Hom A Q) (inj1 : Hom B Q) β†’ Hom P Q
      []βˆ˜ΞΉβ‚ : βˆ€ {Q} {inj0 : Hom A Q} {inj1} β†’ [ inj0 , inj1 ] ∘ ι₁ ≑ inj0
      []βˆ˜ΞΉβ‚‚ : βˆ€ {Q} {inj0 : Hom A Q} {inj1} β†’ [ inj0 , inj1 ] ∘ ΞΉβ‚‚ ≑ inj1

      unique : βˆ€ {Q} {inj0 : Hom A Q} {inj1}
             β†’ {other : Hom P Q}
             β†’ other ∘ ι₁ ≑ inj0
             β†’ other ∘ ΞΉβ‚‚ ≑ inj1
             β†’ other ≑ [ inj0 , inj1 ]

    uniqueβ‚‚ : βˆ€ {Q} {inj0 : Hom A Q} {inj1}
            β†’ βˆ€ {o1} (p1 : o1 ∘ ι₁ ≑ inj0) (q1 : o1 ∘ ΞΉβ‚‚ ≑ inj1)
            β†’ βˆ€ {o2} (p2 : o2 ∘ ι₁ ≑ inj0) (q2 : o2 ∘ ΞΉβ‚‚ ≑ inj1)
            β†’ o1 ≑ o2
    uniqueβ‚‚ p1 q1 p2 q2 = unique p1 q1 βˆ™ sym (unique p2 q2)

A coproduct of and is an explicit choice of coproduct diagram:

  record Coproduct (A B : Ob) : Type (o βŠ” β„“) where
    field
      coapex : Ob
      ι₁ : Hom A coapex
      ΞΉβ‚‚ : Hom B coapex
      has-is-coproduct : is-coproduct ι₁ ΞΉβ‚‚

    open is-coproduct has-is-coproduct public

UniquenessπŸ”—

The uniqueness argument presented here is dual to the argument for the product.

    +-Unique : βˆ€ {A B} (c1 c2 : Coproduct A B) β†’ coapex c1 β‰… coapex c2
    +-Unique c1 c2 = make-iso c1β†’c2 c2β†’c1 c1β†’c2β†’c1 c2β†’c1β†’c2
      where
        module c1 = Coproduct c1
        module c2 = Coproduct c2

        c1β†’c2 : Hom (coapex c1) (coapex c2)
        c1β†’c2 = c1.[ c2.ι₁ , c2.ΞΉβ‚‚ ]

        c2β†’c1 : Hom (coapex c2) (coapex c1)
        c2β†’c1 = c2.[ c1.ι₁ , c1.ΞΉβ‚‚ ]
        c1β†’c2β†’c1 : c1β†’c2 ∘ c2β†’c1 ≑ id
        c1β†’c2β†’c1 =
          c2.uniqueβ‚‚
            (pullr c2.[]βˆ˜ΞΉβ‚ βˆ™ c1.[]βˆ˜ΞΉβ‚)
            (pullr c2.[]βˆ˜ΞΉβ‚‚ βˆ™ c1.[]βˆ˜ΞΉβ‚‚)
            (idl _) (idl _)

        c2β†’c1β†’c2 : c2β†’c1 ∘ c1β†’c2 ≑ id
        c2β†’c1β†’c2 =
          c1.uniqueβ‚‚
            (pullr c1.[]βˆ˜ΞΉβ‚ βˆ™ c2.[]βˆ˜ΞΉβ‚)
            (pullr c1.[]βˆ˜ΞΉβ‚‚ βˆ™ c2.[]βˆ˜ΞΉβ‚‚)
            (idl _) (idl _)

Categories with all binary coproductsπŸ”—

Categories with all binary coproducts are quite common, so we provide an API for working with them. In order to get better printing in goals, we define an unnested record where all operations are top-level fields; this means that goals willl print as [ f , g ] instead of is-coproduct.[_,_] (coproduct A B) f g.

record Binary-coproducts {o β„“} (C : Precategory o β„“) : Type (o βŠ” β„“) where
  no-eta-equality
  open Cat.Reasoning C
  field
    _βŠ•β‚€_ : Ob β†’ Ob β†’ Ob
    ι₁ : βˆ€ {A B} β†’ Hom A (A βŠ•β‚€ B)
    ΞΉβ‚‚ : βˆ€ {A B} β†’ Hom B (A βŠ•β‚€ B)
    [_,_] : βˆ€ {A B X} (inj0 : Hom A X) (inj1 : Hom B X) β†’ Hom (A βŠ•β‚€ B) X
    []βˆ˜ΞΉβ‚ : βˆ€ {A B X} {inj0 : Hom A X} {inj1 : Hom B X} β†’ [ inj0 , inj1 ] ∘ ι₁ ≑ inj0
    []βˆ˜ΞΉβ‚‚ : βˆ€ {A B X} {inj0 : Hom A X} {inj1 : Hom B X} β†’ [ inj0 , inj1 ] ∘ ΞΉβ‚‚ ≑ inj1
    []-unique
      : βˆ€ {A B X} {inj0 : Hom A X} {inj1 : Hom B X}
      β†’ {other : Hom (A βŠ•β‚€ B) X}
      β†’ other ∘ ι₁ ≑ inj0
      β†’ other ∘ ΞΉβ‚‚ ≑ inj1
      β†’ other ≑ [ inj0 , inj1 ]

  infixr 7 _βŠ•β‚€_
  infix 50 _βŠ•β‚_

If a category has all binary coproducts, we can define a bifunctor that sets to their coproduct.

  _βŠ•β‚_ : βˆ€ {a b x y} β†’ Hom a x β†’ Hom b y β†’ Hom (a βŠ•β‚€ b) (x βŠ•β‚€ y)
  f βŠ•β‚ g = [ ι₁ ∘ f , ΞΉβ‚‚ ∘ g ]

  βŠ•-functor : Functor (C Γ—αΆœ C) C
  βŠ•-functor .Fβ‚€ (a , b) = a βŠ•β‚€ b
  βŠ•-functor .F₁ (f , g) = f βŠ•β‚ g
  βŠ•-functor .F-id = sym $ []-unique id-comm-sym id-comm-sym
  βŠ•-functor .F-∘ (f , g) (h , i) =
    sym $ []-unique
      (pullr []βˆ˜ΞΉβ‚ βˆ™ extendl []βˆ˜ΞΉβ‚)
      (pullr []βˆ˜ΞΉβ‚‚ βˆ™ extendl []βˆ˜ΞΉβ‚‚)

We also define a handful of common morphisms.

  βˆ‡ : βˆ€ {a} β†’ Hom (a βŠ•β‚€ a) a
  βˆ‡ = [ id , id ]

  coswap : βˆ€ {a b} β†’ Hom (a βŠ•β‚€ b) (b βŠ•β‚€ a)
  coswap = [ ΞΉβ‚‚ , ι₁ ]

  βŠ•-assoc : βˆ€ {a b c} β†’ Hom (a βŠ•β‚€ (b βŠ•β‚€ c)) ((a βŠ•β‚€ b) βŠ•β‚€ c)
  βŠ•-assoc = [ ι₁ ∘ ι₁ , [ ι₁ ∘ ΞΉβ‚‚ , ΞΉβ‚‚ ] ]