`{Funext} C `{IsStrictCategory D} : IsStrictCategory (C -> D). Proof. typeclasses eauto. Defined.
Require Import Category.Strict Functor.Core NaturalTransformation.Core Functor.Paths. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Identity NaturalTransformation.Composition.Laws NaturalTransformation.Paths.