License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Category.Functor

Contents

Cat
Functors
- Functor instances
  - Related to the product category
  - Hom functors

Description

Synopsis

data Cat :: (* -> * -> *) -> (* -> * -> *) -> * where
- CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag)
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
- type Dom ftag :: * -> * -> *
- type Cod ftag :: * -> * -> *
- type ftag :% a :: *
- (%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)
data Id (k :: * -> * -> *) = Id
data g :.: h where
- (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
- Const :: Obj c2 x -> Const c1 c2 x
type ConstF f = Const (Dom f) (Cod f)
data Opposite f where
- Opposite :: Functor f => f -> Opposite f
data OpOp (k :: * -> * -> *) = OpOp
data OpOpInv (k :: * -> * -> *) = OpOpInv
newtype Any f = Any f
data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
data f1 :***: f2 where
- (:***:) :: (Functor f1, Functor f2) => f1 -> f2 -> f1 :***: f2
data DiagProd (k :: * -> * -> *) = DiagProd
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
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
type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
pattern Swap :: (Category c1, Category c2) => Swap c1 c2
data Hom (k :: * -> * -> *) = Hom
type (:*-:) x k = Hom k :.: Tuple1 (Op k) k x
pattern HomX_ :: Category k => Obj k x -> x :*-: k
type (:-*:) k x = Hom k :.: Tuple2 (Op k) k x
pattern Hom_X :: Category k => Obj k x -> k :-*: 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

Cat

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

Functors are arrows in the category Cat.

Constructors

CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (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 :: Kind k 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 :: Kind k 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 :: Kind k Source # Methods initialObject :: Obj Cat (InitialObject Cat) Source # initialize :: Obj Cat a -> Cat (InitialObject Cat) a Source #
HasTerminalObject Cat Source #	`Unit` is the terminal category.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject Cat :: Kind k Source # Methods terminalObject :: Obj Cat (TerminalObject Cat) Source # terminate :: Obj Cat a -> Cat a (TerminalObject Cat) 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 :: Kind k 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 InitialObject Cat = Void
type TerminalObject Cat Source #
Instance details Defined in Data.Category.Limit type TerminalObject Cat = Unit
type BinaryCoproduct Cat (c1 :: Kind Cat) (c2 :: Kind Cat) Source #
Instance details Defined in Data.Category.Limit type BinaryCoproduct Cat (c1 :: Kind Cat) (c2 :: Kind Cat) = c1 :++: c2
type BinaryProduct Cat (c1 :: Kind Cat) (c2 :: Kind Cat) Source #
Instance details Defined in Data.Category.Limit type BinaryProduct Cat (c1 :: Kind Cat) (c2 :: Kind Cat) = c1 :**: c2
type Exponential Cat (c :: Kind Cat) (d :: Kind Cat) Source #
Instance details Defined in Data.Category.CartesianClosed type Exponential Cat (c :: Kind Cat) (d :: Kind Cat) = 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 #
Functor f => Functor (Any f) Source #
Instance details Defined in Data.Category.Functor Associated Types type Dom (Any f) :: Type -> Type -> Type Source # type Cod (Any f) :: Type -> Type -> Type Source # type (Any f) :% a :: Type Source # Methods (%) :: Any f -> Dom (Any f) a b -> Cod (Any f) (Any f :% a) (Any f :% 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 # Methods (%) :: CodiagCoprod k -> Dom (CodiagCoprod k) a b -> Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b) 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 # Methods (%) :: CoproductFunctor k -> Dom (CoproductFunctor k) a b -> Cod (CoproductFunctor k) (CoproductFunctor k :% a) (CoproductFunctor k :% b) 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 # Methods (%) :: ProductFunctor k -> Dom (ProductFunctor k) a b -> Cod (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b) Source #
(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliForget m) Source #
Instance details Defined in Data.Category.Kleisli Associated Types type Dom (KleisliForget m) :: Type -> Type -> Type Source # type Cod (KleisliForget m) :: Type -> Type -> Type Source # type (KleisliForget m) :% a :: Type Source # Methods (%) :: KleisliForget m -> Dom (KleisliForget m) a b -> Cod (KleisliForget m) (KleisliForget m :% a) (KleisliForget m :% b) Source #
(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliFree m) Source #
Instance details Defined in Data.Category.Kleisli Associated Types type Dom (KleisliFree m) :: Type -> Type -> Type Source # type Cod (KleisliFree m) :: Type -> Type -> Type Source # type (KleisliFree m) :% a :: Type Source # Methods (%) :: KleisliFree m -> Dom (KleisliFree m) a b -> Cod (KleisliFree m) (KleisliFree m :% a) (KleisliFree 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 #
HasInitialObject k => Functor (Initializer k) Source #	`Initializer k` is the functor that sends an object to its initializing arrow.
Instance details Defined in Data.Category.Boolean Associated Types type Dom (Initializer k) :: Type -> Type -> Type Source # type Cod (Initializer k) :: Type -> Type -> Type Source # type (Initializer k) :% a :: Type Source # Methods (%) :: Initializer k -> Dom (Initializer k) a b -> Cod (Initializer k) (Initializer k :% a) (Initializer k :% b) Source #
HasTerminalObject k => Functor (Terminator k) Source #	`Terminator k` is the functor that sends an object to its terminating arrow.
Instance details Defined in Data.Category.Boolean Associated Types type Dom (Terminator k) :: Type -> Type -> Type Source # type Cod (Terminator k) :: Type -> Type -> Type Source # type (Terminator k) :% a :: Type Source # Methods (%) :: Terminator k -> Dom (Terminator k) a b -> Cod (Terminator k) (Terminator k :% a) (Terminator k :% 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 #
Functor p => Functor (LanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (LanHaskF p f) :: Type -> Type -> Type Source # type Cod (LanHaskF p f) :: Type -> Type -> Type Source # type (LanHaskF p f) :% a :: Type Source # Methods (%) :: LanHaskF p f -> Dom (LanHaskF p f) a b -> Cod (LanHaskF p f) (LanHaskF p f :% a) (LanHaskF p f :% b) Source #
Functor p => Functor (RanHaskF p f) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (RanHaskF p f) :: Type -> Type -> Type Source # type Cod (RanHaskF p f) :: Type -> Type -> Type Source # type (RanHaskF p f) :% a :: Type Source # Methods (%) :: RanHaskF p f -> Dom (RanHaskF p f) a b -> Cod (RanHaskF p f) (RanHaskF p f :% a) (RanHaskF p f :% b) Source #
HasLeftKan p k => Functor (LanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (LanFunctor p k) :: Type -> Type -> Type Source # type Cod (LanFunctor p k) :: Type -> Type -> Type Source # type (LanFunctor p k) :% a :: Type Source # Methods (%) :: LanFunctor p k -> Dom (LanFunctor p k) a b -> Cod (LanFunctor p k) (LanFunctor p k :% a) (LanFunctor p k :% b) Source #
HasRightKan p k => Functor (RanFunctor p k) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type Dom (RanFunctor p k) :: Type -> Type -> Type Source # type Cod (RanFunctor p k) :: Type -> Type -> Type Source # type (RanFunctor p k) :% a :: Type Source # Methods (%) :: RanFunctor p k -> Dom (RanFunctor p k) a b -> Cod (RanFunctor p k) (RanFunctor p k :% a) (RanFunctor p k :% 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 #
(Category j, Category k) => HasLeftKan (Id j) k Source #	Lan id = id
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (Id j) k f :: Type Source # Methods lan :: Id j -> Obj (Nat (Dom (Id j)) k) f -> Nat (Dom (Id j)) k f (LanFam (Id j) k f :.: Id j) Source # lanFactorizer :: Nat (Dom (Id j)) k f (h :.: Id j) -> Nat (Cod (Id j)) k (LanFam (Id j) k f) h Source #
(Category j, Category k) => HasRightKan (Id j) k Source #	Ran id = id
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (Id j) k f :: Type Source # Methods ran :: Id j -> Obj (Nat (Dom (Id j)) k) f -> Nat (Dom (Id j)) k (RanFam (Id j) k f :.: Id j) f Source # ranFactorizer :: Nat (Dom (Id j)) k (h :.: Id j) f -> Nat (Cod (Id j)) k h (RanFam (Id j) k f) 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 (->))) :: Kind k 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 LanFam (Id j) k f Source #
Instance details Defined in Data.Category.KanExtension type LanFam (Id j) k f = f
type RanFam (Id j) k f Source #
Instance details Defined in Data.Category.KanExtension type RanFam (Id j) k f = f
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

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 (->))) :: Kind k 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 (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 #
(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 #
(HasLeftKan q k, HasLeftKan p k) => HasLeftKan (q :.: p) k Source #	Lan (q . p) = Lan q . Lan p
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (q :.: p) k f :: Type Source # Methods lan :: (q :.: p) -> Obj (Nat (Dom (q :.: p)) k) f -> Nat (Dom (q :.: p)) k f (LanFam (q :.: p) k f :.: (q :.: p)) Source # lanFactorizer :: Nat (Dom (q :.: p)) k f (h :.: (q :.: p)) -> Nat (Cod (q :.: p)) k (LanFam (q :.: p) k f) h Source #
(HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k Source #	Ran (q . p) = Ran q . Ran p
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (q :.: p) k f :: Type Source # Methods ran :: (q :.: p) -> Obj (Nat (Dom (q :.: p)) k) f -> Nat (Dom (q :.: p)) k (RanFam (q :.: p) k f :.: (q :.: p)) f Source # ranFactorizer :: Nat (Dom (q :.: p)) k (h :.: (q :.: p)) f -> Nat (Cod (q :.: p)) k h (RanFam (q :.: p) k f) 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 (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 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)
type LanFam (q :.: p) k f Source #
Instance details Defined in Data.Category.KanExtension type LanFam (q :.: p) k f = LanFam q k (LanFam p k f)
type RanFam (q :.: p) k f Source #
Instance details Defined in Data.Category.KanExtension type RanFam (q :.: p) k f = RanFam q k (RanFam p k f)

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 (->))) :: Kind k 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 #
HasColimits j k => HasLeftKan (Const j Unit ()) k Source #	The left Kan extension of `f` along a functor to the unit category is the colimit of `f`.
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (Const j Unit ()) k f :: Type Source # Methods lan :: Const j Unit () -> Obj (Nat (Dom (Const j Unit ())) k) f -> Nat (Dom (Const j Unit ())) k f (LanFam (Const j Unit ()) k f :.: Const j Unit ()) Source # lanFactorizer :: Nat (Dom (Const j Unit ())) k f (h :.: Const j Unit ()) -> Nat (Cod (Const j Unit ())) k (LanFam (Const j Unit ()) k f) h Source #
HasLimits j k => HasRightKan (Const j Unit ()) k Source #	The right Kan extension of `f` along a functor to the unit category is the limit of `f`.
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (Const j Unit ()) k f :: Type Source # Methods ran :: Const j Unit () -> Obj (Nat (Dom (Const j Unit ())) k) f -> Nat (Dom (Const j Unit ())) k (RanFam (Const j Unit ()) k f :.: Const j Unit ()) f Source # ranFactorizer :: Nat (Dom (Const j Unit ())) k (h :.: Const j Unit ()) f -> Nat (Cod (Const j Unit ())) k h (RanFam (Const j Unit ()) k f) 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 LanFam (Const j Unit ()) k f Source #
Instance details Defined in Data.Category.KanExtension type LanFam (Const j Unit ()) k f = Const Unit k (ColimitFam j k f)
type RanFam (Const j Unit ()) k f Source #
Instance details Defined in Data.Category.KanExtension type RanFam (Const j Unit ()) k f = Const Unit k (LimitFam j k f)

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

newtype Any f Source #

A functor wrapper in case of conflicting family instance declarations

Constructors

Any f

Instances

Functor f => Functor (Any f) Source #
Instance details Defined in Data.Category.Functor Associated Types type Dom (Any f) :: Type -> Type -> Type Source # type Cod (Any f) :: Type -> Type -> Type Source # type (Any f) :% a :: Type Source # Methods (%) :: Any f -> Dom (Any f) a b -> Cod (Any f) (Any f :% a) (Any f :% b) Source #
Functor p => HasLeftKan (Any p) ((->) :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type LanFam (Any p) (->) f :: Type Source # Methods lan :: Any p -> Obj (Nat (Dom (Any p)) (->)) f -> Nat (Dom (Any p)) (->) f (LanFam (Any p) (->) f :.: Any p) Source # lanFactorizer :: Nat (Dom (Any p)) (->) f (h :.: Any p) -> Nat (Cod (Any p)) (->) (LanFam (Any p) (->) f) h Source #
Functor p => HasRightKan (Any p) ((->) :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.KanExtension Associated Types type RanFam (Any p) (->) f :: Type Source # Methods ran :: Any p -> Obj (Nat (Dom (Any p)) (->)) f -> Nat (Dom (Any p)) (->) (RanFam (Any p) (->) f :.: Any p) f Source # ranFactorizer :: Nat (Dom (Any p)) (->) (h :.: Any p) f -> Nat (Cod (Any p)) (->) h (RanFam (Any p) (->) f) Source #
type Dom (Any f) Source #
Instance details Defined in Data.Category.Functor type Dom (Any f) = Dom f
type Cod (Any f) Source #
Instance details Defined in Data.Category.Functor type Cod (Any f) = Cod f
type (Any f) :% a Source #
Instance details Defined in Data.Category.Functor type (Any f) :% a = f :% a
type LanFam (Any p) ((->) :: Type -> Type -> Type) f Source #
Instance details Defined in Data.Category.KanExtension type LanFam (Any p) ((->) :: Type -> Type -> Type) f = LanHaskF p f
type RanFam (Any p) ((->) :: Type -> Type -> Type) f Source #
Instance details Defined in Data.Category.KanExtension type RanFam (Any p) ((->) :: Type -> Type -> Type) f = RanHaskF p f

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

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 (->))) :: Kind k 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 #
(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 #
(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 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 (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 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 (->))) :: Kind k 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 #