(C D : PreCategory) : Functor (C * D) (D * C) := Build_Functor (C * D) (D * C) (fun cd => (snd_type cd, fst_type cd)%core) (fun _ _ m => (snd_type m, fst_type m)%core) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
Require Import HoTT.Basics HoTT.Types. Require Import Category.Core Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Prod Functor.Prod Functor.Composition.Core Functor.Identity Functor.Composition.Laws.