C : Functor 0 C := Eval simpl in from_initial C. Local Notation "! x" := (@from_terminal _ terminal_category _ _ _ x) : functor_scope. Section unique. Context `{Funext}. Global Instance trunc_initial_category_function `{@IsInitialCategory zero} T : Contr (zero -> T). Proof. refine (Build_Contr _ (initial_category_ind _) _). intro y. apply path_forall; intro x. apply (initial_category_ind _ x). Defined.
Require Import Category.Core Functor.Core Functor.Paths. Require Import InitialTerminalCategory.Core. Require Import NatCategory. Require Import HoTT.Basics.