categories-1.0.7: Categories

Copyright | 2008-2010 Edward Kmett
License | BSD
Maintainer | Edward Kmett <ekmett@gmail.com>
Stability | experimental
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Control.Category.Discrete

Description

Synopsis

- data Discrete a b where
  - Refl :: forall a. Discrete a a
- liftDiscrete :: Discrete a b -> Discrete (f a) (f b)
- cast :: Category k => Discrete a b -> k a b
- inverse :: Discrete a b -> Discrete b a

# Documentation

data Discrete a b where Source #

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

Constructors

Refl :: forall a. Discrete a a |

#### Instances

Instances details

Category Discrete Source # |
Instance details Defined in Control.Category.Discrete Methods id :: Discrete a a Source # (.) :: Discrete b c -> Discrete a b -> Discrete a c Source #

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 #