| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Object.Pushout
Contents
Synopsis
- data Cocone (bs :: LIST k) (a :: COPROD k) where
- data Sink (as :: [k]) where
- class HasCoproducts k => HasPushouts k where
- coequalizer :: forall {k} (a :: k) (b :: k). HasPushouts k => (a ~> b) -> (a ~> b) -> Sink '[b]
- cokernel :: forall k (a :: k) (b :: k). (HasPushouts k, HasZeroObject k) => (a ~> b) -> Sink '[b]
Documentation
data Cocone (bs :: LIST k) (a :: COPROD k) where Source Github #
A cocone is a bunch of arrows with a shared target.
Constructors
| Coapex :: forall {k} (a1 :: k). Ob a1 => Cocone ('L ('[] :: [k])) ('COPR a1) | |
| Coleg :: forall {k} (b :: k) (a1 :: k) (bs1 :: [k]). (b ~> a1) -> Cocone ('L bs1) ('COPR a1) -> Cocone ('L (b ': bs1)) ('COPR a1) |
Instances
| HasCoproducts k => MonoidalProfunctor (Cocone :: LIST k -> COPROD k -> Type) Source Github # | |
| CategoryOf k => Profunctor (Cocone :: LIST k -> COPROD k -> Type) Source Github # | |
data Sink (as :: [k]) where Source Github #
A sink is a cocone, but with the apex type hidden by an existential.
class HasCoproducts 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). (o ~> a) -> (o ~> b) -> Sink '[a, b] Source Github #
Instances
| HasPushouts FINSET Source Github # | |
| HasPullbacks k => HasPushouts (OPPOSITE k) Source Github # | |
coequalizer :: forall {k} (a :: k) (b :: k). HasPushouts k => (a ~> b) -> (a ~> b) -> Sink '[b] Source Github #
cokernel :: forall k (a :: k) (b :: k). (HasPushouts k, HasZeroObject k) => (a ~> b) -> Sink '[b] Source Github #