Functor (S / T) (A * B) := Build_Functor (S / T) (A * B) (fun abf => (CommaCategory.
Require Import Category.Core Functor.Core. Require Import Category.Prod Functor.Prod.Core. Require Import Functor.Composition.Core Functor.Identity. Require Import InitialTerminalCategory.Functors. Require Import Types.Prod. Import Comma.Core.