{C D} c : (swap C D) ((swap D C) c) = c := match c with type_inl _ => idpath | type_inr _ => idpath end.
Require Import Category.Sum Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths HoTT.Tactics Types.Forall. Require Import Basics.Tactics.