Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(** * The coproduct of categories *)

[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]


Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

(** ** Definition of [+] for categories *)
Section internals.
  Variables C D : PreCategory.

  Definition sum_morphism (s d : C + D) : Type
    := match s, d with
         | inl s, inl d => morphism C s d
         | inr s, inr d => morphism D s d
         | _, _ => Empty
       end.

  Global Arguments sum_morphism _ _ / .

  Definition sum_identity (x : C + D) : sum_morphism x x
    := match x with
         | inl x => identity x
         | inr x => identity x
       end.

  Global Arguments sum_identity _ / .

  
C, D: PreCategory
s, d, d': C + D
m1: sum_morphism d d'
m2: sum_morphism s d
sum_morphism s d'

  
C, D: PreCategory
s, d, d': C + D
m1: sum_morphism d d'
m2: sum_morphism s d
sum_morphism s d'

    case s, d, d'; simpl in *;
    solve [ case m1
          | case m2
          | eapply compose; eassumption ].
  Defined.

  Global Arguments sum_compose [_ _ _] _ _ / .
End internals.


C, D: PreCategory
PreCategory


C, D: PreCategory
PreCategory

  refine (@Build_PreCategory
            (C + D)%type
            (sum_morphism C D)
            (sum_identity C D)
            (sum_compose C D)
            _
            _
            _
            _);
  abstract (
      repeat (simpl || apply istrunc_S || intros [] || intro);
      auto with morphism;
      typeclasses eauto
    ).
Defined.

Module Export CategorySumNotations.
  Infix "+" := sum : category_scope.
End CategorySumNotations.