Safe Haskell	None
Language	GHC2024

Proarrow.Limit.Equalizer

Synopsis

class CategoryOf k => HasEqualizers k where
- equalize :: forall (a :: k) (b :: k) r. (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
- factorEqualizer :: forall (a :: k) (b :: k) (c :: k). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom k :.: Hom k) c a
thinEqualize :: forall {k} (a :: k) (b :: k) r. Thin k => (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
thinFactorEqualizer :: forall {k} (a :: k) (b :: k) (c :: k). Thin k => (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom k :.: Hom k) c a
pullbackDefault :: forall {k} (o :: k) (a :: k) (b :: k) r. (HasEqualizers k, HasProducts k) => (a ~> o) -> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
kernel :: forall k (a :: k) (b :: k) r. (HasEqualizers k, HasZeroObject k) => (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r

Documentation

class CategoryOf k => HasEqualizers k where Source Github #

Equalizers 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 arrow and the type, which we hide behind an existential.

Minimal complete definition

factorEqualizer

Methods

equalize :: forall (a :: k) (b :: k) r. (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r Source Github #

default equalize :: forall (a :: k) (b :: k) r. HasInitialObject k => (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (a :: k) (b :: k) (c :: k). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom k :.: Hom k) c a Source Github #

Instances

Instances details

HasEqualizers BOOL Source Github #
Instance details Defined in Proarrow.Category.Instance.Bool Methods equalize :: forall (a :: BOOL) (b :: BOOL) r. (a ~> b) -> (a ~> b) -> (forall (e :: BOOL). (e ~> a) -> r) -> r Source Github # factorEqualizer :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom BOOL :.: Hom BOOL) c a Source Github #
HasEqualizers FINSET Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods equalize :: forall (a :: FINSET) (b :: FINSET) r. (a ~> b) -> (a ~> b) -> (forall (e :: FINSET). (e ~> a) -> r) -> r Source Github # factorEqualizer :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom FINSET :.: Hom FINSET) c a Source Github #
HasEqualizers () Source Github #
Instance details Defined in Proarrow.Limit.Equalizer Methods equalize :: forall (a :: ()) (b :: ()) r. (a ~> b) -> (a ~> b) -> (forall (e :: ()). (e ~> a) -> r) -> r Source Github # factorEqualizer :: forall (a :: ()) (b :: ()) (c :: ()). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom () :.: Hom ()) c a Source Github #
HasCoequalizers k => HasEqualizers (OPPOSITE k) Source Github #
Instance details Defined in Proarrow.Colimit.Coequalizer Methods equalize :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (a ~> b) -> (a ~> b) -> (forall (e :: OPPOSITE k). (e ~> a) -> r) -> r Source Github # factorEqualizer :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom (OPPOSITE k) :.: Hom (OPPOSITE k)) c a Source Github #
(HasEqualizers k1, HasEqualizers k2) => HasEqualizers (k1, k2) Source Github #
Instance details Defined in Proarrow.Limit.Equalizer Methods equalize :: forall (a :: (k1, k2)) (b :: (k1, k2)) r. (a ~> b) -> (a ~> b) -> (forall (e :: (k1, k2)). (e ~> a) -> r) -> r Source Github # factorEqualizer :: forall (a :: (k1, k2)) (b :: (k1, k2)) (c :: (k1, k2)). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom (k1, k2) :.: Hom (k1, k2)) c a Source Github #

thinEqualize :: forall {k} (a :: k) (b :: k) r. Thin k => (a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r Source Github #

In a thin category, arrows don't carry information, so equalizers are just identities.

thinFactorEqualizer :: forall {k} (a :: k) (b :: k) (c :: k). Thin k => (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom k :.: Hom k) c a Source Github #

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

kernel :: forall k (a :: k) (b :: k) r. (HasEqualizers k, HasZeroObject k) => (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r Source Github #