Safe Haskell	None
Language	GHC2021

Control.Comonad.Travel.Boolean

Description

A small but non-trivial example of category - comonad correspondence

Synopsis

data H r
- = H1 r
- | H2 r r
data Implies (x :: Bool) (y :: Bool) where
- ImpId :: forall (x :: Bool). Implies x x
- ImpFT :: Implies 'False 'True
toH :: Travel Implies r -> H r
fromH :: H r -> Travel Implies r

Documentation

data H r Source #

Constructors

H1 r
H2 r r

Instances details

Functor H Source #
Instance details Defined in Control.Comonad.Travel.Boolean Methods fmap :: (a -> b) -> H a -> H b # (<$) :: a -> H b -> H a #
Comonad H Source #
Instance details Defined in Control.Comonad.Travel.Boolean Methods extract :: H a -> a # duplicate :: H a -> H (H a) # extend :: (H a -> b) -> H a -> H b #

data Implies (x :: Bool) (y :: Bool) where Source #

Boolean algebra {False, True} can be seen as a category:

False ---> True
  ↺         ↺

Note: Roughly speaking, there are only three values in types Implies b1 b2, where b1, b2 are chosen from either False or True.

ImpId :: Implies False False
ImpId :: Implies True True
ImpFT :: Implies False True

Constructors

ImpId :: forall (x :: Bool). Implies x x
ImpFT :: Implies 'False 'True

Instances details

Category Implies Source #
Instance details Defined in Control.Comonad.Travel.Boolean Methods id :: forall (a :: Bool). Implies a a # (.) :: forall (b :: Bool) (c :: Bool) (a :: Bool). Implies b c -> Implies a b -> Implies a c #

Travel Implies is isomorphic to H, including its Comonad instance.