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