C : Functor C 1 := Eval simpl in to_terminal C.
Require Import Category.Core Functor.Core Functor.Paths. Require Import InitialTerminalCategory.Core. Require Import NatCategory. Require Import HoTT.Basics.