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