data-category-0.7.2: Category theory

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

Data.Category.Functor

Contents

Description

 
Synopsis

Cat

data Cat :: * -> * -> * where Source #

Functors are arrows in the category Cat.

Constructors

CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag)) 
Instances
Category Cat Source #

Cat is the category with categories as objects and funtors as arrows.

Instance details

Defined in Data.Category.Functor

Methods

src :: Cat a b -> Obj Cat a Source #

tgt :: Cat a b -> Obj Cat b Source #

(.) :: Cat b c -> Cat a b -> Cat a c Source #

HasBinaryCoproducts Cat Source #

The coproduct of categories :++: is the binary coproduct in Cat.

Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct Cat x y :: Type Source #

Methods

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

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

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

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

HasBinaryProducts Cat Source #

The product of categories :**: is the binary product in Cat.

Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryProduct Cat x y :: Type Source #

Methods

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

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

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

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

HasInitialObject Cat Source #

The empty category is the initial object in Cat.

Instance details

Defined in Data.Category.Limit

Associated Types

type InitialObject Cat :: Type Source #

HasTerminalObject Cat Source #

Unit is the terminal category.

Instance details

Defined in Data.Category.Limit

Associated Types

type TerminalObject Cat :: Type Source #

CartesianClosed Cat Source #

Exponentials in Cat are the functor categories.

Instance details

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential Cat y z :: Type Source #

Methods

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

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

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

type InitialObject Cat Source # 
Instance details

Defined in Data.Category.Limit

type TerminalObject Cat Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct Cat (CatW c1) (CatW c2) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
type BinaryProduct Cat (CatW c1) (CatW c2) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
type Exponential Cat (CatW c) (CatW d) Source # 
Instance details

Defined in Data.Category.CartesianClosed

type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)

data CatW :: (* -> * -> *) -> * Source #

We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.

Instances
type BinaryCoproduct Cat (CatW c1) (CatW c2) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
type BinaryProduct Cat (CatW c1) (CatW c2) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
type Exponential Cat (CatW c) (CatW d) Source # 
Instance details

Defined in Data.Category.CartesianClosed

type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)

Functors

class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where Source #

Functors map objects and arrows.

Associated Types

type Dom ftag :: * -> * -> * Source #

The domain, or source category, of the functor.

type Cod ftag :: * -> * -> * Source #

The codomain, or target category, of the functor.

type ftag :% a :: * infixr 9 Source #

:% maps objects.

Methods

(%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b) infixr 9 Source #

% maps arrows.

Instances
Functor Add Source #

Ordinal addition is a bifuntor, it concattenates the maps as it were.

Instance details

Defined in Data.Category.Simplex

Associated Types

type Dom Add :: Type -> Type -> Type Source #

type Cod Add :: Type -> Type -> Type Source #

type Add :% a :: Type Source #

Methods

(%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b) Source #

Functor Forget Source #

Turn Simplex x y arrows into Fin x -> Fin y functions.

Instance details

Defined in Data.Category.Simplex

Associated Types

type Dom Forget :: Type -> Type -> Type Source #

type Cod Forget :: Type -> Type -> Type Source #

type Forget :% a :: Type Source #

Methods

(%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) Source #

Functor Add Source #

Ordinal addition is a bifuntor, it concattenates the maps as it were.

Instance details

Defined in Data.Category.Cube

Associated Types

type Dom Add :: Type -> Type -> Type Source #

type Cod Add :: Type -> Type -> Type Source #

type Add :% a :: Type Source #

Methods

(%) :: Add -> Dom Add a b -> Cod Add (Add :% a) (Add :% b) Source #

Functor Forget Source #

Turn Cube x y arrows into ACube x -> ACube y functions.

Instance details

Defined in Data.Category.Cube

Associated Types

type Dom Forget :: Type -> Type -> Type Source #

type Cod Forget :: Type -> Type -> Type Source #

type Forget :% a :: Type Source #

Methods

(%) :: Forget -> Dom Forget a b -> Cod Forget (Forget :% a) (Forget :% b) Source #

Functor M1 Source # 
Instance details

Defined in Data.Category.Yoneda

Associated Types

type Dom M1 :: Type -> Type -> Type Source #

type Cod M1 :: Type -> Type -> Type Source #

type M1 :% a :: Type Source #

Methods

(%) :: M1 -> Dom M1 a b -> Cod M1 (M1 :% a) (M1 :% b) Source #

Category k => Functor (Hom k) Source #

The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Hom k) :: Type -> Type -> Type Source #

