Functor (1 -> C) C := Build_Functor (1 -> C) C (fun F => F (center _)) (fun s d m => m (center _)) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core NaturalTransformation.Paths. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations. Require Import HoTT.Basics HoTT.Types.