fact: Definition coslice_category_projection : Functor (a / S) A := Eval simpl in snd o comma_category_projection !a S.
imports: Category.Core Functor.Core Category.Prod Functor.Prod.Core Functor.Composition.Core Functor.Identity InitialTerminalCategory.Functors Types.Prod