(F : Functor C D) (F' : Functor C' D) : Functor (C + C') D. Proof. refine (Build_Functor (C + C') D (fun cc' => match cc' with | type_inl c => F c | type_inr c' => F' c' end) (fun s d => match s, d with | type_inl cs, type_inl cd => fun m : morphism _ cs cd => F _1 m | type_inr c's, type_inr c'd => fun m : morphism _ c's c'd => F' _1 m | _, _ => fun m => match m with end end%morphism) _ _); abstract ( repeat (intros [] || intro); simpl in *; auto with functor ). Defined.
Require Import Category.Sum Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths HoTT.Tactics Types.Forall. Require Import Basics.Tactics.