Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Limit

Documentation

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

Instances

Instances details

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

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

Associated Types

type Limit (j :: PRO a i) (d :: PRO k i) :: PRO k a Source Comments #

Methods

limit :: forall (d :: PRO k i). Representable d => Limit j d :~> (d <| j) Source Comments #

limitInv :: forall (d :: PRO k i). Representable d => (d <| j) :~> Limit j d Source Comments #

Instances

Instances details

HasTerminalObject k => HasLimits (Unweighted :: UNIT -> VOID -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: PRO k VOID). Representable d => Limit (Unweighted :: UNIT -> VOID -> Type) d :~> (d <\| (Unweighted :: UNIT -> VOID -> Type)) Source Comments # limitInv :: forall (d :: PRO k VOID). Representable d => (d <\| (Unweighted :: UNIT -> VOID -> Type)) :~> Limit (Unweighted :: UNIT -> VOID -> Type) d Source Comments #
CategoryOf k => HasLimits (Hom :: UNIT -> (OPPOSITE k, k) -> Type) Type Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: PRO Type (OPPOSITE k, k)). Representable d => Limit (Hom :: UNIT -> (OPPOSITE k, k) -> Type) d :~> (d <\| (Hom :: UNIT -> (OPPOSITE k, k) -> Type)) Source Comments # limitInv :: forall (d :: PRO Type (OPPOSITE k, k)). Representable d => (d <\| (Hom :: UNIT -> (OPPOSITE k, k) -> Type)) :~> Limit (Hom :: UNIT -> (OPPOSITE k, k) -> Type) d Source Comments #
HasBinaryProducts k => HasLimits (Unweighted :: UNIT -> COPRODUCT UNIT UNIT -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: PRO k (COPRODUCT UNIT UNIT)). Representable d => Limit (Unweighted :: UNIT -> COPRODUCT UNIT UNIT -> Type) d :~> (d <\| (Unweighted :: UNIT -> COPRODUCT UNIT UNIT -> Type)) Source Comments # limitInv :: forall (d :: PRO k (COPRODUCT UNIT UNIT)). Representable d => (d <\| (Unweighted :: UNIT -> COPRODUCT UNIT UNIT -> Type)) :~> Limit (Unweighted :: UNIT -> COPRODUCT UNIT UNIT -> Type) d Source Comments #

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

data TerminalLimit (d :: PRO k VOID) (a :: k) (b :: UNIT) where Source Comments #

Constructors

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

Instances

Instances details

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

data ProductLimit (d :: PRO k (COPRODUCT UNIT UNIT)) (a :: k) (b :: UNIT) where Source Comments #

Constructors

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

Instances

Instances details

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

choose :: forall k (d :: PRO k (COPRODUCT UNIT UNIT)) (b :: COPRODUCT UNIT UNIT). (HasBinaryProducts k, Representable d) => Obj b -> ((d % ('L 'U :: COPRODUCT UNIT UNIT)) && (d % ('R 'U :: COPRODUCT UNIT UNIT))) ~> (d % b) Source Comments #

newtype End (d :: PRO Type (OPPOSITE k, k)) Source Comments #

Constructors

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

data EndLimit (d :: PRO Type (OPPOSITE k, k)) a (b :: UNIT) where Source Comments #

Constructors

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

Instances

Instances details

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

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

Constructors

Hom :: forall {k} (b :: (OPPOSITE k, k)). Ob b => (UN ('OP :: k -> OPPOSITE k) (Fst b) ~> Snd b) -> Hom 'U b

Instances

Instances details

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