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