type Cod (Hom k) :: Type -> Type -> Type Source #

type (Hom k) :% a :: Type Source #

Methods

(%) :: Hom k -> Dom (Hom k) a b -> Cod (Hom k) (Hom k :% a) (Hom k :% b) Source #

Category k => Functor (DiagProd k) Source #

DiagProd is the diagonal functor for products.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (DiagProd k) :: Type -> Type -> Type Source #

type Cod (DiagProd k) :: Type -> Type -> Type Source #

type (DiagProd k) :% a :: Type Source #

Methods

(%) :: DiagProd k -> Dom (DiagProd k) a b -> Cod (DiagProd k) (DiagProd k :% a) (DiagProd k :% b) Source #

Category k => Functor (OpOpInv k) Source #

The x = Op (Op x) functor.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (OpOpInv k) :: Type -> Type -> Type Source #

type Cod (OpOpInv k) :: Type -> Type -> Type Source #

type (OpOpInv k) :% a :: Type Source #

Methods

(%) :: OpOpInv k -> Dom (OpOpInv k) a b -> Cod (OpOpInv k) (OpOpInv k :% a) (OpOpInv k :% b) Source #

Category k => Functor (OpOp k) Source #

The Op (Op x) = x functor.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (OpOp k) :: Type -> Type -> Type Source #

type Cod (OpOp k) :: Type -> Type -> Type Source #

type (OpOp k) :% a :: Type Source #

Methods

(%) :: OpOp k -> Dom (OpOp k) a b -> Cod (OpOp k) (OpOp k :% a) (OpOp k :% b) Source #

(Category (Dom f), Category (Cod f)) => Functor (Opposite f) Source #

The dual of a functor

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Opposite f) :: Type -> Type -> Type Source #

type Cod (Opposite f) :: Type -> Type -> Type Source #

type (Opposite f) :% a :: Type Source #

Methods

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

Category k => Functor (Id k) Source #

The identity functor on k

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Id k) :: Type -> Type -> Type Source #

type Cod (Id k) :: Type -> Type -> Type Source #

type (Id k) :% a :: Type Source #

Methods

(%) :: Id k -> Dom (Id k) a b -> Cod (Id k) (Id k :% a) (Id k :% b) Source #

Category k => Functor (CodiagCoprod k) Source #

CodiagCoprod is the codiagonal functor for coproducts.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (CodiagCoprod k) :: Type -> Type -> Type Source #

type Cod (CodiagCoprod k) :: Type -> Type -> Type Source #

type (CodiagCoprod k) :% a :: Type Source #

Category k => Functor (Magic k) Source #

Since there is nothing to map in Void, there's a functor from it to any other category.

Instance details

Defined in Data.Category.Void

Associated Types

type Dom (Magic k) :: Type -> Type -> Type Source #

type Cod (Magic k) :: Type -> Type -> Type Source #

type (Magic k) :% a :: Type Source #

Methods

(%) :: Magic k -> Dom (Magic k) a b -> Cod (Magic k) (Magic k :% a) (Magic k :% b) Source #

HasBinaryCoproducts k => Functor (CoproductFunctor k) Source #

Binary coproduct as a bifunctor.

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (CoproductFunctor k) :: Type -> Type -> Type Source #

type Cod (CoproductFunctor k) :: Type -> Type -> Type Source #

type (CoproductFunctor k) :% a :: Type Source #

HasBinaryProducts k => Functor (ProductFunctor k) Source #

Binary product as a bifunctor.

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (ProductFunctor k) :: Type -> Type -> Type Source #

type Cod (ProductFunctor k) :: Type -> Type -> Type Source #

type (ProductFunctor k) :% a :: Type Source #

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) Source # 
Instance details

Defined in Data.Category.Kleisli

Associated Types

type Dom (KleisliAdjG m) :: Type -> Type -> Type Source #

type Cod (KleisliAdjG m) :: Type -> Type -> Type Source #

type (KleisliAdjG m) :% a :: Type Source #

Methods

(%) :: KleisliAdjG m -> Dom (KleisliAdjG m) a b -> Cod (KleisliAdjG m) (KleisliAdjG m :% a) (KleisliAdjG m :% b) Source #

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) Source # 
Instance details

Defined in Data.Category.Kleisli

Associated Types

type Dom (KleisliAdjF m) :: Type -> Type -> Type Source #

type Cod (KleisliAdjF m) :: Type -> Type -> Type Source #

type (KleisliAdjF m) :% a :: Type Source #

Methods

