Data.Category.Functor

Cat

data Cat :: * -> * -> * where

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

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

Defined in Data.Category.Functor

Methods

src :: Cat a b -> Obj Cat a

tgt :: Cat a b -> Obj Cat b

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

HasBinaryCoproducts Cat

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

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct Cat x y :: Type

Methods

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

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

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

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

HasBinaryProducts Cat

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

Defined in Data.Category.Limit

Associated Types

type BinaryProduct Cat x y :: Type

Methods

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

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

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

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

HasInitialObject Cat

The empty category is the initial object in Cat.

Defined in Data.Category.Limit

Associated Types

type InitialObject Cat :: Type

Methods

initialObject :: Obj Cat (InitialObject Cat)

initialize :: Obj Cat a -> Cat (InitialObject Cat) a

HasTerminalObject Cat

Unit is the terminal category.

Defined in Data.Category.Limit

Associated Types

type TerminalObject Cat :: Type

Methods

terminalObject :: Obj Cat (TerminalObject Cat)

terminate :: Obj Cat a -> Cat a (TerminalObject Cat)

CartesianClosed Cat

Exponentials in Cat are the functor categories.

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential Cat y z :: Type

Methods

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

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

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

type InitialObject Cat

Defined in Data.Category.Limit

type InitialObject Cat = CatW Void

type TerminalObject Cat

Defined in Data.Category.Limit

type TerminalObject Cat = CatW Unit

type BinaryCoproduct Cat (CatW c1) (CatW c2)

Defined in Data.Category.Limit

type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)

type BinaryProduct Cat (CatW c1) (CatW c2)

Defined in Data.Category.Limit

type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)

type Exponential Cat (CatW c) (CatW d)

Defined in Data.Category.CartesianClosed

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

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

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)

Defined in Data.Category.Limit

type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)

type BinaryProduct Cat (CatW c1) (CatW c2)

Defined in Data.Category.Limit

type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)

type Exponential Cat (CatW c) (CatW d)

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

Functors map objects and arrows.

Associated Types

type Dom ftag :: * -> * -> *

The domain, or source category, of the functor.

type Cod ftag :: * -> * -> *

The codomain, or target category, of the functor.

type ftag :% a :: * infixr 9

:% maps objects.

Methods

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

% maps arrows.

Instances

Functor Add

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

Defined in Data.Category.Simplex

Associated Types

type Dom Add :: Type -> Type -> Type

type Cod Add :: Type -> Type -> Type

type Add :% a :: Type

Methods

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

Functor Forget

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

Defined in Data.Category.Simplex

Associated Types

type Dom Forget :: Type -> Type -> Type

type Cod Forget :: Type -> Type -> Type

type Forget :% a :: Type

Methods

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

Functor Add

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

Defined in Data.Category.Cube

Associated Types

type Dom Add :: Type -> Type -> Type

type Cod Add :: Type -> Type -> Type

type Add :% a :: Type

Methods

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

Functor Forget

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

Defined in Data.Category.Cube

Associated Types

type Dom Forget :: Type -> Type -> Type

type Cod Forget :: Type -> Type -> Type

type Forget :% a :: Type

Methods

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

Functor M1

Defined in Data.Category.Yoneda

Associated Types

type Dom M1 :: Type -> Type -> Type

type Cod M1 :: Type -> Type -> Type

type M1 :% a :: Type

Methods

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

Category k => Functor (Hom k)

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

Defined in Data.Category.Functor

Associated Types

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

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

type (Hom k) :% a :: Type

Methods

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

Category k => Functor (DiagProd k)

DiagProd is the diagonal functor for products.

Defined in Data.Category.Functor

Associated Types

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

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

type (DiagProd k) :% a :: Type

Methods

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

Category k => Functor (OpOpInv k)

The x = Op (Op x) functor.

Defined in Data.Category.Functor

Associated Types

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

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

type (OpOpInv k) :% a :: Type

Methods

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

Category k => Functor (OpOp k)

The Op (Op x) = x functor.

Defined in Data.Category.Functor

Associated Types

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

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

type (OpOp k) :% a :: Type

Methods

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

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

The dual of a functor

Defined in Data.Category.Functor

Associated Types

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

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

type (Opposite f) :% a :: Type

Methods

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

Category k => Functor (Id k)

The identity functor on k

Defined in Data.Category.Functor

Associated Types

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

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

type (Id k) :% a :: Type

Methods

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

Category k => Functor (CodiagCoprod k)

CodiagCoprod is the codiagonal functor for coproducts.

Defined in Data.Category.Coproduct

Associated Types

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

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

type (CodiagCoprod k) :% a :: Type

Methods

(%) :: CodiagCoprod k -> Dom (CodiagCoprod k) a b -> Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b)

Category k => Functor (Magic k)

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

Defined in Data.Category.Void

Associated Types

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

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

type (Magic k) :% a :: Type

Methods

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

HasBinaryCoproducts k => Functor (CoproductFunctor k)

