fact: Definition functor' : Functor (C -> 1) 1 := Functors.to_terminal _.
imports: Category.Core Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core NaturalTransformation.Paths InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations HoTT.Basics HoTT.Types