(%) :: KleisliAdjF m -> Dom (KleisliAdjF m) a b -> Cod (KleisliAdjF m) (KleisliAdjF m :% a) (KleisliAdjF m :% b) Source #

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) Source #

ForgetAlg m is the forgetful functor for Alg m.

Instance details

Defined in Data.Category.Dialg

Associated Types

type Dom (ForgetAlg m) :: Type -> Type -> Type Source #

type Cod (ForgetAlg m) :: Type -> Type -> Type Source #

type (ForgetAlg m) :% a :: Type Source #

Methods

(%) :: ForgetAlg m -> Dom (ForgetAlg m) a b -> Cod (ForgetAlg m) (ForgetAlg m :% a) (ForgetAlg m :% b) Source #

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) Source #

FreeAlg M takes x to the free algebra (M x, mu_x) of the monad M.

Instance details

Defined in Data.Category.Dialg

Associated Types

type Dom (FreeAlg m) :: Type -> Type -> Type Source #

type Cod (FreeAlg m) :: Type -> Type -> Type Source #

type (FreeAlg m) :% a :: Type Source #

Methods

(%) :: FreeAlg m -> Dom (FreeAlg m) a b -> Cod (FreeAlg m) (FreeAlg m :% a) (FreeAlg m :% b) Source #

CartesianClosed k => Functor (ExpFunctor k) Source #

The exponential as a bifunctor.

Instance details

Defined in Data.Category.CartesianClosed

Associated Types

type Dom (ExpFunctor k) :: Type -> Type -> Type Source #

type Cod (ExpFunctor k) :: Type -> Type -> Type Source #

type (ExpFunctor k) :% a :: Type Source #

Methods

(%) :: ExpFunctor k -> Dom (ExpFunctor k) a b -> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b) 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 #

EFunctor f => Functor (UnderlyingF f) Source #

The underlying functor of an enriched functor f

Instance details

Defined in Data.Category.Enriched

Associated Types

type Dom (UnderlyingF f) :: Type -> Type -> Type Source #

type Cod (UnderlyingF f) :: Type -> Type -> Type Source #

type (UnderlyingF f) :% a :: Type Source #

Methods

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

(Functor f1, Functor f2) => Functor (f1 :***: f2) Source #

f1 :***: f2 is the product of the functors f1 and f2.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (f1 :***: f2) :: Type -> Type -> Type Source #

type Cod (f1 :***: f2) :: Type -> Type -> Type Source #

type (f1 :***: f2) :% a :: Type Source #

Methods

(%) :: (f1 :***: f2) -> Dom (f1 :***: f2) a b -> Cod (f1 :***: f2) ((f1 :***: f2) :% a) ((f1 :***: f2) :% b) Source #

(Category c1, Category c2) => Functor (Proj2 c1 c2) Source #

Proj2 is a bifunctor that projects out the second component of a product.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Proj2 c1 c2) :: Type -> Type -> Type Source #

type Cod (Proj2 c1 c2) :: Type -> Type -> Type Source #

type (Proj2 c1 c2) :% a :: Type Source #

Methods

(%) :: Proj2 c1 c2 -> Dom (Proj2 c1 c2) a b -> Cod (Proj2 c1 c2) (Proj2 c1 c2 :% a) (Proj2 c1 c2 :% b) Source #

(Category c1, Category c2) => Functor (Proj1 c1 c2) Source #

Proj1 is a bifunctor that projects out the first component of a product.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Proj1 c1 c2) :: Type -> Type -> Type Source #

type Cod (Proj1 c1 c2) :: Type -> Type -> Type Source #

type (Proj1 c1 c2) :% a :: Type Source #

Methods

(%) :: Proj1 c1 c2 -> Dom (Proj1 c1 c2) a b -> Cod (Proj1 c1 c2) (Proj1 c1 c2 :% a) (Proj1 c1 c2 :% b) Source #

(Category (Cod g), Category (Dom h)) => Functor (g :.: h) Source #

The composition of two functors.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (g :.: h) :: Type -> Type -> Type Source #

type Cod (g :.: h) :: Type -> Type -> Type Source #

type (g :.: h) :% a :: Type Source #

Methods

(%) :: (g :.: h) -> Dom (g :.: h) a b -> Cod (g :.: h) ((g :.: h) :% a) ((g :.: h) :% b) Source #

(Category c1, Category c2) => Functor (Tuple c1 c2) Source #

Tuple converts an object a to the functor Tuple1 a.

Instance details

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (Tuple c1 c2) :: Type -> Type -> Type Source #

