Safe Haskell	None
Language	GHC2024

Proarrow.Colimit.Pushout

Contents

Orphan instances

Synopsis

class CategoryOf k => HasPushouts k where
- pushout :: forall (o :: k) (a :: k) (b :: k) r. (o ~> a) -> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
thinPushout :: forall {k} (o :: k) (a :: k) (b :: k) r. (Thin k, HasCoproducts k) => (o ~> a) -> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
coequalizerDefault :: forall {k} (a :: k) (b :: k) r. (HasPushouts k, HasCoproducts k) => (a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
cokernelPair :: forall k (a :: k) (b :: k) r. HasPushouts k => (a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
isEpi :: forall k (a :: k) (b :: k). (HasPushouts k, Eq2 (Hom k)) => (a ~> b) -> Bool

Documentation

class CategoryOf k => HasPushouts k where Source Github #

Pushouts are an inherently dependently typed concept: The type of the apex 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

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

Instances

Instances details

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

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

In a thin category, arrows don't carry information, so pushouts are just coproducts.

coequalizerDefault :: forall {k} (a :: k) (b :: k) r. (HasPushouts k, HasCoproducts k) => (a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r Source Github #

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

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

Orphan instances

HasPushouts k => HasPullbacks (OPPOSITE k) Source Github #
Instance details 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 #