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

Data.Category.WeightedLimit

Description

Synopsis

type WeightedCone w d e = forall a. Obj (Dom w) a -> (w :% a) -> Cod d e (d :% a)
class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where
- type WeightedLimit k w d :: Type
- limitObj :: FunctorOf (Dom w) k d => w -> d -> Obj k (WLimit w d)
- limit :: FunctorOf (Dom w) k d => w -> d -> WeightedCone w d (WLimit w d)
- limitFactorizer :: FunctorOf (Dom w) k d => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)
type WLimit w d = WeightedLimit (Cod d) w d
data LimitFunctor (k :: Type -> Type -> Type) w = LimitFunctor w
class Category v => HasEnds v where
- type End (v :: Type -> Type -> Type) t :: Type
- end :: FunctorOf (Op k :**: k) v t => t -> Obj v (End v t)
- endCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (End v t) (t :% (a, a))
- endFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t)
data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = EndFunctor
newtype HaskEnd t = HaskEnd {
- getHaskEnd :: forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a)
}
type WeightedCocone w d e = forall a. Obj (Dom w) a -> (w :% a) -> Cod d (d :% a) e
class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where
- type WeightedColimit k w d :: Type
- colimitObj :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d)
- colimit :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d)
- colimitFactorizer :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e
type WColimit w d = WeightedColimit (Cod d) w d
data ColimitFunctor (k :: Type -> Type -> Type) w = ColimitFunctor w
class Category v => HasCoends v where
- type Coend (v :: Type -> Type -> Type) t :: Type
- coend :: FunctorOf (Op k :**: k) v t => t -> Obj v (Coend v t)
- coendCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (t :% (a, a)) (Coend v t)
- coendFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x
data OpHom (k :: Type -> Type -> Type) = OpHom
data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) = CoendFunctor
data HaskCoend t where
- HaskCoend :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> (t :% (a, a)) -> HaskCoend t

Documentation

type WeightedCone w d e = forall a. Obj (Dom w) a -> (w :% a) -> Cod d e (d :% a) Source #

class (Functor w, Cod w ~ (->), Category k) => HasWLimits k w where Source #

w-weighted limits in the category k.

Associated Types

type WeightedLimit k w d :: Type Source #

Methods

limitObj :: FunctorOf (Dom w) k d => w -> d -> Obj k (WLimit w d) Source #

limit :: FunctorOf (Dom w) k d => w -> d -> WeightedCone w d (WLimit w d) Source #

limitFactorizer :: FunctorOf (Dom w) k d => w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d) Source #

Instances

Instances details

HasEnds k => HasWLimits k (Hom k) Source #	Ends as Hom-weighted limits
Instance details Defined in Data.Category.WeightedLimit Associated Types type WeightedLimit k (Hom k) d Source # Methods 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 #
HasLimits j k => HasWLimits k (Const j (->) ()) Source #	Regular limits as weigthed limits, weighted by the constant functor to `()`.
Instance details Defined in Data.Category.WeightedLimit Associated Types type WeightedLimit k (Const j (->) ()) d Source # Methods 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 #

type WLimit w d = WeightedLimit (Cod d) w d Source #

data LimitFunctor (k :: Type -> Type -> Type) w Source #

Constructors

LimitFunctor w

Instances

Instances details

HasWLimits k w => Functor (LimitFunctor k w) Source #
Instance details Defined in Data.Category.WeightedLimit Associated Types type Dom (LimitFunctor k w) :: Type -> Type -> Type Source # type Cod (LimitFunctor k w) :: Type -> Type -> Type Source # type (LimitFunctor k w) :% a Source # Methods (%) :: LimitFunctor k w -> Dom (LimitFunctor k w) a b -> Cod (LimitFunctor k w) (LimitFunctor k w :% a) (LimitFunctor k w :% b) Source #
type Cod (LimitFunctor k w) Source #
Instance details Defined in Data.Category.WeightedLimit type Cod (LimitFunctor k w) = k
type Dom (LimitFunctor k w) Source #
Instance details Defined in Data.Category.WeightedLimit type Dom (LimitFunctor k w) = Nat (Dom w) k
type (LimitFunctor k w) :% d Source #
Instance details Defined in Data.Category.WeightedLimit type (LimitFunctor k w) :% d = WeightedLimit k w d

class Category v => HasEnds v where Source #

Associated Types

type End (v :: Type -> Type -> Type) t :: Type Source #

Methods

end :: FunctorOf (Op k :**: k) v t => t -> Obj v (End v t) Source #

endCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (End v t) (t :% (a, a)) Source #

endFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v x (t :% (a, a))) -> v x (End v t) Source #

Instances

Instances details

HasEnds (->) Source #

Instance details

Defined in Data.Category.WeightedLimit

Associated Types

type End (->) t Source #

Methods

