{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| Module  : FiniteCategories
Description : __'Ens'__ are full subcategories of __Set__ (__'FinSet'__ for us) in a given set universe.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

__'Ens'__ are full subcategories of __Set__ (__'FinSet'__ for us) in a given set universe.

(See "Categories for the Working Mathematican" Saunders Mac Lane. p.11)
-}

module Math.FiniteCategories.Ens 
(
    Ens,
    ens
)
where
    import          Math.FiniteCategory
    import          Math.FiniteCategories.FullSubcategory
    import          Math.Categories.FinSet

    import          Data.WeakSet            (Set) 
    import          Data.WeakSet.Safe 
    
    -- | __'Ens'__ are full subcategories of __Set__ (__'FinSet'__ for us) in a given set universe.
    type Ens a = InheritedFullSubcategory (FinSet a) (Function a) (Set a)

    -- | The __'Ens'__ generated by a set universe. (See "Categories for the Working Mathematican" Saunders Mac Lane. p.11)
    ens :: Set (Set a) -> Ens a
    ens s = InheritedFullSubcategory FinSet s