Documentation
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.
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.