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