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