Binary coproduct as a bifunctor.

Defined in Data.Category.Limit

Associated Types

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

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

type (CoproductFunctor k) :% a :: Type

Methods

(%) :: CoproductFunctor k -> Dom (CoproductFunctor k) a b -> Cod (CoproductFunctor k) (CoproductFunctor k :% a) (CoproductFunctor k :% b)

HasBinaryProducts k => Functor (ProductFunctor k)

Binary product as a bifunctor.

Defined in Data.Category.Limit

Associated Types

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

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

type (ProductFunctor k) :% a :: Type

Methods

(%) :: ProductFunctor k -> Dom (ProductFunctor k) a b -> Cod (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b)

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m)

Defined in Data.Category.Kleisli

Associated Types

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

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

type (KleisliAdjG m) :% a :: Type

Methods

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

(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m)

Defined in Data.Category.Kleisli

Associated Types

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

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

type (KleisliAdjF m) :% a :: Type

Methods

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

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

ForgetAlg m is the forgetful functor for Alg m.

Defined in Data.Category.Dialg

Associated Types

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

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

type (ForgetAlg m) :% a :: Type

Methods

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

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

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

Defined in Data.Category.Dialg

Associated Types

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

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

type (FreeAlg m) :% a :: Type

Methods

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

CartesianClosed k => Functor (ExpFunctor k)

The exponential as a bifunctor.

Defined in Data.Category.CartesianClosed

Associated Types

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

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

type (ExpFunctor k) :% a :: Type

Methods

(%) :: ExpFunctor k -> Dom (ExpFunctor k) a b -> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b)

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

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

Defined in Data.Category.Fix

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Fix

Associated Types

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

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

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

Methods

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

EFunctor f => Functor (UnderlyingF f)

The underlying functor of an enriched functor f

Defined in Data.Category.Enriched

Associated Types

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

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

type (UnderlyingF f) :% a :: Type

Methods

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

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

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

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

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

The composition of two functors.

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

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

Tuple converts an object a to the functor Tuple1 a.

Defined in Data.Category.NaturalTransformation

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.NaturalTransformation

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.NaturalTransformation

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Coproduct

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Coproduct

Associated Types

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

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

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

Methods

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

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

Inj2 is a functor which injects into the right category.

Defined in Data.Category.Coproduct

Associated Types

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

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

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

Methods

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

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

Inj1 is a functor which injects into the left category.

Defined in Data.Category.Coproduct

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Limit

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Limit

Associated Types

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

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

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

Methods

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

HasColimits j k => Functor (ColimitFunctor j k)

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

Defined in Data.Category.Limit

Associated Types

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

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

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

Methods

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

HasLimits j k => Functor (LimitFunctor j k)

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

Defined in Data.Category.Limit

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Limit

Associated Types

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

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

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

Methods

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

TensorProduct f => Functor (Replicate f a)

Replicate a monoid a number of times.

Defined in Data.Category.Simplex

Associated Types

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

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

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

Methods

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

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

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

Defined in Data.Category.Yoneda

Associated Types

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

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

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

Methods

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

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

The constant functor.

Defined in Data.Category.Functor

Associated Types

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

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

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

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)

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

Composition of functors is a functor.

Defined in Data.Category.NaturalTransformation

Associated Types

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

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

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

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)

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

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

Defined in Data.Category.Coproduct

Associated Types

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

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

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

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)

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

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

Defined in Data.Category.Coproduct

Associated Types

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

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

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

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)

Category k => Functor (Arrow k a b)

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

Defined in Data.Category.Boolean

Associated Types

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

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

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

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)

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

Functor instances

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

Constructors

Id

Instances

Category k => Functor (Id k)

The identity functor on k

Defined in Data.Category.Functor

Associated Types

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

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

type (Id k) :% a :: Type

Methods

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

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

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>.

Defined in Data.Category.Dialg

Associated Types

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

Methods

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

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

type Dom (Id k)

Defined in Data.Category.Functor

type Dom (Id k) = k

type Cod (Id k)

Defined in Data.Category.Functor

type Cod (Id k) = k

type (Id k) :% a

Defined in Data.Category.Functor

type (Id k) :% a = a

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

Defined in Data.Category.Dialg

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

data g :.: h where

Constructors

(:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h

Instances

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

The composition of two functors.

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

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

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>.

Defined in Data.Category.Dialg

Associated Types

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

Methods

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

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

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

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

Defined in Data.Category.Fix

Associated Types

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

Methods

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

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

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))

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

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)))

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)))

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))

type Dom (g :.: h)

Defined in Data.Category.Functor

type Dom (g :.: h) = Dom h

type Cod (g :.: h)

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)))

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)

Defined in Data.Category.Fix

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

type (g :.: h) :% a

Defined in Data.Category.Functor

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

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

Constructors

Const :: Obj c2 x -> Const c1 c2 x

Instances

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

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>.

Defined in Data.Category.Dialg

