(** * Notations for categories *)Require Category.Dual. Require Category.Morphisms. Require Category.Pi. Require Category.Prod. Require Category.Sum. Require Category.Sigma. Include Category.Core.CategoryCoreNotations. Include Category.Dual.CategoryDualNotations. Include Category.Morphisms.CategoryMorphismsNotations. Include Category.Pi.CategoryPiNotations. Include Category.Prod.CategoryProdNotations. Include Category.Sum.CategorySumNotations. Include Category.Sigma.CategorySigmaNotations.