PreCategory. Proof. refine (@Build_PreCategory SectionOfFunctor (fun F G => NaturalTransformation F G) (fun F => 1) (fun _ _ _ T U => T o U) _ _ _ _); abstract (path_natural_transformation; auto with morphism). Defined.
Require Import Functor.Core NaturalTransformation.Core. Require Import Category.Strict. Require Import Functor.Identity NaturalTransformation.Identity. Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core. Require Import Functor.Paths. Require Import HoTT.Basics HoTT.Types.