Functor (a / S) A := Eval simpl in snd o comma_category_projection !a S.
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.