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

Data.Category.NaturalTransformation

Contents

Natural transformations
Functor category
Functor isomorphisms
Related functors

Description

Synopsis

type (:~>) f g = forall c d. (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
type Component f g z = Cod f (f :% z) (g :% z)
(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)
o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
pattern NatId :: () => (Functor f, c ~ Dom f, d ~ Cod f) => f -> Nat c d f f
srcF :: Nat c d f g -> f
tgtF :: Nat c d f g -> g
data Nat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
- Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
type Endo k = Nat k k
type Presheaves k = Nat (Op k) (->)
type Profunctors c d = Nat (Op d :**: c) (->)
compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
data FunctorCompose (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) (e :: Type -> Type -> Type) = FunctorCompose
type EndoFunctorCompose k = FunctorCompose k k k
type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f
pattern Precompose :: (Category e, Functor f) => f -> Precompose f e
type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f
pattern Postcompose :: (Category c, Functor f) => f -> Postcompose f c
type Curry1 c1 c2 f = Postcompose f c2 :.: Tuple c1 c2
pattern Curry1 :: (Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) => f -> Curry1 c1 c2 f
type Curry2 c1 c2 f = Postcompose f c1 :.: Curry1 c2 c1 (Swap c2 c1)
pattern Curry2 :: (Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) => f -> Curry2 c1 c2 f
data Wrap f h = Wrap f h
data Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Apply
data Tuple (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Tuple
data Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Opp
type Opposite f = Opp (Dom f) (Cod f) :.: Tuple1 (Op (Nat (Dom f) (Cod f))) (Op (Dom f)) f
pattern Opposite :: Functor f => f -> Opposite f
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
type (:*%:) x f = (x :*-: Cod f) :.: f
pattern HomXF :: Functor f => Obj (Cod f) x -> f -> x :*%: f
type (:%*:) f x = (Cod f :-*: x) :.: Opposite f
pattern HomFX :: Functor f => f -> Obj (Cod f) x -> f :%*: x

Natural transformations

type (:~>) f g = forall c d. (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g Source #

f :~> g is a natural transformation from functor f to functor g.

type Component f g z = Cod f (f :% z) (g :% z) Source #

A component for an object z is an arrow from F z to G z.

(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b) infixl 9 Source #

'n ! a' returns the component for the object a of a natural transformation n. This can be generalized to any arrow (instead of just identity arrows).

o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g) Source #

Horizontal composition of natural transformations.

natId :: Functor f => f -> Nat (Dom f) (Cod f) f f Source #

The identity natural transformation of a functor.

pattern NatId :: () => (Functor f, c ~ Dom f, d ~ Cod f) => f -> Nat c d f f Source #

srcF :: Nat c d f g -> f Source #

tgtF :: Nat c d f g -> g Source #

Functor category

data Nat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where Source #

Natural transformations are built up of components, one for each object z in the domain category of f and g.

Constructors

Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g

Instances

Instances details

Category k => CartesianClosed (Presheaves k :: Type -> Type -> Type) Source #	The category of presheaves on a category `C` is cartesian closed for any `C`.
Instance details Defined in Data.Category.CartesianClosed Associated Types type Exponential (Presheaves k) y z :: Kind k Source # Methods apply :: forall (y :: k0) (z :: k0). Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k (BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y) z Source # tuple :: forall (y :: k0) (z :: k0). Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k z (Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y)) Source # (^^^) :: forall (z1 :: k0) (z2 :: k0) (y2 :: k0) (y1 :: k0). Presheaves k z1 z2 -> Presheaves k y2 y1 -> Presheaves k (Exponential (Presheaves k) y1 z1) (Exponential (Presheaves k) y2 z2) Source #
Category d => Category (Nat c d :: Type -> Type -> Type) Source #	Functor category D^C. Objects of D^C are functors from C to D. Arrows of D^C are natural transformations.
Instance details Defined in Data.Category.NaturalTransformation Methods src :: forall (a :: k) (b :: k). Nat c d a b -> Obj (Nat c d) a Source # tgt :: forall (a :: k) (b :: k). Nat c d a b -> Obj (Nat c d) b Source # (.) :: forall (b :: k) (c0 :: k) (a :: k). Nat c d b c0 -> Nat c d a b -> Nat c d a c0 Source #
(Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d :: Type -> Type -> Type) Source #	The functor coproduct `:+:` is the binary coproduct in functor categories.
Instance details Defined in Data.Category.Limit Associated Types type BinaryCoproduct (Nat c d) x y :: Kind k Source # Methods inj1 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d x (BinaryCoproduct (Nat c d) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d y (BinaryCoproduct (Nat c d) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). Nat c d x a -> Nat c d y a -> Nat c d (BinaryCoproduct (Nat c d) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Nat c d a1 b1 -> Nat c d a2 b2 -> Nat c d (BinaryCoproduct (Nat c d) a1 a2) (BinaryCoproduct (Nat c d) b1 b2) Source #
(Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d :: Type -> Type -> Type) Source #	The functor product `:*:` is the binary product in functor categories.
Instance details Defined in Data.Category.Limit Associated Types type BinaryProduct (Nat c d) x y :: Kind k Source # Methods proj1 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (Nat c d) x -> Obj (Nat c d) y -> Nat c d (BinaryProduct (Nat c d) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). Nat c d a x -> Nat c d a y -> Nat c d a (BinaryProduct (Nat c d) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Nat c d a1 b1 -> Nat c d a2 b2 -> Nat c d (BinaryProduct (Nat c d) a1 a2) (BinaryProduct (Nat c d) b1 b2) Source #
(Category c, HasInitialObject d) => HasInitialObject (Nat c d :: Type -> Type -> Type) Source #	The constant functor to the initial object is itself the initial object in its functor category.
Instance details Defined in Data.Category.Limit Associated Types type InitialObject (Nat c d) :: Kind k Source # Methods initialObject :: Obj (Nat c d) (InitialObject (Nat c d)) Source # initialize :: forall (a :: k). Obj (Nat c d) a -> Nat c d (InitialObject (Nat c d)) a Source #
(Category c, HasTerminalObject d) => HasTerminalObject (Nat c d :: Type -> Type -> Type) Source #	The constant functor to the terminal object is itself the terminal object in its functor category.
Instance details Defined in Data.Category.Limit Associated Types type TerminalObject (Nat c d) :: Kind k Source # Methods terminalObject :: Obj (Nat c d) (TerminalObject (Nat c d)) Source # terminate :: forall (a :: k). Obj (Nat c d) a -> Nat c d a (TerminalObject (Nat c d)) Source #
type Exponential (Presheaves k :: Type -> Type -> Type) (y :: Kind (Nat (Op k) (->))) (z :: Kind (Nat (Op k) (->))) Source #
Instance details Defined in Data.Category.CartesianClosed type Exponential (Presheaves k :: Type -> Type -> Type) (y :: Kind (Nat (Op k) (->))) (z :: Kind (Nat (Op k) (->))) = PShExponential k y z
type InitialObject (Nat c d :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Limit type InitialObject (Nat c d :: Type -> Type -> Type) = Const c d (InitialObject d)
type TerminalObject (Nat c d :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Limit type TerminalObject (Nat c d :: Type -> Type -> Type) = Const c d (TerminalObject d)
type BinaryCoproduct (Nat c d :: Type -> Type -> Type) (x :: Kind (Nat c d)) (y :: Kind (Nat c d)) Source #
Instance details Defined in Data.Category.Limit type BinaryCoproduct (Nat c d :: Type -> Type -> Type) (x :: Kind (Nat c d)) (y :: Kind (Nat c d)) = x :+: y
type BinaryProduct (Nat c d :: Type -> Type -> Type) (x :: Kind (Nat c d)) (y :: Kind (Nat c d)) Source #
Instance details Defined in Data.Category.Limit type BinaryProduct (Nat c d :: Type -> Type -> Type) (x :: Kind (Nat c d)) (y :: Kind (Nat c d)) = x :*: y

type Endo k = Nat k k Source #

The category of endofunctors.

type Presheaves k = Nat (Op k) (->) Source #

type Profunctors c d = Nat (Op d :**: c) (->) Source #

Functor isomorphisms

compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h)) Source #

compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h) Source #

idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f Source #

idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f)) Source #

idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f Source #

idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f) Source #

constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g Source #

constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x)) Source #

constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g Source #

constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x) Source #

Related functors

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

Constructors

FunctorCompose

Instances

Instances details

Category k => TensorProduct (EndoFunctorCompose k) Source #	Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
Instance details Defined in Data.Category.Monoidal Associated Types type Unit (EndoFunctorCompose k) :: Kind (Cod f) Source # Methods unitObject :: EndoFunctorCompose k -> Obj (Cod (EndoFunctorCompose k)) (Unit (EndoFunctorCompose k)) Source # leftUnitor :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) a Source # leftUnitorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 a (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) Source # rightUnitor :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) a Source # rightUnitorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 a (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) Source # associator :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c)) (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c))) Source # associatorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c))) (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c)) 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 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 #
type Unit (EndoFunctorCompose k) Source #
Instance details Defined in Data.Category.Monoidal type Unit (EndoFunctorCompose k) = Id k
type Cod (FunctorCompose c d e) Source #
Instance details Defined in Data.Category.NaturalTransformation type Cod (FunctorCompose c d e) = Nat c e
type Dom (FunctorCompose c d e) Source #
Instance details Defined in Data.Category.NaturalTransformation type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d
type (FunctorCompose c d e) :% (f, g) Source #
Instance details Defined in Data.Category.NaturalTransformation type (FunctorCompose c d e) :% (f, g) = f :.: g

type EndoFunctorCompose k = FunctorCompose k k k Source #

Composition of endofunctors is a functor.

type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f Source #

