inverse' : Functor 1 (C -> 1) := Functors.
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.