fact: Definition arrow_category := comma_category (Functor.Identity.identity C) (Functor.Identity.identity C).
imports: Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Strict HoTT.Basics HoTT.Types