License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Functor.Kan.Square

Description

Synopsis

lanSquare :: Functor f => Square '[] '[] '[f] '[j, Lan j f]
lanFactor :: Functor g => Square '[] '[] '[f] '[j, g] -> Square '[] '[] '[Lan j f] '[g]
ranSquare :: Functor g => Square '[] '[] '[j, Ran j g] '[g]
ranFactor :: Functor f => Square '[] '[] '[j, f] '[g] -> Square '[] '[] '[f] '[Ran j g]

Documentation

lanSquare :: Functor f => Square '[] '[] '[f] '[j, Lan j f] Source #

+--f--+
|  v  |
|  @  |
| / \ |
| v v |
+-j-L-+

lanFactor :: Functor g => Square '[] '[] '[f] '[j, g] -> Square '[] '[] '[Lan j f] '[g] Source #

+--f--+     +--L--+
|  v  |     |  v  |
|  @  | ==> |  @  |
| / \ |     |  |  |
| v v |     |  v  |
+-j-g-+     +--g--+

Any square like the one on the left factors through lanSquare. lanFactor gives the remaining square.

ranSquare :: Functor g => Square '[] '[] '[j, Ran j g] '[g] Source #

+-j-R-+
| v v |
| \ / |
|  @  |
|  v  |
+--g--+

ranFactor :: Functor f => Square '[] '[] '[j, f] '[g] -> Square '[] '[] '[f] '[Ran j g] Source #

+-j-f-+     +--f--+
| v v |     |  v  |
| \ / | ==> |  @  |
|  @  |     |  |  |
|  v  |     |  v  |
+--g--+     +--R--+

Any square like the one on the left factors through ranSquare. ranFactor gives the remaining square.