Control.Comonad.Square

Documentation

extract :: Comonad w => Square '[] '[] '[w] '[]

+--w--+
|  v  |
|  X  |
|     |
+-----+

extend :: Comonad w => Square '[Costar w] '[] '[w] '[w]

+--w--+
|  v  |
w<-E  |
|  v  |
+--w--+

extend as a square

Right identity law:

+--w--+
|  v  |     +--w--+
w<-E  |     |  v  |
|  v  | === w<-/  |
|  X  |     |     |
+-----+     +-----+

Left identity law:

+---w-+
|   v |     +--w--+
| /-E |     |  |  |
| v | | === |  v  |
| X v |     |  |  |
+---w-+     +--w--+

Associativity law:

+--w--+     +---w-+
|  v  |     |   v |
w<-E  |     | /-E |
|  v  | === w<E | |
w<-E  |     | | | |
|  v  |     w</ v |
+--w--+     +---w-+

duplicate :: Comonad w => Square '[] '[] '[w] '[w, w]

+---w-+
|   v |
| /-@ |
| v v |
+-w-w-+

duplicate = fromRight ||| extend

(<=<) :: Comonad w => Square '[Costar w, Costar w] '[Costar w] '[] '[]

+-----+
|  /-<w
w<-@  |
w<-/  |
+-----+

Cokleisli composition `(W.<=<)`

(<=<) = fromRight === extend === toLeft