end :: forall (k :: Type -> Type -> Type) t. FunctorOf (Op k :**: k) (->) t => t -> Obj (->) (End (->) t) Source #

endCounit :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> End (->) t -> (t :% (a, a)) Source #

endFactorizer :: FunctorOf (Op k :**: k) (->) t => t -> (forall a. Obj k a -> x -> (t :% (a, a))) -> x -> End (->) t Source #

data EndFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) Source #

Constructors

EndFunctor

Instances

Instances details

(HasEnds v, Category k) => Functor (EndFunctor k v) Source #
Instance details Defined in Data.Category.WeightedLimit Associated Types type Dom (EndFunctor k v) :: Type -> Type -> Type Source # type Cod (EndFunctor k v) :: Type -> Type -> Type Source # type (EndFunctor k v) :% a Source # Methods (%) :: EndFunctor k v -> Dom (EndFunctor k v) a b -> Cod (EndFunctor k v) (EndFunctor k v :% a) (EndFunctor k v :% b) Source #
type Cod (EndFunctor k v) Source #
Instance details Defined in Data.Category.WeightedLimit type Cod (EndFunctor k v) = v
type Dom (EndFunctor k v) Source #
Instance details Defined in Data.Category.WeightedLimit type Dom (EndFunctor k v) = Nat (Op k :**: k) v
type (EndFunctor k v) :% t Source #
Instance details Defined in Data.Category.WeightedLimit type (EndFunctor k v) :% t = End v t

newtype HaskEnd t Source #

Constructors

HaskEnd
Fields getHaskEnd :: forall k a. FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> t :% (a, a)

type WeightedCocone w d e = forall a. Obj (Dom w) a -> (w :% a) -> Cod d (d :% a) e Source #

class (Functor w, Cod w ~ (->), Category k) => HasWColimits k w where Source #

w-weighted colimits in the category k.

Associated Types

type WeightedColimit k w d :: Type Source #

Methods

colimitObj :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k (WColimit w d) Source #

colimit :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> WeightedCocone w d (WColimit w d) Source #

colimitFactorizer :: (FunctorOf j k d, Op j ~ Dom w) => w -> d -> Obj k e -> WeightedCocone w d e -> k (WColimit w d) e Source #

Instances

Instances details

HasCoends k => HasWColimits k (OpHom k) Source #	Coends as OpHom-weighted colimits
Instance details Defined in Data.Category.WeightedLimit Associated Types type WeightedColimit k (OpHom k) d Source # Methods colimitObj :: forall (j :: Type -> Type -> Type) d. (FunctorOf j k d, Op j ~ Dom (OpHom k)) => OpHom k -> d -> Obj k (WColimit (OpHom k) d) Source # colimit :: forall (j :: Type -> Type -> Type) d. (FunctorOf j k d, Op j ~ Dom (OpHom k)) => OpHom k -> d -> WeightedCocone (OpHom k) d (WColimit (OpHom k) d) Source # colimitFactorizer :: forall (j :: Type -> Type -> Type) d e. (FunctorOf j k d, Op j ~ Dom (OpHom k)) => OpHom k -> d -> Obj k e -> WeightedCocone (OpHom k) d e -> k (WColimit (OpHom k) d) e Source #
HasColimits j k => HasWColimits k (Const (Op j) (->) ()) Source #	Regular colimits as weigthed colimits, weighted by the constant functor to `()`.
Instance details Defined in Data.Category.WeightedLimit Associated Types type WeightedColimit k (Const (Op j) (->) ()) d Source # Methods 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 #

type WColimit w d = WeightedColimit (Cod d) w d Source #

data ColimitFunctor (k :: Type -> Type -> Type) w Source #

Constructors

ColimitFunctor w

Instances

Instances details

(Functor w, Category k, HasWColimits k (w :.: OpOp (Dom w))) => Functor (ColimitFunctor k w) Source #
Instance details Defined in Data.Category.WeightedLimit Associated Types type Dom (ColimitFunctor k w) :: Type -> Type -> Type Source # type Cod (ColimitFunctor k w) :: Type -> Type -> Type Source # type (ColimitFunctor k w) :% a Source # Methods (%) :: ColimitFunctor k w -> Dom (ColimitFunctor k w) a b -> Cod (ColimitFunctor k w) (ColimitFunctor k w :% a) (ColimitFunctor k w :% b) Source #
type Cod (ColimitFunctor k w) Source #
Instance details Defined in Data.Category.WeightedLimit type Cod (ColimitFunctor k w) = k
type Dom (ColimitFunctor k w) Source #
Instance details Defined in Data.Category.WeightedLimit type Dom (ColimitFunctor k w) = Nat (Op (Dom w)) k
type (ColimitFunctor k w) :% d Source #
Instance details Defined in Data.Category.WeightedLimit type (ColimitFunctor k w) :% d = WeightedColimit k (w :.: OpOp (Dom w)) d

