proposition: Lemma isstrict_functor_category `{Funext} C `{IsStrictCategory D} : IsStrictCategory (C -> D).
proof: Proof. typeclasses eauto. Defined.
imports: Category.Strict Functor.Core NaturalTransformation.Core Functor.Paths NaturalTransformation.Composition.Core NaturalTransformation.Identity NaturalTransformation.Composition.Laws NaturalTransformation.Paths