Data.Category.Adjunction

Adjunctions

data Adjunction c d f g

mkAdjunction

leftAdjunct

rightAdjunct

Adjunctions as a category

idAdj

composeAdj

data AdjArrow c d

Adjunctions from universal morphisms

initialPropAdjunction

terminalPropAdjunction

Universal morphisms from adjunctions

adjunctionInitialProp

adjunctionTerminalProp

Examples

precomposeAdj

postcomposeAdj

contAdj