Associated Types

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

Methods

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

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

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

The constant functor.

Defined in Data.Category.Functor

Associated Types

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

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

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

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)

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

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)

Defined in Data.Category.Functor

type Dom (Const c1 c2 x) = c1

type Cod (Const c1 c2 x)

Defined in Data.Category.Functor

type Cod (Const c1 c2 x) = c2

type (Const c1 c2 x) :% a

Defined in Data.Category.Functor

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

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

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

data Opposite f where

Constructors

Opposite :: Functor f => f -> Opposite f

Instances

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

The dual of a functor

Defined in Data.Category.Functor

Associated Types

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

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

type (Opposite f) :% a :: Type

Methods

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

type Dom (Opposite f)

Defined in Data.Category.Functor

type Dom (Opposite f) = Op (Dom f)

type Cod (Opposite f)

Defined in Data.Category.Functor

type Cod (Opposite f) = Op (Cod f)

type (Opposite f) :% a

Defined in Data.Category.Functor

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

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

Constructors

OpOp

Instances

Category k => Functor (OpOp k)

The Op (Op x) = x functor.

Defined in Data.Category.Functor

Associated Types

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

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

type (OpOp k) :% a :: Type

Methods

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

type Dom (OpOp k)

Defined in Data.Category.Functor

type Dom (OpOp k) = Op (Op k)

type Cod (OpOp k)

Defined in Data.Category.Functor

type Cod (OpOp k) = k

type (OpOp k) :% a

Defined in Data.Category.Functor

type (OpOp k) :% a = a

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

Constructors

OpOpInv

Instances

Category k => Functor (OpOpInv k)

The x = Op (Op x) functor.

Defined in Data.Category.Functor

Associated Types

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

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

type (OpOpInv k) :% a :: Type

Methods

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

type Dom (OpOpInv k)

Defined in Data.Category.Functor

type Dom (OpOpInv k) = k

type Cod (OpOpInv k)

Defined in Data.Category.Functor

type Cod (OpOpInv k) = Op (Op k)

type (OpOpInv k) :% a

Defined in Data.Category.Functor

type (OpOpInv k) :% a = a

Related to the product category

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

Constructors

Proj1

Instances

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

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

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

type Dom (Proj1 c1 c2)

Defined in Data.Category.Functor

type Dom (Proj1 c1 c2) = c1 :**: c2

type Cod (Proj1 c1 c2)

Defined in Data.Category.Functor

type Cod (Proj1 c1 c2) = c1

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

Defined in Data.Category.Functor

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

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

Constructors

Proj2

Instances

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

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

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

type Dom (Proj2 c1 c2)

Defined in Data.Category.Functor

type Dom (Proj2 c1 c2) = c1 :**: c2

type Cod (Proj2 c1 c2)

Defined in Data.Category.Functor

type Cod (Proj2 c1 c2) = c2

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

Defined in Data.Category.Functor

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

data f1 :***: f2 where

Constructors

(:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2

Instances

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

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

Defined in Data.Category.Functor

Associated Types

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

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

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

Methods

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

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

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>.

Defined in Data.Category.Dialg

Associated Types

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

Methods

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

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

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

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

Defined in Data.Category.Fix

Associated Types

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

Methods

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

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

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))

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

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)))

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)))

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))

type Dom (f1 :***: f2)

Defined in Data.Category.Functor

type Dom (f1 :***: f2) = Dom f1 :**: Dom f2

type Cod (f1 :***: f2)

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)))

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)

Defined in Data.Category.Fix

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

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

Defined in Data.Category.Functor

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

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

Constructors

DiagProd

Instances

Category k => Functor (DiagProd k)

DiagProd is the diagonal functor for products.

Defined in Data.Category.Functor

Associated Types

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

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

type (DiagProd k) :% a :: Type

Methods

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

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

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>.

Defined in Data.Category.Dialg

Associated Types

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

Methods

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

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

type Dom (DiagProd k)

Defined in Data.Category.Functor

type Dom (DiagProd k) = k

type Cod (DiagProd k)

Defined in Data.Category.Functor

type Cod (DiagProd k) = k :**: k

type (DiagProd k) :% a

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)))

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

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

Tuple1 tuples with a fixed object on the left.

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

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

Tuple2 tuples with a fixed object on the right.

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

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

swap swaps the 2 categories of the product of categories.

Hom functors

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

Constructors

Hom

Instances

Category k => Functor (Hom k)

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

Defined in Data.Category.Functor

Associated Types

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

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

type (Hom k) :% a :: Type

Methods

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

type Dom (Hom k)

Defined in Data.Category.Functor

type Dom (Hom k) = Op k :**: k

type Cod (Hom k)

Defined in Data.Category.Functor

type Cod (Hom k) = ((->) :: Type -> Type -> Type)

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

Defined in Data.Category.Functor

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

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

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

The covariant functor Hom(X,--)

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

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

The contravariant functor Hom(--,X)

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

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

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

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

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

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