data-category-0.7.2: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Category.Fix

Description

 
Synopsis

Documentation

newtype Fix f a b Source #

Constructors

Fix (f (Fix f) a b) 
Instances
Category (f (Fix f)) => Category (Fix f) Source #

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

Instance details

Defined in Data.Category.Fix

Methods

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

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

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

Category (f (Fix f)) => Functor (Unwrap (Fix f)) Source #

The Unwrap functor unwraps Fix f to f (Fix f).

Instance details

Defined in Data.Category.Fix

Associated Types

type Dom (Unwrap (Fix f)) :: Type -> Type -> Type Source #

type Cod (Unwrap (Fix f)) :: Type -> Type -> Type Source #

type (Unwrap (Fix f)) :% a :: Type Source #

Methods

(%) :: Unwrap (Fix f) -> Dom (Unwrap (Fix f)) a b -> Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% b) Source #

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

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

Instance details

Defined in Data.Category.Fix

Associated Types

type Dom (Wrap (Fix f)) :: Type -> Type -> Type Source #

type Cod (Wrap (Fix f)) :: Type -> Type -> Type Source #

type (Wrap (Fix f)) :% a :: Type Source #

Methods

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

HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) Source # 
Instance details

Defined in Data.Category.Fix

Associated Types

type BinaryCoproduct (Fix f) x y :: Type Source #

Methods

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

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

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

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

HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) Source # 
Instance details

Defined in Data.Category.Fix

Associated Types

type BinaryProduct (Fix f) x y :: Type Source #

Methods

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

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

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

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

HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) Source # 
Instance details

Defined in Data.Category.Fix

Associated Types

type InitialObject (Fix f) :: Type Source #

HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) Source # 
Instance details

Defined in Data.Category.Fix

Associated Types

type TerminalObject (Fix f) :: Type Source #

CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) Source # 
Instance details

Defined in Data.Category.Fix

Associated Types

type Exponential (Fix f) y z :: Type Source #

Methods

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

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

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

(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source #

Fix f inherits tensor products from f (Fix f).

Instance details

Defined in Data.Category.Fix

Associated Types

type Unit (WrapTensor (Fix f) t) :: Type Source #

Methods

unitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source #

leftUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) a Source #

leftUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) Source #

rightUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) a Source #

rightUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) Source #

associator :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) Source #

associatorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) Source #

type Dom (Unwrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Dom (Unwrap (Fix f)) = Fix f
type Dom (Wrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Dom (Wrap (Fix f)) = f (Fix f)
type Cod (Unwrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Cod (Unwrap (Fix f)) = f (Fix f)
type Cod (Wrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Cod (Wrap (Fix f)) = Fix f
type InitialObject (Fix f) Source #

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

Instance details

Defined in Data.Category.Fix

type InitialObject (Fix f) = InitialObject (f (Fix f))
type TerminalObject (Fix f) Source #

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

Instance details

Defined in Data.Category.Fix

type (Unwrap (Fix f)) :% a Source # 
Instance details

Defined in Data.Category.Fix

type (Unwrap (Fix f)) :% a = a
type (Wrap (Fix f)) :% a Source # 
Instance details

Defined in Data.Category.Fix

type (Wrap (Fix f)) :% a = a
type BinaryCoproduct (Fix f) x y Source #

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

Instance details

Defined in Data.Category.Fix

type BinaryCoproduct (Fix f) x y = BinaryCoproduct (f (Fix f)) x y
type BinaryProduct (Fix f) x y Source #

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

Instance details

Defined in Data.Category.Fix

type BinaryProduct (Fix f) x y = BinaryProduct (f (Fix f)) x y
type Exponential (Fix f) y z Source #

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

Instance details

Defined in Data.Category.Fix

type Exponential (Fix f) y z = Exponential (f (Fix f)) y z
type Unit (WrapTensor (Fix f) t) Source # 
Instance details

Defined in Data.Category.Fix

type Unit (WrapTensor (Fix f) t) = Unit t

data Wrap (f :: * -> * -> *) Source #

Constructors

Wrap 
Instances
Category (f (Fix f)) => Functor (Wrap (Fix f)) Source #

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

Instance details

Defined in Data.Category.Fix

Associated Types

type Dom (Wrap (Fix f)) :: Type -> Type -> Type Source #

type Cod (Wrap (Fix f)) :: Type -> Type -> Type Source #

type (Wrap (Fix f)) :% a :: Type Source #

Methods

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

(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source #

Fix f inherits tensor products from f (Fix f).

Instance details

Defined in Data.Category.Fix

Associated Types

type Unit (WrapTensor (Fix f) t) :: Type Source #

Methods

unitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source #

leftUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) a Source #

leftUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) Source #

rightUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) a Source #

rightUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) Source #

associator :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) Source #

associatorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) Source #

type Dom (Wrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Dom (Wrap (Fix f)) = f (Fix f)
type Cod (Wrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Cod (Wrap (Fix f)) = Fix f
type (Wrap (Fix f)) :% a Source # 
Instance details

Defined in Data.Category.Fix

type (Wrap (Fix f)) :% a = a
type Unit (WrapTensor (Fix f) t) Source # 
Instance details

Defined in Data.Category.Fix

type Unit (WrapTensor (Fix f) t) = Unit t

data Unwrap (f :: * -> * -> *) Source #

Constructors

Unwrap 
Instances
Category (f (Fix f)) => Functor (Unwrap (Fix f)) Source #

The Unwrap functor unwraps Fix f to f (Fix f).

Instance details

Defined in Data.Category.Fix

Associated Types

type Dom (Unwrap (Fix f)) :: Type -> Type -> Type Source #

type Cod (Unwrap (Fix f)) :: Type -> Type -> Type Source #

type (Unwrap (Fix f)) :% a :: Type Source #

Methods

(%) :: Unwrap (Fix f) -> Dom (Unwrap (Fix f)) a b -> Cod (Unwrap (Fix f)) (Unwrap (Fix f) :% a) (Unwrap (Fix f) :% b) Source #

(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source #

Fix f inherits tensor products from f (Fix f).

Instance details

Defined in Data.Category.Fix

Associated Types

type Unit (WrapTensor (Fix f) t) :: Type Source #

Methods

unitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source #

leftUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) a Source #

leftUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) Source #

rightUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) a Source #

rightUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) Source #

associator :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) Source #

associatorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) Source #

type Dom (Unwrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Dom (Unwrap (Fix f)) = Fix f
type Cod (Unwrap (Fix f)) Source # 
Instance details

Defined in Data.Category.Fix

type Cod (Unwrap (Fix f)) = f (Fix f)
type (Unwrap (Fix f)) :% a Source # 
Instance details

Defined in Data.Category.Fix

type (Unwrap (Fix f)) :% a = a
type Unit (WrapTensor (Fix f) t) Source # 
Instance details

Defined in Data.Category.Fix

type Unit (WrapTensor (Fix f) t) = Unit t

type WrapTensor f t = (Wrap f :.: t) :.: (Unwrap f :***: Unwrap f) Source #

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

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.

type Z = I1 () Source #

type S n = I2 n Source #

pattern Z :: Obj Omega Z Source #

pattern S :: Omega a b -> Omega (S a) (S b) Source #

z2s :: Obj Omega n -> Omega Z (S n) Source #