Safe Haskell	None
Language	GHC2024

Proarrow.Limit.Pullback

Synopsis

class CategoryOf k => HasPullbacks k where
- pullback :: forall (o :: k) (a :: k) (b :: k) r. (a ~> o) -> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
thinPullback :: forall {k} (o :: k) (a :: k) (b :: k) r. (Thin k, HasProducts k) => (a ~> o) -> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
equalizerDefault :: forall {k} (a :: k) (b :: k) r. (HasPullbacks k, HasProducts k) => (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
kernelPair :: forall k (a :: k) (b :: k) r. HasPullbacks k => (a ~> b) -> (forall (p :: k). (p ~> a) -> (p ~> a) -> r) -> r
isMono :: forall k (a :: k) (b :: k). (HasPullbacks k, Eq2 (Hom k)) => (a ~> b) -> Bool

Documentation

class CategoryOf k => HasPullbacks k where Source Github #

Pullbacks are an inherently dependently typed concept: The type of the base object depends on the values of the given arrows. But at runtime we can still calculate the arrows and the type, which we hide behind an existential.

Methods

pullback :: forall (o :: k) (a :: k) (b :: k) r. (a ~> o) -> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

Instances

Instances details

HasPullbacks BOOL Source Github #
Instance details Defined in Proarrow.Category.Instance.Bool Methods pullback :: forall (o :: BOOL) (a :: BOOL) (b :: BOOL) r. (a ~> o) -> (b ~> o) -> (forall (p :: BOOL). (p ~> a) -> (p ~> b) -> r) -> r Source Github #
HasPullbacks FINSET Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods pullback :: forall (o :: FINSET) (a :: FINSET) (b :: FINSET) r. (a ~> o) -> (b ~> o) -> (forall (p :: FINSET). (p ~> a) -> (p ~> b) -> r) -> r Source Github #
HasPullbacks () Source Github #
Instance details Defined in Proarrow.Limit.Pullback Methods pullback :: forall (o :: ()) (a :: ()) (b :: ()) r. (a ~> o) -> (b ~> o) -> (forall (p :: ()). (p ~> a) -> (p ~> b) -> r) -> r Source Github #
HasPushouts k => HasPullbacks (COSPAN k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Cospan Methods pullback :: forall (o :: COSPAN k) (a :: COSPAN k) (b :: COSPAN k) r. (a ~> o) -> (b ~> o) -> (forall (p :: COSPAN k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #
HasPushouts k => HasPullbacks (OPPOSITE k) Source Github #
Instance details Defined in Proarrow.Colimit.Pushout Methods pullback :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r. (a ~> o) -> (b ~> o) -> (forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #
HasPullbacks k => HasPullbacks (SPAN k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Span Methods pullback :: forall (o :: SPAN k) (a :: SPAN k) (b :: SPAN k) r. (a ~> o) -> (b ~> o) -> (forall (p :: SPAN k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #
(HasPullbacks k1, HasPullbacks k2) => HasPullbacks (k1, k2) Source Github #
Instance details Defined in Proarrow.Limit.Pullback Methods pullback :: forall (o :: (k1, k2)) (a :: (k1, k2)) (b :: (k1, k2)) r. (a ~> o) -> (b ~> o) -> (forall (p :: (k1, k2)). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

thinPullback :: forall {k} (o :: k) (a :: k) (b :: k) r. (Thin k, HasProducts k) => (a ~> o) -> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

In a thin category, arrows don't carry information, so pullbacks are just products.

equalizerDefault :: forall {k} (a :: k) (b :: k) r. (HasPullbacks k, HasProducts k) => (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r Source Github #

kernelPair :: forall k (a :: k) (b :: k) r. HasPullbacks k => (a ~> b) -> (forall (p :: k). (p ~> a) -> (p ~> a) -> r) -> r Source Github #

isMono :: forall k (a :: k) (b :: k). (HasPullbacks k, Eq2 (Hom k)) => (a ~> b) -> Bool Source Github #