type Cod (Tuple c1 c2) :: Type -> Type -> Type Source #

type (Tuple c1 c2) :% a :: Type Source #

Methods

(%) :: Tuple c1 c2 -> Dom (Tuple c1 c2) a b -> Cod (Tuple c1 c2) (Tuple c1 c2 :% a) (Tuple c1 c2 :% b) Source #

(Category c1, Category c2) => Functor (Apply c1 c2) Source #

Apply is a bifunctor, Apply :% (f, a) applies f to a, i.e. f :% a.

Instance details

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (Apply c1 c2) :: Type -> Type -> Type Source #

type Cod (Apply c1 c2) :: Type -> Type -> Type Source #

type (Apply c1 c2) :% a :: Type Source #

Methods

(%) :: Apply c1 c2 -> Dom (Apply c1 c2) a b -> Cod (Apply c1 c2) (Apply c1 c2 :% a) (Apply c1 c2 :% b) Source #

(Functor f, Functor h) => Functor (Wrap f h) Source #

Wrap f h is the functor such that Wrap f h :% g = f :.: g :.: h, for functors g that compose with f and h.

Instance details

Defined in Data.Category.NaturalTransformation

Associated Types

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

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

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

Methods

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

(Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) Source #

A natural transformation Nat c d is isomorphic to a functor from c :**: 2 to d.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (NatAsFunctor f g) :: Type -> Type -> Type Source #

type Cod (NatAsFunctor f g) :: Type -> Type -> Type Source #

type (NatAsFunctor f g) :% a :: Type Source #

Methods

(%) :: NatAsFunctor f g -> Dom (NatAsFunctor f g) a b -> Cod (NatAsFunctor f g) (NatAsFunctor f g :% a) (NatAsFunctor f g :% b) Source #

(Functor f1, Functor f2) => Functor (f1 :+++: f2) Source #

f1 :+++: f2 is the coproduct of the functors f1 and f2.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (f1 :+++: f2) :: Type -> Type -> Type Source #

type Cod (f1 :+++: f2) :: Type -> Type -> Type Source #

type (f1 :+++: f2) :% a :: Type Source #

Methods

(%) :: (f1 :+++: f2) -> Dom (f1 :+++: f2) a b -> Cod (f1 :+++: f2) ((f1 :+++: f2) :% a) ((f1 :+++: f2) :% b) Source #

(Category c1, Category c2) => Functor (Inj2 c1 c2) Source #

Inj2 is a functor which injects into the right category.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Inj2 c1 c2) :: Type -> Type -> Type Source #

type Cod (Inj2 c1 c2) :: Type -> Type -> Type Source #

type (Inj2 c1 c2) :% a :: Type Source #

Methods

(%) :: Inj2 c1 c2 -> Dom (Inj2 c1 c2) a b -> Cod (Inj2 c1 c2) (Inj2 c1 c2 :% a) (Inj2 c1 c2 :% b) Source #

(Category c1, Category c2) => Functor (Inj1 c1 c2) Source #

Inj1 is a functor which injects into the left category.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Inj1 c1 c2) :: Type -> Type -> Type Source #

type Cod (Inj1 c1 c2) :: Type -> Type -> Type Source #

type (Inj1 c1 c2) :% a :: Type Source #

Methods

(%) :: Inj1 c1 c2 -> Dom (Inj1 c1 c2) a b -> Cod (Inj1 c1 c2) (Inj1 c1 c2 :% a) (Inj1 c1 c2 :% b) Source #

(Category (Dom p), Category (Cod p)) => Functor (p :+: q) Source #

The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (p :+: q) :: Type -> Type -> Type Source #

type Cod (p :+: q) :: Type -> Type -> Type Source #

type (p :+: q) :% a :: Type Source #

Methods

(%) :: (p :+: q) -> Dom (p :+: q) a b -> Cod (p :+: q) ((p :+: q) :% a) ((p :+: q) :% b) Source #

(Category (Dom p), Category (Cod p)) => Functor (p :*: q) Source #

The product of two functors, passing the same object to both functors and taking the product of the results.

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (p :*: q) :: Type -> Type -> Type Source #

type Cod (p :*: q) :: Type -> Type -> Type Source #

type (p :*: q) :% a :: Type Source #

Methods

(%) :: (p :*: q) -> Dom (p :*: q) a b -> Cod (p :*: q) ((p :*: q) :% a) ((p :*: q) :% b) Source #

HasColimits j k => Functor (ColimitFunctor j k) Source #

