fact: Definition snd : Functor (C * D) D := Build_Functor (C * D) D (@snd _ _) (fun _ _ => @snd _ _) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
imports: Category.Core Functor.Core Category.Prod Functor.Composition.Core Types.Prod