License | BSD-style (see the file LICENSE) |
---|---|
Maintainer | sjoerd@w3future.com |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- data Cat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where
- class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
- type FunctorOf a b t = (Functor t, Dom t ~ a, Cod t ~ b)
- data Id (k :: Type -> Type -> Type) = Id
- data g :.: h where
- data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where
- type ConstF f = Const (Dom f) (Cod f)
- data OpOp (k :: Type -> Type -> Type) = OpOp
- data OpOpInv (k :: Type -> Type -> Type) = OpOpInv
- newtype Any f = Any f
- data Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj1
- data Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Proj2
- data f1 :***: f2 where
- data DiagProd (k :: Type -> Type -> Type) = 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 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
- pattern Swap :: (Category c1, Category c2) => Swap c1 c2
- data Hom (k :: Type -> Type -> Type) = 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 ProfunctorOf c d t = (FunctorOf (Op c :**: d) (->) t, Category c, Category d)
Cat
data Cat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type where Source #
Functors are arrows in the category Cat.
CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (Dom ftag) (Cod ftag) |
Instances
Category Cat Source # |
|
CartesianClosed Cat Source # | Exponentials in |
Defined in Data.Category.CartesianClosed type Exponential Cat y z :: Kind k Source # apply :: forall (y :: k) (z :: k). Obj Cat y -> Obj Cat z -> Cat (BinaryProduct Cat (Exponential Cat y z) y) z Source # tuple :: forall (y :: k) (z :: k). Obj Cat y -> Obj Cat z -> Cat z (Exponential Cat y (BinaryProduct Cat z y)) Source # (^^^) :: forall (z1 :: k) (z2 :: k) (y2 :: k) (y1 :: k). Cat z1 z2 -> Cat y2 y1 -> Cat (Exponential Cat y1 z1) (Exponential Cat y2 z2) Source # | |
HasBinaryCoproducts Cat Source # | The coproduct of categories |
Defined in Data.Category.Limit type BinaryCoproduct Cat x y :: Kind k Source # inj1 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat x (BinaryCoproduct Cat x y) Source # inj2 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat y (BinaryCoproduct Cat x y) Source # (|||) :: forall (x :: k) (a :: k) (y :: k). Cat x a -> Cat y a -> Cat (BinaryCoproduct Cat x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). Cat a1 b1 -> Cat a2 b2 -> Cat (BinaryCoproduct Cat a1 a2) (BinaryCoproduct Cat b1 b2) Source # | |
HasBinaryProducts Cat Source # | The product of categories |
Defined in Data.Category.Limit type BinaryProduct Cat x y :: Kind k Source # proj1 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj Cat x -> Obj Cat y -> Cat (BinaryProduct Cat x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). Cat a x -> Cat a y -> Cat a (BinaryProduct Cat x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 |
Defined in Data.Category.Limit type InitialObject Cat :: Kind k Source # initialObject :: Obj Cat (InitialObject Cat) Source # initialize :: forall (a :: k). Obj Cat a -> Cat (InitialObject Cat) a Source # | |
HasTerminalObject Cat Source # |
|
Defined in Data.Category.Limit type TerminalObject Cat :: Kind k Source # terminalObject :: Obj Cat (TerminalObject Cat) Source # terminate :: forall (a :: k). Obj Cat a -> Cat a (TerminalObject Cat) Source # | |
type InitialObject Cat Source # | |
Defined in Data.Category.Limit | |
type TerminalObject Cat Source # | |
Defined in Data.Category.Limit | |
type Exponential Cat (c :: Kind Cat) (d :: Kind Cat) Source # | |
Defined in Data.Category.CartesianClosed | |
type BinaryCoproduct Cat (c1 :: Kind Cat) (c2 :: Kind Cat) Source # | |
Defined in Data.Category.Limit | |
type BinaryProduct Cat (c1 :: Kind Cat) (c2 :: Kind Cat) Source # | |
Defined in Data.Category.Limit |
Functors
class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where Source #
Functors map objects and arrows.
type Dom ftag :: Type -> Type -> Type Source #
The domain, or source category, of the functor.
type Cod ftag :: Type -> Type -> Type Source #
The codomain, or target category, of the functor.
type ftag :% a :: Type infixr 9 Source #
:%
maps objects.
Instances
Functor Add Source # | Ordinal addition is a bifuntor, it concattenates the maps as it were. |
Functor Forget Source # | Turn |
Functor LinearTensor Source # | |
Defined in Data.Category.Monoidal type Dom LinearTensor :: Type -> Type -> Type Source # type Cod LinearTensor :: Type -> Type -> Type Source # type LinearTensor :% a Source # (%) :: LinearTensor -> Dom LinearTensor a b -> Cod LinearTensor (LinearTensor :% a) (LinearTensor :% b) Source # | |
Functor Floor Source # | |
Functor FromInteger Source # | |
Defined in Data.Category.Preorder type Dom FromInteger :: Type -> Type -> Type Source # type Cod FromInteger :: Type -> Type -> Type Source # type FromInteger :% a Source # (%) :: FromInteger -> Dom FromInteger a b -> Cod FromInteger (FromInteger :% a) (FromInteger :% b) Source # | |
Functor Add Source # | Ordinal addition is a bifuntor, it concattenates the maps as it were. |
Functor Forget Source # | Turn |
Functor M1 Source # | |
HasInitialObject k => Functor (Initializer k) Source # |
|
Defined in Data.Category.Boolean type Dom (Initializer k) :: Type -> Type -> Type Source # type Cod (Initializer k) :: Type -> Type -> Type Source # type (Initializer k) :% a Source # (%) :: Initializer k -> Dom (Initializer k) a b -> Cod (Initializer k) (Initializer k :% a) (Initializer k :% b) Source # | |
HasTerminalObject k => Functor (Terminator k) Source # |
|
Defined in Data.Category.Boolean type Dom (Terminator k) :: Type -> Type -> Type Source # type Cod (Terminator k) :: Type -> Type -> Type Source # type (Terminator k) :% a Source # (%) :: Terminator k -> Dom (Terminator k) a b -> Cod (Terminator k) (Terminator k :% a) (Terminator k :% b) Source # | |
CartesianClosed k => Functor (ExpFunctor k) Source # | The exponential as a bifunctor. |
Defined in Data.Category.CartesianClosed type Dom (ExpFunctor k) :: Type -> Type -> Type Source # type Cod (ExpFunctor k) :: Type -> Type -> Type Source # type (ExpFunctor k) :% a Source # (%) :: ExpFunctor k -> Dom (ExpFunctor k) a b -> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b) Source # | |
Category k => Functor (IdArrow k) Source # | |
Category k => Functor (Src k) Source # | |
Category k => Functor (Tgt k) Source # | |
Category k => Functor (CodiagCoprod k) Source # |
|
Defined in Data.Category.Coproduct type Dom (CodiagCoprod k) :: Type -> Type -> Type Source # type Cod (CodiagCoprod k) :: Type -> Type -> Type Source # type (CodiagCoprod k) :% a Source # (%) :: CodiagCoprod k -> Dom (CodiagCoprod k) a b -> Cod (CodiagCoprod k) (CodiagCoprod k :% a) (CodiagCoprod k :% b) Source # | |
(Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) Source # |
|
(Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) Source # |
|
EFunctor f => Functor (UnderlyingF f) Source # | The underlying functor of an enriched functor |
Defined in Data.Category.Enriched.Functor type Dom (UnderlyingF f) :: Type -> Type -> Type Source # type Cod (UnderlyingF f) :: Type -> Type -> Type Source # type (UnderlyingF f) :% a Source # (%) :: UnderlyingF f -> Dom (UnderlyingF f) a b -> Cod (UnderlyingF f) (UnderlyingF f :% a) (UnderlyingF f :% b) Source # | |
Category (f (Fix f)) => Functor (Unwrap (Fix f)) Source # | The |
Category (f (Fix f)) => Functor (Wrap (Fix f)) Source # | |
Functor f => Functor (Any f) Source # | |
Category k => Functor (DiagProd k) Source # |
|
Category k => Functor (Hom k) Source # | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument. |
Category k => Functor (Id k) Source # | The identity functor on k |
Category k => Functor (OpOp k) Source # | The |
Category k => Functor (OpOpInv k) Source # | The |
(Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliForget m) Source # | |
Defined in Data.Category.Kleisli type Dom (KleisliForget m) :: Type -> Type -> Type Source # type Cod (KleisliForget m) :: Type -> Type -> Type Source # type (KleisliForget m) :% a Source # (%) :: 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 # | |
Defined in Data.Category.Kleisli type Dom (KleisliFree m) :: Type -> Type -> Type Source # type Cod (KleisliFree m) :: Type -> Type -> Type Source # type (KleisliFree m) :% a Source # (%) :: KleisliFree m -> Dom (KleisliFree m) a b -> Cod (KleisliFree m) (KleisliFree m :% a) (KleisliFree m :% b) Source # | |
HasBinaryCoproducts k => Functor (CoproductFunctor k) Source # | Binary coproduct as a bifunctor. |
Defined in Data.Category.Limit type Dom (CoproductFunctor k) :: Type -> Type -> Type Source # type Cod (CoproductFunctor k) :: Type -> Type -> Type Source # type (CoproductFunctor k) :% a Source # (%) :: 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. |
Defined in Data.Category.Limit type Dom (ProductFunctor k) :: Type -> Type -> Type Source # type Cod (ProductFunctor k) :: Type -> Type -> Type Source # type (ProductFunctor k) :% a Source # (%) :: ProductFunctor k -> Dom (ProductFunctor k) a b -> Cod (ProductFunctor k) (ProductFunctor k :% a) (ProductFunctor k :% b) Source # | |
TensorProduct t => Functor (Day t) Source # | |
Category k => Functor (Magic k) Source # | Since there is nothing to map in |
Category k => Functor (OpHom k) Source # | The Hom-functor but with opposite domain. |
(Functor f1, Functor f2) => Functor (f1 :+++: f2) Source # |
|
(Category c1, Category c2) => Functor (Inj1 c1 c2) Source # |
|
(Category c1, Category c2) => Functor (Inj2 c1 c2) Source # |
|
(Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) Source # | A natural transformation |
Defined in Data.Category.Coproduct type Dom (NatAsFunctor f g) :: Type -> Type -> Type Source # type Cod (NatAsFunctor f g) :: Type -> Type -> Type Source # type (NatAsFunctor f g) :% a Source # (%) :: 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 # |
|
(Category (Cod g), Category (Dom h)) => Functor (g :.: h) Source # | The composition of two functors. |
(Category c1, Category c2) => Functor (Proj1 c1 c2) Source # |
|
(Category c1, Category c2) => Functor (Proj2 c1 c2) Source # |
|
HasLeftKan p k => Functor (LanFunctor p k) Source # | |
Defined in Data.Category.KanExtension type Dom (LanFunctor p k) :: Type -> Type -> Type Source # type Cod (LanFunctor p k) :: Type -> Type -> Type Source # type (LanFunctor p k) :% a Source # (%) :: LanFunctor p k -> Dom (LanFunctor p k) a b -> Cod (LanFunctor p k) (LanFunctor p k :% a) (LanFunctor p k :% b) Source # | |
Functor p => Functor (LanHaskF p f) Source # | |
HasRightKan p k => Functor (RanFunctor p k) Source # | |
Defined in Data.Category.KanExtension type Dom (RanFunctor p k) :: Type -> Type -> Type Source # type Cod (RanFunctor p k) :: Type -> Type -> Type Source # type (RanFunctor p k) :% a Source # (%) :: RanFunctor p k -> Dom (RanFunctor p k) a b -> Cod (RanFunctor p k) (RanFunctor p k :% a) (RanFunctor p k :% b) Source # | |
Functor p => Functor (RanHaskF p f) 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. |
(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. |
HasColimits j k => Functor (ColimitFunctor j k) Source # | If every diagram of type |
Defined in Data.Category.Limit type Dom (ColimitFunctor j k) :: Type -> Type -> Type Source # type Cod (ColimitFunctor j k) :: Type -> Type -> Type Source # type (ColimitFunctor j k) :% a Source # (%) :: ColimitFunctor j k -> Dom (ColimitFunctor j k) a b -> Cod (ColimitFunctor j k) (ColimitFunctor j k :% a) (ColimitFunctor j k :% b) Source # | |
(Category j, Category k) => Functor (Diag j k) Source # | The diagonal functor from (index-) category J to k. |
HasLimits j k => Functor (LimitFunctor j k) Source # | If every diagram of type |
Defined in Data.Category.Limit type Dom (LimitFunctor j k) :: Type -> Type -> Type Source # type Cod (LimitFunctor j k) :: Type -> Type -> Type Source # type (LimitFunctor j k) :% a Source # (%) :: LimitFunctor j k -> Dom (LimitFunctor j k) a b -> Cod (LimitFunctor j k) (LimitFunctor j k :% a) (LimitFunctor j k :% b) Source # | |
(Category c1, Category c2) => Functor (Apply c1 c2) Source # |
|
(Category c1, Category c2) => Functor (Opp c1 c2) Source # | Turning a functor into its dual is contravariantly functorial. |
(Category c1, Category c2) => Functor (Tuple c1 c2) Source # | |
(Functor f, Functor h) => Functor (Wrap f h) Source # |
|
TensorProduct f => Functor (Replicate f a) Source # | Replicate a monoid a number of times. |
(HasCoends v, Category k) => Functor (CoendFunctor k v) Source # | |
Defined in Data.Category.WeightedLimit type Dom (CoendFunctor k v) :: Type -> Type -> Type Source # type Cod (CoendFunctor k v) :: Type -> Type -> Type Source # type (CoendFunctor k v) :% a Source # (%) :: CoendFunctor k v -> Dom (CoendFunctor k v) a b -> Cod (CoendFunctor k v) (CoendFunctor k v :% a) (CoendFunctor k v :% b) Source # | |
(Functor w, Category k, HasWColimits k (w :.: OpOp (Dom w))) => Functor (ColimitFunctor k w) Source # | |
Defined in Data.Category.WeightedLimit type Dom (ColimitFunctor k w) :: Type -> Type -> Type Source # type Cod (ColimitFunctor k w) :: Type -> Type -> Type Source # type (ColimitFunctor k w) :% a Source # (%) :: ColimitFunctor k w -> Dom (ColimitFunctor k w) a b -> Cod (ColimitFunctor k w) (ColimitFunctor k w :% a) (ColimitFunctor k w :% b) Source # | |
(HasEnds v, Category k) => Functor (EndFunctor k v) Source # | |
Defined in Data.Category.WeightedLimit type Dom (EndFunctor k v) :: Type -> Type -> Type Source # type Cod (EndFunctor k v) :: Type -> Type -> Type Source # type (EndFunctor k v) :% a Source # (%) :: EndFunctor k v -> Dom (EndFunctor k v) a b -> Cod (EndFunctor k v) (EndFunctor k v :% a) (EndFunctor k v :% b) Source # | |
HasWLimits k w => Functor (LimitFunctor k w) Source # | |
Defined in Data.Category.WeightedLimit type Dom (LimitFunctor k w) :: Type -> Type -> Type Source # type Cod (LimitFunctor k w) :: Type -> Type -> Type Source # type (LimitFunctor k w) :% a Source # (%) :: LimitFunctor k w -> Dom (LimitFunctor k w) a b -> Cod (LimitFunctor k w) (LimitFunctor k w :% a) (LimitFunctor k w :% b) Source # | |
(Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) Source # |
|
Category k => Functor (Arrow k a b) Source # | Any functor from the Boolean category points to an arrow in its target category. |
(Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) Source # |
|
(Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) Source # |
|
(EFunctor f, EDom f ~ InHask c, ECod f ~ InHask d, Category c, Category d) => Functor (UnderlyingHask c d f) Source # | The underlying functor of an enriched functor |
Defined in Data.Category.Enriched.Functor type Dom (UnderlyingHask c d f) :: Type -> Type -> Type Source # type Cod (UnderlyingHask c d f) :: Type -> Type -> Type Source # type (UnderlyingHask c d f) :% a Source # (%) :: UnderlyingHask c d f -> Dom (UnderlyingHask c d f) a b -> Cod (UnderlyingHask c d f) (UnderlyingHask c d f :% a) (UnderlyingHask c d f :% b) Source # | |
(Category c1, Category c2) => Functor (Const c1 c2 x) Source # | The constant functor. |
(Category c, Category d, Category e) => Functor (FunctorCompose c d e) Source # | Composition of functors is a functor. |
Defined in Data.Category.NaturalTransformation 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 # (%) :: 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 # |
Functor instances
data Id (k :: Type -> Type -> Type) Source #
Instances
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | The category for defining the natural numbers and primitive recursion can be described as
|
Defined in Data.Category.Dialg initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: forall (a :: k). Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source # | |
Category k => Functor (Id k) Source # | The identity functor on k |
(Category j, Category k) => HasLeftKan (Id j) k Source # | Lan id = id |
(Category j, Category k) => HasRightKan (Id j) k Source # | Ran id = id |
type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | |
Defined in Data.Category.Dialg | |
type Cod (Id k) Source # | |
Defined in Data.Category.Functor | |
type Dom (Id k) Source # | |
Defined in Data.Category.Functor | |
type (Id k) :% a Source # | |
Defined in Data.Category.Functor | |
type LanFam (Id j) k f Source # | |
Defined in Data.Category.KanExtension | |
type RanFam (Id j) k f Source # | |
Defined in Data.Category.KanExtension |
Instances
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | The category for defining the natural numbers and primitive recursion can be described as
|
Defined in Data.Category.Dialg initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: forall (a :: k). 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. |
(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source # |
|
Defined in Data.Category.Fix 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 |
Defined in Data.Category.KanExtension | |
(HasRightKan q k, HasRightKan p k) => HasRightKan (q :.: p) k Source # | Ran (q . p) = Ran q . Ran p |
Defined in Data.Category.KanExtension | |
type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | |
Defined in Data.Category.Dialg | |
type Cod (g :.: h) Source # | |
Defined in Data.Category.Functor | |
type Dom (g :.: h) Source # | |
Defined in Data.Category.Functor | |
type Unit (WrapTensor (Fix f) t) Source # | |
Defined in Data.Category.Fix | |
type (g :.: h) :% a Source # | |
Defined in Data.Category.Functor | |
type LanFam (q :.: p) k f Source # | |
Defined in Data.Category.KanExtension | |
type RanFam (q :.: p) k f Source # | |
Defined in Data.Category.KanExtension |
data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where Source #
Instances
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | The category for defining the natural numbers and primitive recursion can be described as
|
Defined in Data.Category.Dialg initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: forall (a :: k). Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source # | |
HasColimits j k => HasWColimits k (Const (Op j) (->) ()) Source # | Regular colimits as weigthed colimits, weighted by the constant functor to |
Defined in Data.Category.WeightedLimit type WeightedColimit k (Const (Op j) (->) ()) d Source # colimitObj :: forall (j0 :: Type -> Type -> Type) d. (FunctorOf j0 k d, Op j0 ~ Dom (Const (Op j) (->) ())) => Const (Op j) (->) () -> d -> Obj k (WColimit (Const (Op j) (->) ()) d) Source # colimit :: forall (j0 :: Type -> Type -> Type) d. (FunctorOf j0 k d, Op j0 ~ Dom (Const (Op j) (->) ())) => Const (Op j) (->) () -> d -> WeightedCocone (Const (Op j) (->) ()) d (WColimit (Const (Op j) (->) ()) d) Source # colimitFactorizer :: forall (j0 :: Type -> Type -> Type) d e. (FunctorOf j0 k d, Op j0 ~ Dom (Const (Op j) (->) ())) => Const (Op j) (->) () -> d -> Obj k e -> WeightedCocone (Const (Op j) (->) ()) d e -> k (WColimit (Const (Op j) (->) ()) d) e Source # | |
HasLimits j k => HasWLimits k (Const j (->) ()) Source # | Regular limits as weigthed limits, weighted by the constant functor to |
Defined in Data.Category.WeightedLimit type WeightedLimit k (Const j (->) ()) d Source # limitObj :: FunctorOf (Dom (Const j (->) ())) k d => Const j (->) () -> d -> Obj k (WLimit (Const j (->) ()) d) Source # limit :: FunctorOf (Dom (Const j (->) ())) k d => Const j (->) () -> d -> WeightedCone (Const j (->) ()) d (WLimit (Const j (->) ()) d) Source # limitFactorizer :: FunctorOf (Dom (Const j (->) ())) k d => Const j (->) () -> d -> Obj k e -> WeightedCone (Const j (->) ()) d e -> k e (WLimit (Const j (->) ()) d) Source # | |
(Category c1, Category c2) => Functor (Const c1 c2 x) Source # | The constant functor. |
HasColimits j k => HasLeftKan (Const j Unit ()) k Source # | The left Kan extension of |
Defined in Data.Category.KanExtension 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 |
Defined in Data.Category.KanExtension 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 (->) (->) ()) (DiagProd (->))) Source # | |
Defined in Data.Category.Dialg | |
type WeightedColimit k (Const (Op j) (->) ()) d Source # | |
Defined in Data.Category.WeightedLimit | |
type WeightedLimit k (Const j (->) ()) d Source # | |
Defined in Data.Category.WeightedLimit | |
type Cod (Const c1 c2 x) Source # | |
Defined in Data.Category.Functor | |
type Dom (Const c1 c2 x) Source # | |
Defined in Data.Category.Functor | |
type (Const c1 c2 x) :% a Source # | |
Defined in Data.Category.Functor | |
type LanFam (Const j Unit ()) k f Source # | |
Defined in Data.Category.KanExtension | |
type RanFam (Const j Unit ()) k f Source # | |
type ConstF f = Const (Dom f) (Cod f) Source #
The constant functor with the same domain and codomain as f.
A functor wrapper in case of conflicting family instance declarations
Any f |
Instances
Functor f => Functor (Any f) Source # | |
Functor p => HasLeftKan (Any p) (->) Source # | |
Defined in Data.Category.KanExtension | |
Functor p => HasRightKan (Any p) (->) Source # | |
Defined in Data.Category.KanExtension | |
type Cod (Any f) Source # | |
Defined in Data.Category.Functor | |
type Dom (Any f) Source # | |
Defined in Data.Category.Functor | |
type (Any f) :% a Source # | |
Defined in Data.Category.Functor | |
type LanFam (Any p) (->) f Source # | |
Defined in Data.Category.KanExtension | |
type RanFam (Any p) (->) f Source # | |
Defined in Data.Category.KanExtension |
Related to the product category
data Proj1 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #
Instances
(Category c1, Category c2) => Functor (Proj1 c1 c2) Source # |
|
type Cod (Proj1 c1 c2) Source # | |
Defined in Data.Category.Functor | |
type Dom (Proj1 c1 c2) Source # | |
Defined in Data.Category.Functor | |
type (Proj1 c1 c2) :% (a1, a2) Source # | |
Defined in Data.Category.Functor |
data Proj2 (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) Source #
Instances
(Category c1, Category c2) => Functor (Proj2 c1 c2) Source # |
|
type Cod (Proj2 c1 c2) Source # | |
Defined in Data.Category.Functor | |
type Dom (Proj2 c1 c2) Source # | |
Defined in Data.Category.Functor | |
type (Proj2 c1 c2) :% (a1, a2) Source # | |
Defined in Data.Category.Functor |
data f1 :***: f2 where Source #
Instances
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | The category for defining the natural numbers and primitive recursion can be described as
|
Defined in Data.Category.Dialg initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: forall (a :: k). Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source # | |
(Functor f1, Functor f2) => Functor (f1 :***: f2) Source # |
|
(TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source # |
|
Defined in Data.Category.Fix 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 (->) (->) ()) (DiagProd (->))) Source # | |
Defined in Data.Category.Dialg | |
type Cod (f1 :***: f2) Source # | |
type Dom (f1 :***: f2) Source # | |
type Unit (WrapTensor (Fix f) t) Source # | |
Defined in Data.Category.Fix | |
type (f1 :***: f2) :% (a1, a2) Source # | |
Defined in Data.Category.Functor |
data DiagProd (k :: Type -> Type -> Type) Source #
Instances
HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | The category for defining the natural numbers and primitive recursion can be described as
|
Defined in Data.Category.Dialg initialObject :: Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) Source # initialize :: forall (a :: k). Obj (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) a -> Dialg (Tuple1 (->) (->) ()) (DiagProd (->)) (InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))) a Source # | |
Category k => Functor (DiagProd k) Source # |
|
type InitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->))) Source # | |
Defined in Data.Category.Dialg | |
type Cod (DiagProd k) Source # | |
Defined in Data.Category.Functor | |
type Dom (DiagProd k) Source # | |
Defined in Data.Category.Functor | |
type (DiagProd k) :% a Source # | |
Defined in Data.Category.Functor |
pattern Tuple1 :: (Category c1, Category c2) => Obj c1 a -> Tuple1 c1 c2 a Source #
Tuple1
tuples with a fixed object on the left.
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 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = (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 :: Type -> Type -> Type) Source #
Instances
HasEnds k => HasWLimits k (Hom k) Source # | Ends as Hom-weighted limits |
Defined in Data.Category.WeightedLimit type WeightedLimit k (Hom k) d Source # limitObj :: FunctorOf (Dom (Hom k)) k d => Hom k -> d -> Obj k (WLimit (Hom k) d) Source # limit :: FunctorOf (Dom (Hom k)) k d => Hom k -> d -> WeightedCone (Hom k) d (WLimit (Hom k) d) Source # limitFactorizer :: FunctorOf (Dom (Hom k)) k d => Hom k -> d -> Obj k e -> WeightedCone (Hom k) d e -> k e (WLimit (Hom k) d) Source # | |
Category k => Functor (Hom k) Source # | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument. |
type WeightedLimit k (Hom k) d Source # | |
Defined in Data.Category.WeightedLimit | |
type Cod (Hom k) Source # | |
Defined in Data.Category.Functor | |
type Dom (Hom k) Source # | |
Defined in Data.Category.Functor | |
type (Hom k) :% (a1, a2) Source # | |
Defined in Data.Category.Functor |