Data.Category.Fix

Documentation

newtype Fix f a b

Constructors

Fix (f (Fix f) a b)

Instances

Category (f (Fix f)) => Category (Fix f)

Fix f is the fixed point category for a category combinator f.

Methods

src :: Fix f a b -> Obj (Fix f) a

tgt :: Fix f a b -> Obj (Fix f) b

(.) :: Fix f b c -> Fix f a b -> Fix f a c

HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)

Fix f inherits its (co)limits from f (Fix f).

Associated Types

type BinaryCoproduct (Fix f :: * -> * -> *) x y :: *

Methods

inj1 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f x (BinaryCoproduct (Fix f) x y)

inj2 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f y (BinaryCoproduct (Fix f) x y)

(|||) :: Fix f x a -> Fix f y a -> Fix f (BinaryCoproduct (Fix f) x y) a

(+++) :: Fix f a1 b1 -> Fix f a2 b2 -> Fix f (BinaryCoproduct (Fix f) a1 a2) (BinaryCoproduct (Fix f) b1 b2)

HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)

Fix f inherits its (co)limits from f (Fix f).

Associated Types

type BinaryProduct (Fix f :: * -> * -> *) x y :: *

Methods

proj1 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) x

proj2 :: Obj (Fix f) x -> Obj (Fix f) y -> Fix f (BinaryProduct (Fix f) x y) y

(&&&) :: Fix f a x -> Fix f a y -> Fix f a (BinaryProduct (Fix f) x y)

(***) :: Fix f a1 b1 -> Fix f a2 b2 -> Fix f (BinaryProduct (Fix f) a1 a2) (BinaryProduct (Fix f) b1 b2)

HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)

Fix f inherits its (co)limits from f (Fix f).

Associated Types

type InitialObject (Fix f :: * -> * -> *) :: *

Methods

initialObject :: Obj (Fix f) (InitialObject (Fix f))

initialize :: Obj (Fix f) a -> Fix f (InitialObject (Fix f)) a

HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)

Fix f inherits its (co)limits from f (Fix f).

Associated Types

type TerminalObject (Fix f :: * -> * -> *) :: *

Methods

terminalObject :: Obj (Fix f) (TerminalObject (Fix f))

terminate :: Obj (Fix f) a -> Fix f a (TerminalObject (Fix f))

CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)

Fix f inherits its exponentials from f (Fix f).

Associated Types

type Exponential (Fix f :: * -> * -> *) y z :: *

Methods

apply :: Obj (Fix f) y -> Obj (Fix f) z -> Fix f (BinaryProduct (Fix f) (Exponential (Fix f) y z) y) z

tuple :: Obj (Fix f) y -> Obj (Fix f) z -> Fix f z (Exponential (Fix f) y (BinaryProduct (Fix f) z y))

(^^^) :: Fix f z1 z2 -> Fix f y2 y1 -> Fix f (Exponential (Fix f) y1 z1) (Exponential (Fix f) y2 z2)

type InitialObject (Fix f)

type InitialObject (Fix f) = InitialObject (f (Fix f))

type TerminalObject (Fix f)

type TerminalObject (Fix f) = TerminalObject (f (Fix f))

type BinaryCoproduct (Fix f) a b

type BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b

type BinaryProduct (Fix f) a b

type BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b

type Exponential (Fix f) a b

type Exponential (Fix f) a b = Exponential (f (Fix f)) a b

data Wrap f

Constructors

Wrap

Instances

Category (f (Fix f)) => Functor (Wrap f)

The Wrap functor wraps Fix around f (Fix f).

Associated Types

type Dom (Wrap f) :: * -> * -> *

type Cod (Wrap f) :: * -> * -> *

type (Wrap f) :% a :: *

Methods

(%) :: Wrap f -> Dom (Wrap f) a b -> Cod (Wrap f) (Wrap f :% a) (Wrap f :% b)

type Dom (Wrap f)

type Dom (Wrap f) = f (Fix f)

type Cod (Wrap f)

type Cod (Wrap f) = Fix f

type (Wrap f) :% a

type (Wrap f) :% a = a

type Omega = Fix ((:>>:) Unit)

Take the Omega category, add a new disctinct object, and an arrow from that object to every object in Omega, and you get Omega again.