If every diagram of type j has a colimit in k there exists a colimit functor. It can be seen as a generalisation of (+++).

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (ColimitFunctor j k) :: Type -> Type -> Type Source #

type Cod (ColimitFunctor j k) :: Type -> Type -> Type Source #

type (ColimitFunctor j k) :% a :: Type Source #

Methods

(%) :: ColimitFunctor j k -> Dom (ColimitFunctor j k) a b -> Cod (ColimitFunctor j k) (ColimitFunctor j k :% a) (ColimitFunctor j k :% b) Source #

HasLimits j k => Functor (LimitFunctor j k) Source #

If every diagram of type j has a limit in k there exists a limit functor. It can be seen as a generalisation of (***).

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (LimitFunctor j k) :: Type -> Type -> Type Source #

type Cod (LimitFunctor j k) :: Type -> Type -> Type Source #

type (LimitFunctor j k) :% a :: Type Source #

Methods

(%) :: LimitFunctor j k -> Dom (LimitFunctor j k) a b -> Cod (LimitFunctor j k) (LimitFunctor j k :% a) (LimitFunctor j k :% b) Source #

(Category j, Category k) => Functor (Diag j k) Source #

The diagonal functor from (index-) category J to k.

Instance details

Defined in Data.Category.Limit

Associated Types

type Dom (Diag j k) :: Type -> Type -> Type Source #

type Cod (Diag j k) :: Type -> Type -> Type Source #

type (Diag j k) :% a :: Type Source #

Methods

(%) :: Diag j k -> Dom (Diag j k) a b -> Cod (Diag j k) (Diag j k :% a) (Diag j k :% b) Source #

TensorProduct f => Functor (Replicate f a) Source #

Replicate a monoid a number of times.

Instance details

Defined in Data.Category.Simplex

Associated Types

type Dom (Replicate f a) :: Type -> Type -> Type Source #

type Cod (Replicate f a) :: Type -> Type -> Type Source #

type (Replicate f a) :% a :: Type Source #

Methods

(%) :: Replicate f a -> Dom (Replicate f a) a0 b -> Cod (Replicate f a) (Replicate f a :% a0) (Replicate f a :% b) Source #

(Category k, Functor f, Dom f ~ Op k, Cod f ~ ((->) :: Type -> Type -> Type)) => Functor (Yoneda k f) Source #

Yoneda converts a functor f into a natural transformation from the hom functor to f.

Instance details

Defined in Data.Category.Yoneda

Associated Types

type Dom (Yoneda k f) :: Type -> Type -> Type Source #

type Cod (Yoneda k f) :: Type -> Type -> Type Source #

type (Yoneda k f) :% a :: Type Source #

Methods

(%) :: Yoneda k f -> Dom (Yoneda k f) a b -> Cod (Yoneda k f) (Yoneda k f :% a) (Yoneda k f :% b) Source #

(Category c1, Category c2) => Functor (Const c1 c2 x) Source #

The constant functor.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Const c1 c2 x) :: Type -> Type -> Type Source #

type Cod (Const c1 c2 x) :: Type -> Type -> Type Source #

type (Const c1 c2 x) :% a :: Type Source #

Methods

(%) :: Const c1 c2 x -> Dom (Const c1 c2 x) a b -> Cod (Const c1 c2 x) (Const c1 c2 x :% a) (Const c1 c2 x :% b) Source #

(Category c, Category d, Category e) => Functor (FunctorCompose c d e) Source #

Composition of functors is a functor.

Instance details

Defined in Data.Category.NaturalTransformation

Associated Types

type Dom (FunctorCompose c d e) :: Type -> Type -> Type Source #

type Cod (FunctorCompose c d e) :: Type -> Type -> Type Source #

type (FunctorCompose c d e) :% a :: Type Source #

Methods

(%) :: FunctorCompose c d e -> Dom (FunctorCompose c d e) a b -> Cod (FunctorCompose c d e) (FunctorCompose c d e :% a) (FunctorCompose c d e :% b) Source #

(Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) Source #

Cotuple2 projects out to the right category, replacing a value from the left category with a fixed object.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Cotuple2 c1 c2 a2) :: Type -> Type -> Type Source #

type Cod (Cotuple2 c1 c2 a2) :: Type -> Type -> Type Source #

type (Cotuple2 c1 c2 a2) :% a :: Type Source #

Methods

(%) :: Cotuple2 c1 c2 a2 -> Dom (Cotuple2 c1 c2 a2) a b -> Cod (Cotuple2 c1 c2 a2) (Cotuple2 c1 c2 a2 :% a) (Cotuple2 c1 c2 a2 :% b) Source #

(Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) Source #

Cotuple1 projects out to the left category, replacing a value from the right category with a fixed object.

Instance details

Defined in Data.Category.Coproduct

Associated Types

type Dom (Cotuple1 c1 c2 a1) :: Type -> Type -> Type Source #

type Cod (Cotuple1 c1 c2 a1) :: Type -> Type -> Type Source #

type (Cotuple1 c1 c2 a1) :% a :: Type Source #

Methods

(%) :: Cotuple1 c1 c2 a1 -> Dom (Cotuple1 c1 c2 a1) a b -> Cod (Cotuple1 c1 c2 a1) (Cotuple1 c1 c2 a1 :% a) (Cotuple1 c1 c2 a1 :% b) Source #

Category k => Functor (Arrow k a b) Source #

Any functor from the Boolean category points to an arrow in its target category.

Instance details

Defined in Data.Category.Boolean

Associated Types

type Dom (Arrow k a b) :: Type -> Type -> Type Source #

type Cod (Arrow k a b) :: Type -> Type -> Type Source #

type (Arrow k a b) :% a :: Type Source #

Methods

(%) :: Arrow k a b -> Dom (Arrow k a b) a0 b0 -> Cod (Arrow k a b) (Arrow k a b :% a0) (Arrow k a b :% b0) Source #

type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b) Source #

Functor instances

data Id (k :: * -> * -> *) Source #

Constructors

Id 
Instances
Category k => Functor (Id k) Source #

The identity functor on k

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Id k) :: Type -> Type -> Type Source #

type Cod (Id k) :: Type -> Type -> Type Source #

type (Id k) :% a :: Type Source #

Methods

(%) :: Id k -> Dom (Id k) a b -> Cod (Id k) (Id k :% a) (Id k :% b) Source #

HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source #

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

Instance details

Defined in Data.Category.Dialg

Associated Types

type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type Source #

Methods

initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source #

initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source #

type Dom (Id k) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (Id k) = k
type Cod (Id k) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (Id k) = k
type (Id k) :% a Source # 
Instance details

Defined in Data.Category.Functor

type (Id k) :% a = a
type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source # 
Instance details

Defined in Data.Category.Dialg

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) = NatNum

data g :.: h where Source #

Constructors

(:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h 
Instances
(Category (Cod g), Category (Dom h)) => Functor (g :.: h) Source #

The composition of two functors.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (g :.: h) :: Type -> Type -> Type Source #

type Cod (g :.: h) :: Type -> Type -> Type Source #

type (g :.: h) :% a :: Type Source #

Methods

(%) :: (g :.: h) -> Dom (g :.: h) a b -> Cod (g :.: h) ((g :.: h) :% a) ((g :.: h) :% b) Source #

HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source #

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

Instance details

Defined in Data.Category.Dialg

Associated Types

type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type Source #

Methods

initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source #

initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a 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 (g :.: h) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (g :.: h) = Dom h
type Cod (g :.: h) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (g :.: h) = Cod g
type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source # 
Instance details

Defined in Data.Category.Dialg

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) = NatNum
type Unit (WrapTensor (Fix f) t) Source # 
Instance details

Defined in Data.Category.Fix

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

Defined in Data.Category.Functor

type (g :.: h) :% a = g :% (h :% a)

data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where Source #

Constructors

Const :: Obj c2 x -> Const c1 c2 x 
Instances
HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source #

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

Instance details

Defined in Data.Category.Dialg

Associated Types

type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type Source #

Methods

initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source #

initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source #

(Category c1, Category c2) => Functor (Const c1 c2 x) Source #

The constant functor.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Const c1 c2 x) :: Type -> Type -> Type Source #

type Cod (Const c1 c2 x) :: Type -> Type -> Type Source #

type (Const c1 c2 x) :% a :: Type Source #

Methods

(%) :: Const c1 c2 x -> Dom (Const c1 c2 x) a b -> Cod (Const c1 c2 x) (Const c1 c2 x :% a) (Const c1 c2 x :% b) Source #

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source # 
Instance details

Defined in Data.Category.Dialg

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) = NatNum
type Dom (Const c1 c2 x) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (Const c1 c2 x) = c1
type Cod (Const c1 c2 x) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (Const c1 c2 x) = c2
type (Const c1 c2 x) :% a Source # 
Instance details

Defined in Data.Category.Functor

type (Const c1 c2 x) :% a = x

type ConstF f = Const (Dom f) (Cod f) Source #

