| License | BSD-style (see the file LICENSE) |
|---|---|
| Maintainer | sjoerd@w3future.com |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Data.Functor.Adjunction.Square
Description
Synopsis
- leftAdjunct :: Adjunction f g => Square '[Costar f] '[Star g] '[] '[]
- rightAdjunct :: Adjunction f g => Square '[Star g] '[Costar f] '[] '[]
- unit :: Adjunction f g => Square '[] '[] '[] '[f, g]
- counit :: Adjunction f g => Square '[] '[] '[g, f] '[]
Documentation
leftAdjunct :: Adjunction f g => Square '[Costar f] '[Star g] '[] '[] Source #
+-----+ | | f<-@->g | | +-----+
leftAdjunct = unit === (toLeft ||| toRight)
rightAdjunct :: Adjunction f g => Square '[Star g] '[Costar f] '[] '[] Source #
+-----+ | | g>-@-<f | | +-----+
rightAdjunct = (fromLeft ||| fromRight) === counit
unit :: Adjunction f g => Square '[] '[] '[] '[f, g] Source #
+-----+ | | | /@\ | | v v | +-f-g-+
unit = fromRight ||| leftAdj ||| fromLeft
counit :: Adjunction f g => Square '[] '[] '[g, f] '[] Source #
+-g-f-+ | v v | | \@/ | | | +-----+
counit = toRight ||| rightAdjoint ||| toLeft