posttensor I.
Require Import Basics.Utf8. Require Import Category.Core Category.Morphisms. Require Import Functor.Core Require Import NaturalTransformation.Core. Require Import FunctorCategory.Core FunctorCategory.Morphisms. Require Import ProductLaws.