C D : Functor (C + D) (D + C) := sum (inr _ _) (inl _ _).
Require Import Category.Sum Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths HoTT.Tactics Types.Forall. Require Import Basics.Tactics.