The constant functor with the same domain and codomain as f.

data Opposite f where Source #

Constructors

Opposite :: Functor f => f -> Opposite f 
Instances
(Category (Dom f), Category (Cod f)) => Functor (Opposite f) Source #

The dual of a functor

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Opposite f) :: Type -> Type -> Type Source #

type Cod (Opposite f) :: Type -> Type -> Type Source #

type (Opposite f) :% a :: Type Source #

Methods

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

type Dom (Opposite f) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (Opposite f) = Op (Dom f)
type Cod (Opposite f) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (Opposite f) = Op (Cod f)
type (Opposite f) :% a Source # 
Instance details

Defined in Data.Category.Functor

type (Opposite f) :% a = f :% a

data OpOp (k :: * -> * -> *) Source #

Constructors

OpOp 
Instances
Category k => Functor (OpOp k) Source #

The Op (Op x) = x functor.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (OpOp k) :: Type -> Type -> Type Source #

type Cod (OpOp k) :: Type -> Type -> Type Source #

type (OpOp k) :% a :: Type Source #

Methods

(%) :: OpOp k -> Dom (OpOp k) a b -> Cod (OpOp k) (OpOp k :% a) (OpOp k :% b) Source #

type Dom (OpOp k) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (OpOp k) = Op (Op k)
type Cod (OpOp k) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (OpOp k) = k
type (OpOp k) :% a Source # 
Instance details

Defined in Data.Category.Functor

type (OpOp k) :% a = a

data OpOpInv (k :: * -> * -> *) Source #

Constructors

OpOpInv 
Instances
Category k => Functor (OpOpInv k) Source #

The x = Op (Op x) functor.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (OpOpInv k) :: Type -> Type -> Type Source #

type Cod (OpOpInv k) :: Type -> Type -> Type Source #

type (OpOpInv k) :% a :: Type Source #

Methods

(%) :: OpOpInv k -> Dom (OpOpInv k) a b -> Cod (OpOpInv k) (OpOpInv k :% a) (OpOpInv k :% b) Source #

type Dom (OpOpInv k) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (OpOpInv k) = k
type Cod (OpOpInv k) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (OpOpInv k) = Op (Op k)
type (OpOpInv k) :% a Source # 
Instance details

Defined in Data.Category.Functor

type (OpOpInv k) :% a = a

Related to the product category

data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) Source #

Constructors

Proj1 
Instances
(Category c1, Category c2) => Functor (Proj1 c1 c2) Source #

Proj1 is a bifunctor that projects out the first component of a product.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Proj1 c1 c2) :: Type -> Type -> Type Source #

type Cod (Proj1 c1 c2) :: Type -> Type -> Type Source #

type (Proj1 c1 c2) :% a :: Type Source #

Methods

(%) :: Proj1 c1 c2 -> Dom (Proj1 c1 c2) a b -> Cod (Proj1 c1 c2) (Proj1 c1 c2 :% a) (Proj1 c1 c2 :% b) Source #

type Dom (Proj1 c1 c2) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (Proj1 c1 c2) = c1 :**: c2
type Cod (Proj1 c1 c2) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (Proj1 c1 c2) = c1
type (Proj1 c1 c2) :% (a1, a2) Source # 
Instance details

Defined in Data.Category.Functor

type (Proj1 c1 c2) :% (a1, a2) = a1

data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) Source #

Constructors

Proj2 
Instances
(Category c1, Category c2) => Functor (Proj2 c1 c2) Source #

Proj2 is a bifunctor that projects out the second component of a product.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Proj2 c1 c2) :: Type -> Type -> Type Source #

type Cod (Proj2 c1 c2) :: Type -> Type -> Type Source #

type (Proj2 c1 c2) :% a :: Type Source #

Methods

(%) :: Proj2 c1 c2 -> Dom (Proj2 c1 c2) a b -> Cod (Proj2 c1 c2) (Proj2 c1 c2 :% a) (Proj2 c1 c2 :% b) Source #

type Dom (Proj2 c1 c2) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (Proj2 c1 c2) = c1 :**: c2
type Cod (Proj2 c1 c2) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (Proj2 c1 c2) = c2
type (Proj2 c1 c2) :% (a1, a2) Source # 
Instance details

Defined in Data.Category.Functor

type (Proj2 c1 c2) :% (a1, a2) = a2

data f1 :***: f2 where Source #

Constructors

(:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2 
Instances
(Functor f1, Functor f2) => Functor (f1 :***: f2) Source #

f1 :***: f2 is the product of the functors f1 and f2.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (f1 :***: f2) :: Type -> Type -> Type Source #

type Cod (f1 :***: f2) :: Type -> Type -> Type Source #

type (f1 :***: f2) :% a :: Type Source #

Methods

(%) :: (f1 :***: f2) -> Dom (f1 :***: f2) a b -> Cod (f1 :***: f2) ((f1 :***: f2) :% a) ((f1 :***: f2) :% b) Source #

HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source #

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

Instance details

Defined in Data.Category.Dialg

Associated Types

type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type Source #

Methods

initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source #

initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a 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 (f1 :***: f2) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (f1 :***: f2) = Dom f1 :**: Dom f2
type Cod (f1 :***: f2) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (f1 :***: f2) = Cod f1 :**: Cod f2
type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source # 
Instance details

Defined in Data.Category.Dialg

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) = NatNum
type Unit (WrapTensor (Fix f) t) Source # 
Instance details

Defined in Data.Category.Fix

type Unit (WrapTensor (Fix f) t) = Unit t
type (f1 :***: f2) :% (a1, a2) Source # 
Instance details

Defined in Data.Category.Functor

type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)

data DiagProd (k :: * -> * -> *) Source #

Constructors

DiagProd 
Instances
Category k => Functor (DiagProd k) Source #

DiagProd is the diagonal functor for products.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (DiagProd k) :: Type -> Type -> Type Source #

type Cod (DiagProd k) :: Type -> Type -> Type Source #

type (DiagProd k) :% a :: Type Source #

Methods

(%) :: DiagProd k -> Dom (DiagProd k) a b -> Cod (DiagProd k) (DiagProd k :% a) (DiagProd k :% b) Source #

HasInitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source #

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

Instance details

Defined in Data.Category.Dialg

Associated Types

type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) :: Type Source #

Methods

initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source #

initialize :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source #

type Dom (DiagProd k) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (DiagProd k) = k
type Cod (DiagProd k) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (DiagProd k) = k :**: k
type (DiagProd k) :% a Source # 
Instance details

Defined in Data.Category.Functor

type (DiagProd k) :% a = (a, a)
type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) Source # 
Instance details

Defined in Data.Category.Dialg

type InitialObject (Dialg (Tuple1 ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) ()) (DiagProd ((->) :: Type -> Type -> Type))) = NatNum

type Tuple1 c1 c2 a = (Const c2 c1 a :***: Id c2) :.: DiagProd c2 Source #

pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a Source #

Tuple1 tuples with a fixed object on the left.

type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a Source #

pattern Tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a Source #

Tuple2 tuples with a fixed object on the right.

type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2) Source #

pattern Swap :: (Category c1, Category c2) => Swap c1 c2 Source #

swap swaps the 2 categories of the product of categories.

Hom functors

data Hom (k :: * -> * -> *) Source #

Constructors

Hom 
Instances
Category k => Functor (Hom k) Source #

The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.

Instance details

Defined in Data.Category.Functor

Associated Types

type Dom (Hom k) :: Type -> Type -> Type Source #

type Cod (Hom k) :: Type -> Type -> Type Source #

type (Hom k) :% a :: Type Source #

Methods

(%) :: Hom k -> Dom (Hom k) a b -> Cod (Hom k) (Hom k :% a) (Hom k :% b) Source #

type Dom (Hom k) Source # 
Instance details

Defined in Data.Category.Functor

type Dom (Hom k) = Op k :**: k
type Cod (Hom k) Source # 
Instance details

Defined in Data.Category.Functor

type Cod (Hom k) = ((->) :: Type -> Type -> Type)
type (Hom k) :% (a1, a2) Source # 
Instance details

Defined in Data.Category.Functor

type (Hom k) :% (a1, a2) = k a1 a2

type (:*-:) x k = Hom k :.: Tuple1 (Op k) k x Source #

pattern HomX_ :: Category k => Obj k x -> x :*-: k Source #

The covariant functor Hom(X,--)

type (:-*:) k x = Hom k :.: Tuple2 (Op k) k x Source #

pattern Hom_X :: Category k => Obj k x -> k :-*: x Source #

The contravariant functor Hom(--,X)

type HomF f g = Hom (Cod f) :.: (Opposite f :***: g) Source #

pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g Source #

type Star f = HomF (Id (Cod f)) f Source #

pattern Star :: Functor f => f -> Star f Source #

type Costar f = HomF f (Id (Cod f)) Source #

pattern Costar :: Functor f => f -> Costar f Source #