Data.Category.Limit

Preliminairies

Diagonal Functor

data Diag

type DiagF f

Cones

type Cone f n

type Cocone f n

coneVertex

coconeVertex

Limits

type family LimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *

type Limit f

class HasLimits j k

data LimitFunctor j k

limitAdj

rightAdjointPreservesLimits

rightAdjointPreservesLimitsInv

Colimits

type family ColimitFam (j :: * -> * -> *) (k :: * -> * -> *) (f :: *) :: *

type Colimit f

class HasColimits j k

data ColimitFunctor j k

colimitAdj

leftAdjointPreservesColimits

leftAdjointPreservesColimitsInv

Limits of type Void

class HasTerminalObject k

class HasInitialObject k

data Zero

Limits of type Pair

class HasBinaryProducts k

data ProductFunctor k

data p :*: q

prodAdj

class HasBinaryCoproducts k

data CoproductFunctor k

data p :+: q

coprodAdj