{-| Module : FiniteCategories Description : An example of 'FullSubcategory' of __'FinCat'__. Copyright : Guillaume Sabbagh 2022 License : GPL-3 Maintainer : guillaumesabbagh@protonmail.com Stability : experimental Portability : portable An example of 'FullSubcategory' of __'FinCat'__. -} module Math.FiniteCategories.FinCat.Examples ( exampleFinCatNumbers, ) where import Data.WeakSet.Safe import Math.Categories import Math.FiniteCategories import Math.FiniteCategory -- | The 'FullSubcategory' of __'FinCat'__ containing the number categories 0,1, and 2. exampleFinCatNumbers :: FullSubcategory (FinCat NumberCategory NumberCategoryMorphism numberCategoryObject) (FinFunctor NumberCategory NumberCategoryMorphism numberCategoryObject) NumberCategory exampleFinCatNumbers = FullSubcategory FinCat (numberCategory <$> (set [0..2]))