Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Limit

Synopsis

class Representable (Limit j1 d) => IsRepresentableLimit (j1 :: i +-> j) (d :: i +-> k)
class (Profunctor j, forall (d :: i +-> k). Representable d => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where
- type Limit (j :: i +-> a) (d :: i +-> k) :: a +-> k
- limit :: forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d
- limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Representable p) => ((p :.: j) :~> d) -> p :~> Limit j d
rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Adjunction f g, Representable d, Representable f, Representable g, HasLimits j k, HasLimits j k') => Limit j (g :.: d) :~> (g :.: Limit j d)
rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Representable d, Representable g, HasLimits j k, HasLimits j k') => (g :.: Limit j d) :~> Limit j (g :.: d)
type Unweighted = TerminalProfunctor :: k -> j -> Type
data TerminalLimit (d :: VOID +-> k) (a :: k) (b :: ()) where
- TerminalLimit :: forall {k} (d :: VOID +-> k) (a :: k). (a ~> (TerminalObject :: k)) -> TerminalLimit d a '()
data ProductLimit (d :: COPRODUCT () () +-> k) (a :: k) (b :: ()) where
- ProductLimit :: forall {k} (d :: COPRODUCT () () +-> k) (a :: k). (a ~> (ProductLimit d % '())) -> ProductLimit d a '()
choose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()). (HasBinaryProducts k, Representable d) => Obj b -> ((d % ('L '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))) && (d % ('R '() :: COLLAGE (InitialProfunctor :: () -> () -> Type)))) ~> (d % b)
newtype End (d :: (OPPOSITE k, k) +-> Type) = End {
- unEnd :: forall (a :: k) (b :: k). (a ~> b) -> d % '('OP a, b)
}
data EndLimit (d :: (OPPOSITE k, k) +-> Type) a (b :: ()) where
- EndLimit :: forall {k} (d :: (OPPOSITE k, k) +-> Type) a. (a -> End d) -> EndLimit d a '()
data Hom (a :: ()) (b :: (OPPOSITE k, k)) where
- Hom :: forall {k} (a1 :: k) (b1 :: k). (a1 ~> b1) -> Hom '() '('OP a1, b1)

Documentation

class Representable (Limit j1 d) => IsRepresentableLimit (j1 :: i +-> j) (d :: i +-> k) Source Comments #

Instances

Instances details

Representable (Limit j2 d) => IsRepresentableLimit (j2 :: i +-> j1) (d :: i +-> k) Source Comments #
Instance details Defined in Proarrow.Category.Limit

class (Profunctor j, forall (d :: i +-> k). Representable d => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where Source Comments #

profunctor-weighted limits

Associated Types

type Limit (j :: i +-> a) (d :: i +-> k) :: a +-> k Source Comments #

Methods

limit :: forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d Source Comments #

limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Representable p) => ((p :.: j) :~> d) -> p :~> Limit j d Source Comments #

Instances

Instances details

HasTerminalObject k => HasLimits (Unweighted :: () -> VOID -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: VOID +-> k). Representable d => (Limit (Unweighted :: () -> VOID -> Type) d :.: (Unweighted :: () -> VOID -> Type)) :~> d Source Comments # limitUniv :: forall (d :: VOID +-> k) (p :: () +-> k). (Representable d, Representable p) => ((p :.: (Unweighted :: () -> VOID -> Type)) :~> d) -> p :~> Limit (Unweighted :: () -> VOID -> Type) d Source Comments #
CategoryOf k => HasLimits (Hom :: () -> (OPPOSITE k, k) -> Type) Type Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: (OPPOSITE k, k) +-> Type). Representable d => (Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d Source Comments # limitUniv :: forall (d :: (OPPOSITE k, k) +-> Type) (p :: () +-> Type). (Representable d, Representable p) => ((p :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d) -> p :~> Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d Source Comments #
HasBinaryProducts k => HasLimits (Unweighted :: () -> COPRODUCT () () -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: COPRODUCT () () +-> k). Representable d => (Limit (Unweighted :: () -> COPRODUCT () () -> Type) d :.: (Unweighted :: () -> COPRODUCT () () -> Type)) :~> d Source Comments # limitUniv :: forall (d :: COPRODUCT () () +-> k) (p :: () +-> k). (Representable d, Representable p) => ((p :.: (Unweighted :: () -> COPRODUCT () () -> Type)) :~> d) -> p :~> Limit (Unweighted :: () -> COPRODUCT () () -> Type) d Source Comments #

rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Adjunction f g, Representable d, Representable f, Representable g, HasLimits j k, HasLimits j k') => Limit j (g :.: d) :~> (g :.: Limit j d) Source Comments #

rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Representable d, Representable g, HasLimits j k, HasLimits j k') => (g :.: Limit j d) :~> Limit j (g :.: d) Source Comments #

type Unweighted = TerminalProfunctor :: k -> j -> Type Source Comments #

data TerminalLimit (d :: VOID +-> k) (a :: k) (b :: ()) where Source Comments #

Constructors

TerminalLimit :: forall {k} (d :: VOID +-> k) (a :: k). (a ~> (TerminalObject :: k)) -> TerminalLimit d a '()

Instances

Instances details

HasTerminalObject k => Profunctor (TerminalLimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods dimap :: forall (c :: k) (a :: k) (b :: ()) (d0 :: ()). (c ~> a) -> (b ~> d0) -> TerminalLimit d a b -> TerminalLimit d c d0 Source Comments # (\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> TerminalLimit d a b -> r Source Comments #
HasTerminalObject k => Representable (TerminalLimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods index :: forall (a :: k) (b :: ()). TerminalLimit d a b -> a ~> (TerminalLimit d % b) Source Comments # tabulate :: forall (b :: ()) (a :: k). Ob b => (a ~> (TerminalLimit d % b)) -> TerminalLimit d a b Source Comments # repMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (TerminalLimit d % a) ~> (TerminalLimit d % b) Source Comments #
type (TerminalLimit d :: k -> () -> Type) % '() Source Comments #
Instance details Defined in Proarrow.Category.Limit type (TerminalLimit d :: k -> () -> Type) % '() = TerminalObject :: k

data ProductLimit (d :: COPRODUCT () () +-> k) (a :: k) (b :: ()) where Source Comments #

Constructors

ProductLimit :: forall {k} (d :: COPRODUCT () () +-> k) (a :: k). (a ~> (ProductLimit d % '())) -> ProductLimit d a '()

Instances

Instances details

(HasBinaryProducts k, Representable d) => Profunctor (ProductLimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods dimap :: forall (c :: k) (a :: k) (b :: ()) (d0 :: ()). (c ~> a) -> (b ~> d0) -> ProductLimit d a b -> ProductLimit d c d0 Source Comments # (\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> ProductLimit d a b -> r Source Comments #
(HasBinaryProducts k, Representable d) => Representable (ProductLimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods index :: forall (a :: k) (b :: ()). ProductLimit d a b -> a ~> (ProductLimit d % b) Source Comments # tabulate :: forall (b :: ()) (a :: k). Ob b => (a ~> (ProductLimit d % b)) -> ProductLimit d a b Source Comments # repMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (ProductLimit d % a) ~> (ProductLimit d % b) Source Comments #
type (ProductLimit d :: k -> () -> Type) % '() Source Comments #
Instance details Defined in Proarrow.Category.Limit type (ProductLimit d :: k -> () -> Type) % '() = (d % ('L '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))) && (d % ('R '() :: COLLAGE (InitialProfunctor :: () -> () -> Type)))

choose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()). (HasBinaryProducts k, Representable d) => Obj b -> ((d % ('L '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))) && (d % ('R '() :: COLLAGE (InitialProfunctor :: () -> () -> Type)))) ~> (d % b) Source Comments #

newtype End (d :: (OPPOSITE k, k) +-> Type) Source Comments #

Constructors

End
Fields unEnd :: forall (a :: k) (b :: k). (a ~> b) -> d % '('OP a, b)

data EndLimit (d :: (OPPOSITE k, k) +-> Type) a (b :: ()) where Source Comments #

Constructors

EndLimit :: forall {k} (d :: (OPPOSITE k, k) +-> Type) a. (a -> End d) -> EndLimit d a '()

Instances

Instances details

Representable d => Profunctor (EndLimit d :: Type -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods dimap :: forall c a (b :: ()) (d0 :: ()). (c ~> a) -> (b ~> d0) -> EndLimit d a b -> EndLimit d c d0 Source Comments # (\\) :: forall a (b :: ()) r. ((Ob a, Ob b) => r) -> EndLimit d a b -> r Source Comments #
Representable d => Representable (EndLimit d :: Type -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods index :: forall a (b :: ()). EndLimit d a b -> a ~> (EndLimit d % b) Source Comments # tabulate :: forall (b :: ()) a. Ob b => (a ~> (EndLimit d % b)) -> EndLimit d a b Source Comments # repMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (EndLimit d % a) ~> (EndLimit d % b) Source Comments #
type (EndLimit d :: Type -> () -> Type) % '() Source Comments #
Instance details Defined in Proarrow.Category.Limit type (EndLimit d :: Type -> () -> Type) % '() = End d

data Hom (a :: ()) (b :: (OPPOSITE k, k)) where Source Comments #

Constructors

Hom :: forall {k} (a1 :: k) (b1 :: k). (a1 ~> b1) -> Hom '() '('OP a1, b1)

Instances

Instances details

CategoryOf k => Profunctor (Hom :: () -> (OPPOSITE k, k) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods dimap :: forall (c :: ()) (a :: ()) (b :: (OPPOSITE k, k)) (d :: (OPPOSITE k, k)). (c ~> a) -> (b ~> d) -> Hom a b -> Hom c d Source Comments # (\\) :: forall (a :: ()) (b :: (OPPOSITE k, k)) r. ((Ob a, Ob b) => r) -> Hom a b -> r Source Comments #
CategoryOf k => HasLimits (Hom :: () -> (OPPOSITE k, k) -> Type) Type Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: (OPPOSITE k, k) +-> Type). Representable d => (Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d Source Comments # limitUniv :: forall (d :: (OPPOSITE k, k) +-> Type) (p :: () +-> Type). (Representable d, Representable p) => ((p :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d) -> p :~> Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d Source Comments #
type Limit (Hom :: () -> (OPPOSITE k, k) -> Type) (d :: (OPPOSITE k, k) +-> Type) Source Comments #
Instance details Defined in Proarrow.Category.Limit type Limit (Hom :: () -> (OPPOSITE k, k) -> Type) (d :: (OPPOSITE k, k) +-> Type) = EndLimit d