class Category v => HasCoends v where Source #

Associated Types

type Coend (v :: Type -> Type -> Type) t :: Type Source #

Methods

coend :: FunctorOf (Op k :**: k) v t => t -> Obj v (Coend v t) Source #

coendCounit :: FunctorOf (Op k :**: k) v t => t -> Obj k a -> v (t :% (a, a)) (Coend v t) Source #

coendFactorizer :: FunctorOf (Op k :**: k) v t => t -> (forall a. Obj k a -> v (t :% (a, a)) x) -> v (Coend v t) x Source #

Instances

Instances details

HasCoends (->) Source #

Instance details

Defined in Data.Category.WeightedLimit

Associated Types

type Coend (->) t Source #

Methods

coend :: forall (k :: Type -> Type -> Type) t. FunctorOf (Op k :**: k) (->) t => t -> Obj (->) (Coend (->) t) Source #

coendCounit :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> (t :% (a, a)) -> Coend (->) t Source #

coendFactorizer :: FunctorOf (Op k :**: k) (->) t => t -> (forall a. Obj k a -> (t :% (a, a)) -> x) -> Coend (->) t -> x Source #

data OpHom (k :: Type -> Type -> Type) Source #

Constructors

OpHom

Instances

Instances details

HasCoends k => HasWColimits k (OpHom k) Source #	Coends as OpHom-weighted colimits
Instance details Defined in Data.Category.WeightedLimit Associated Types type WeightedColimit k (OpHom k) d Source # Methods colimitObj :: forall (j :: Type -> Type -> Type) d. (FunctorOf j k d, Op j ~ Dom (OpHom k)) => OpHom k -> d -> Obj k (WColimit (OpHom k) d) Source # colimit :: forall (j :: Type -> Type -> Type) d. (FunctorOf j k d, Op j ~ Dom (OpHom k)) => OpHom k -> d -> WeightedCocone (OpHom k) d (WColimit (OpHom k) d) Source # colimitFactorizer :: forall (j :: Type -> Type -> Type) d e. (FunctorOf j k d, Op j ~ Dom (OpHom k)) => OpHom k -> d -> Obj k e -> WeightedCocone (OpHom k) d e -> k (WColimit (OpHom k) d) e Source #
Category k => Functor (OpHom k) Source #	The Hom-functor but with opposite domain.
Instance details Defined in Data.Category.WeightedLimit Associated Types type Dom (OpHom k) :: Type -> Type -> Type Source # type Cod (OpHom k) :: Type -> Type -> Type Source # type (OpHom k) :% a Source # Methods (%) :: OpHom k -> Dom (OpHom k) a b -> Cod (OpHom k) (OpHom k :% a) (OpHom k :% b) Source #
type WeightedColimit k (OpHom k) d Source #
Instance details Defined in Data.Category.WeightedLimit type WeightedColimit k (OpHom k) d = Coend k d
type Cod (OpHom k) Source #
Instance details Defined in Data.Category.WeightedLimit type Cod (OpHom k) = (->)
type Dom (OpHom k) Source #
Instance details Defined in Data.Category.WeightedLimit type Dom (OpHom k) = Op (Op k :**: k)
type (OpHom k) :% (a1, a2) Source #
Instance details Defined in Data.Category.WeightedLimit type (OpHom k) :% (a1, a2) = k a2 a1

data CoendFunctor (k :: Type -> Type -> Type) (v :: Type -> Type -> Type) Source #

Constructors

CoendFunctor

Instances

Instances details

(HasCoends v, Category k) => Functor (CoendFunctor k v) Source #
Instance details Defined in Data.Category.WeightedLimit Associated Types type Dom (CoendFunctor k v) :: Type -> Type -> Type Source # type Cod (CoendFunctor k v) :: Type -> Type -> Type Source # type (CoendFunctor k v) :% a Source # Methods (%) :: CoendFunctor k v -> Dom (CoendFunctor k v) a b -> Cod (CoendFunctor k v) (CoendFunctor k v :% a) (CoendFunctor k v :% b) Source #
type Cod (CoendFunctor k v) Source #
Instance details Defined in Data.Category.WeightedLimit type Cod (CoendFunctor k v) = v
type Dom (CoendFunctor k v) Source #
Instance details Defined in Data.Category.WeightedLimit type Dom (CoendFunctor k v) = Nat (Op k :**: k) v
type (CoendFunctor k v) :% t Source #
Instance details Defined in Data.Category.WeightedLimit type (CoendFunctor k v) :% t = Coend v t

data HaskCoend t where Source #

Constructors

HaskCoend :: FunctorOf (Op k :**: k) (->) t => t -> Obj k a -> (t :% (a, a)) -> HaskCoend t