Library HoTT.Categories.Category.Notations
Require Category.Core.
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.
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.