(a : A) : Functor (A / a) A := Eval simpl in fst o comma_category_projection 1 _.
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.