Copyright	Guillaume Sabbagh 2023
License	GPL-3
Maintainer	guillaumesabbagh@protonmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Math.FiniteCategories.DiscreteTwo

Description

The DiscreteTwo category contains two objects and their identities.

You can construct it using DiscreteCategory, it is defined as a standalone category because it is often used unlike other discrete categories.

Synopsis

data DiscreteTwoOb
- = A
- | B
type DiscreteTwoAr = DiscreteTwoOb
data DiscreteTwo = DiscreteTwo
twoDiagram :: (Category c m o, Morphism m o) => c -> o -> o -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
insertionDiscreteTwoInDiscreteCategory :: Eq t => DiscreteCategory t -> t -> t -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb (DiscreteCategory t) (DiscreteMorphism t) t

Documentation

data DiscreteTwoOb Source #

DiscreteTwoOb is a datatype used as the object type and the morphism type.

It has two constructors A and B.

Constructors

A
B

Instances

Instances details

PrettyPrint DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods pprint :: Int -> DiscreteTwoOb -> String Source # pprintWithIndentations :: Int -> Int -> String -> DiscreteTwoOb -> String Source # pprintIndent :: Int -> DiscreteTwoOb -> String Source #
Simplifiable DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods simplify :: DiscreteTwoOb -> DiscreteTwoOb #
Generic DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Associated Types type Rep DiscreteTwoOb :: Type -> Type Methods from :: DiscreteTwoOb -> Rep DiscreteTwoOb x to :: Rep DiscreteTwoOb x -> DiscreteTwoOb
Show DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods showsPrec :: Int -> DiscreteTwoOb -> ShowS show :: DiscreteTwoOb -> String showList :: [DiscreteTwoOb] -> ShowS
Eq DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods (==) :: DiscreteTwoOb -> DiscreteTwoOb -> Bool (/=) :: DiscreteTwoOb -> DiscreteTwoOb -> Bool
Morphism DiscreteTwoOb DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods (@) :: DiscreteTwoOb -> DiscreteTwoOb -> DiscreteTwoOb Source # (@?) :: DiscreteTwoOb -> DiscreteTwoOb -> Maybe DiscreteTwoOb Source # source :: DiscreteTwoOb -> DiscreteTwoOb Source # target :: DiscreteTwoOb -> DiscreteTwoOb Source #
Category DiscreteTwo DiscreteTwoOb DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods identity :: DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb Source # ar :: DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb -> Set DiscreteTwoOb Source # genAr :: DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb -> Set DiscreteTwoOb Source # decompose :: DiscreteTwo -> DiscreteTwoOb -> [DiscreteTwoOb] Source #
FiniteCategory DiscreteTwo DiscreteTwoOb DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods ob :: DiscreteTwo -> Set DiscreteTwoOb Source #
Eq a => CartesianClosedCategory (FinSet a) (Function a) (Set a) (FinSet (TwoProduct a)) (Function (TwoProduct a)) (Set (TwoProduct a)) (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a)) Source #
Instance details Defined in Math.Categories.FinSet Methods internalHom :: TwoBase (FinSet a) (Function a) (Set a) -> Tripod (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a)) Source #
type Rep DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo type Rep DiscreteTwoOb = D1 ('MetaData "DiscreteTwoOb" "Math.FiniteCategories.DiscreteTwo" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "A" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "B" 'PrefixI 'False) (U1 :: Type -> Type))

type DiscreteTwoAr = DiscreteTwoOb Source #

There are two identities corresponding to A and B.

data DiscreteTwo Source #

DiscreteTwo is a datatype used as category type.

Constructors

DiscreteTwo

Instances

Instances details

PrettyPrint DiscreteTwo Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods pprint :: Int -> DiscreteTwo -> String Source # pprintWithIndentations :: Int -> Int -> String -> DiscreteTwo -> String Source # pprintIndent :: Int -> DiscreteTwo -> String Source #
Simplifiable DiscreteTwo Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods simplify :: DiscreteTwo -> DiscreteTwo #
Generic DiscreteTwo Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Associated Types type Rep DiscreteTwo :: Type -> Type Methods from :: DiscreteTwo -> Rep DiscreteTwo x to :: Rep DiscreteTwo x -> DiscreteTwo
Show DiscreteTwo Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods showsPrec :: Int -> DiscreteTwo -> ShowS show :: DiscreteTwo -> String showList :: [DiscreteTwo] -> ShowS
Eq DiscreteTwo Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods (==) :: DiscreteTwo -> DiscreteTwo -> Bool (/=) :: DiscreteTwo -> DiscreteTwo -> Bool
Category DiscreteTwo DiscreteTwoOb DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods identity :: DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb Source # ar :: DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb -> Set DiscreteTwoOb Source # genAr :: DiscreteTwo -> DiscreteTwoOb -> DiscreteTwoOb -> Set DiscreteTwoOb Source # decompose :: DiscreteTwo -> DiscreteTwoOb -> [DiscreteTwoOb] Source #
FiniteCategory DiscreteTwo DiscreteTwoOb DiscreteTwoOb Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo Methods ob :: DiscreteTwo -> Set DiscreteTwoOb Source #
type Rep DiscreteTwo Source #
Instance details Defined in Math.FiniteCategories.DiscreteTwo type Rep DiscreteTwo = D1 ('MetaData "DiscreteTwo" "Math.FiniteCategories.DiscreteTwo" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "DiscreteTwo" 'PrefixI 'False) (U1 :: Type -> Type))

twoDiagram :: (Category c m o, Morphism m o) => c -> o -> o -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o Source #

Constructs a diagram from DiscreteTwo to another category.

insertionDiscreteTwoInDiscreteCategory :: Eq t => DiscreteCategory t -> t -> t -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb (DiscreteCategory t) (DiscreteMorphism t) t Source #

Return an insertion functor from DiscreteTwo to a DiscreteCategory given a DiscreteCategory and the image of A and B.