(** * Coproduct of natural transformations *)
Require Import Category.Sum Functor.Sum NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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

Section sum.
  Definition sum
             C C' D F G F' G'
             (T : @NaturalTransformation C D F G)
             (T' : @NaturalTransformation C' D F' G')
  : NaturalTransformation (F + F') (G + G').
C, C', D: PreCategory
F, G: Core.Functor C D
F', G': Core.Functor C' D
T: NaturalTransformation F G
T': NaturalTransformation F' G'
NaturalTransformation (F + F') (G + G')
  Proof.
C, C', D: PreCategory
F, G: Core.Functor C D
F', G': Core.Functor C' D
T: NaturalTransformation F G
T': NaturalTransformation F' G'
NaturalTransformation (F + F') (G + G')
    refine (Build_NaturalTransformation
              (F + F') (G + G')
              (fun x => match x with
                          | Basics.Overture.inl c => T c
                          | Basics.Overture.inr c' => T' c'
                        end)
              _).
C, C', D: PreCategory
F, G: Core.Functor C D
F', G': Core.Functor C' D
T: NaturalTransformation F G
T': NaturalTransformation F' G'
forall (s d : (C + C')%category)
(m : morphism (C + C') s d),
(match
   d as x
   return
     (morphism D (Core.object_of (F + F') x)
        (Core.object_of (G + G') x))
 with
 | Overture.inl c => T c
 | Overture.inr c' => T' c'
 end o Core.morphism_of (F + F') m)%morphism =
(Core.morphism_of (G + G') m
 o match
     s as x
     return
       (morphism D (Core.object_of (F + F') x)
          (Core.object_of (G + G') x))
   with
   | Overture.inl c => T c
   | Overture.inr c' => T' c'
   end)%morphism
    abstract (
        repeat (intros [] || intro); simpl;
        auto with natural_transformation
      ).
  Defined.
End sum.

Module Export NaturalTransformationSumNotations.
  Notation "T + U" := (sum T U) : natural_transformation_scope.
End NaturalTransformationSumNotations.