`{Funext} `{@IsInitialCategory zero} : Pseudofunctor zero := Build_Pseudofunctor zero (fun x => initial_category_ind _ x) (fun x _ _ => initial_category_ind _ x) (fun x _ _ _ _ => initial_category_ind _ x) (fun x => initial_category_ind _ x) (fun x => initial_category_ind _ x) (fun x => initial_category_ind _ x) (fun x => initial_category_ind _ x).
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.