`{Funext} `{@IsTerminalCategory one Hone Hone'} (c : PreCategory) : Pseudofunctor one. Proof. refine (Build_Pseudofunctor one (fun _ => c) (fun _ _ _ => 1%functor) (fun _ _ _ _ _ => reflexivity _) (fun _ => reflexivity _) _ _ _); simpl; abstract ( intros; path_natural_transformation; rewrite ap_const; simpl; reflexivity ). Defined.
Require Import Category.Core Functor.Core. Require Import Functor.Identity. Require Import Pseudofunctor.Core. Require Import InitialTerminalCategory.Core. Require Import FunctorCategory.Morphisms. Require Import NaturalTransformation.Paths. Require Import NatCategory. Require Import PathGroupoids.