Precompose f e is the functor such that Precompose f e :% g = g :.: f, for functors g that compose with f and with codomain e.

pattern Precompose :: (Category e, Functor f) => f -> Precompose f e Source #

type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f Source #

Postcompose f c is the functor such that Postcompose f c :% g = f :.: g, for functors g that compose with f and with domain c.

pattern Postcompose :: (Category c, Functor f) => f -> Postcompose f c Source #

type Curry1 c1 c2 f = Postcompose f c2 :.: Tuple c1 c2 Source #

pattern Curry1 :: (Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) => f -> Curry1 c1 c2 f Source #

Curry on the first "argument" of a functor from a product category.

type Curry2 c1 c2 f = Postcompose f c1 :.: Curry1 c2 c1 (Swap c2 c1) Source #

pattern Curry2 :: (Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) => f -> Curry2 c1 c2 f Source #

Curry on the second "argument" of a functor from a product category.

data Wrap f h Source #

Constructors

Wrap f h

Instances

Instances details

(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 Source # Methods (%) :: Wrap f h -> Dom (Wrap f h) a b -> Cod (Wrap f h) (Wrap f h :% a) (Wrap f h :% b) Source #
type Cod (Wrap f h) Source #
Instance details Defined in Data.Category.NaturalTransformation type Cod (Wrap f h) = Nat (Dom h) (Cod f)
type Dom (Wrap f h) Source #
Instance details Defined in Data.Category.NaturalTransformation type Dom (Wrap f h) = Nat (Cod h) (Dom f)
type (Wrap f h) :% g Source #
Instance details Defined in Data.Category.NaturalTransformation type (Wrap f h) :% g = (f :.: g) :.: h

data Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #

Constructors

Apply

Instances

Instances details

(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 Source # Methods (%) :: Apply c1 c2 -> Dom (Apply c1 c2) a b -> Cod (Apply c1 c2) (Apply c1 c2 :% a) (Apply c1 c2 :% b) Source #
type Cod (Apply c1 c2) Source #
Instance details Defined in Data.Category.NaturalTransformation type Cod (Apply c1 c2) = c1
type Dom (Apply c1 c2) Source #
Instance details Defined in Data.Category.NaturalTransformation type Dom (Apply c1 c2) = Nat c2 c1 :**: c2
type (Apply c1 c2) :% (f, a) Source #
Instance details Defined in Data.Category.NaturalTransformation type (Apply c1 c2) :% (f, a) = f :% a

data Tuple (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #

Constructors

Tuple

Instances

Instances details

(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 Source # Methods (%) :: Tuple c1 c2 -> Dom (Tuple c1 c2) a b -> Cod (Tuple c1 c2) (Tuple c1 c2 :% a) (Tuple c1 c2 :% b) Source #
type Cod (Tuple c1 c2) Source #
Instance details Defined in Data.Category.NaturalTransformation type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)
type Dom (Tuple c1 c2) Source #
Instance details Defined in Data.Category.NaturalTransformation type Dom (Tuple c1 c2) = c1
type (Tuple c1 c2) :% a Source #
Instance details Defined in Data.Category.NaturalTransformation type (Tuple c1 c2) :% a = Tuple1 c1 c2 a

data Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #

Constructors

Opp

Instances

Instances details

(Category c1, Category c2) => Functor (Opp c1 c2) Source #	Turning a functor into its dual is contravariantly functorial.
Instance details Defined in Data.Category.NaturalTransformation Associated Types type Dom (Opp c1 c2) :: Type -> Type -> Type Source # type Cod (Opp c1 c2) :: Type -> Type -> Type Source # type (Opp c1 c2) :% a Source # Methods (%) :: Opp c1 c2 -> Dom (Opp c1 c2) a b -> Cod (Opp c1 c2) (Opp c1 c2 :% a) (Opp c1 c2 :% b) Source #
type Cod (Opp c1 c2) Source #
Instance details Defined in Data.Category.NaturalTransformation type Cod (Opp c1 c2) = Op c2
type Dom (Opp c1 c2) Source #
Instance details Defined in Data.Category.NaturalTransformation type Dom (Opp c1 c2) = Op (Nat c1 c2) :**: Op c1
type (Opp c1 c2) :% (f, a) Source #
Instance details Defined in Data.Category.NaturalTransformation type (Opp c1 c2) :% (f, a) = f :% a

type Opposite f = Opp (Dom f) (Cod f) :.: Tuple1 (Op (Nat (Dom f) (Cod f))) (Op (Dom f)) f Source #

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

The dual of a functor

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 #

type (:*%:) x f = (x :*-: Cod f) :.: f Source #

pattern HomXF :: Functor f => Obj (Cod f) x -> f -> x :*%: f Source #

The covariant functor Hom(X,F-)

type (:%*:) f x = (Cod f :-*: x) :.: Opposite f Source #

pattern HomFX :: Functor f => f -> Obj (Cod f) x -> f :%*: x Source #

The contravariant functor Hom(F-,X)