categories-1.0.7: Categories

Copyright2008-2010 Edward Kmett
LicenseBSD
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Control.Category.Discrete

Description

 

Synopsis

Documentation

data Discrete a b where Source

Category of discrete objects. The only arrows are identity arrows.

Constructors

Refl :: Discrete a a 

Instances

liftDiscrete :: Discrete a b -> Discrete (f a) (f b) Source

Discrete a b acts as a proof that a = b, lift that proof into something of kind * -> *

cast :: Category k => Discrete a b -> k a b Source

Lower the proof that a ~ b to an arbitrary category.

inverse :: Discrete a b -> Discrete b a Source