Safe Haskell	None
Language	GHC2024

Proarrow.Colimit.Coequalizer

Contents

Orphan instances

Description

depends on the given arrows, so it is hidden behind an existential) and factorCoequalizer for the universal property.

Synopsis

class CategoryOf k => HasCoequalizers k where
- coequalize :: forall (a :: k) (b :: k) r. (a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
- factorCoequalizer :: forall (c :: k) (x :: k) (c' :: k). (x ~> c) -> (x ~> c') -> c ~> c'
thinCoequalize :: forall {k} (a :: k) (b :: k) r. Thin k => (a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
pushoutDefault :: forall {k} (o :: k) (a :: k) (b :: k) r. (HasCoequalizers k, HasCoproducts k) => (o ~> a) -> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
factorPushoutDefault :: forall {k} (a :: k) (b :: k) (p :: k) (q :: k). (HasCoequalizers k, HasCoproducts k) => (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
cokernel :: forall k (a :: k) (b :: k) r. (HasCoequalizers k, HasZeroObject k) => (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r

Documentation

class CategoryOf k => HasCoequalizers k where Source Github #

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

Methods

coequalize :: forall (a :: k) (b :: k) r. (a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: k) (x :: k) (c' :: k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

factorCoequalizer q h requires q to be epi and h to be constant on q's fibers; q is typically (though not necessarily) the coequalizer arrow produced by coequalize.

Instances

Instances details

HasCoequalizers BOOL Source Github #	Dual to the `HasEqualizers` instance for `BOOL`.
Instance details Defined in Proarrow.Colimit.Coequalizer Methods coequalize :: forall (a :: BOOL) (b :: BOOL) r. (a ~> b) -> (a ~> b) -> (forall (c :: BOOL). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: BOOL) (x :: BOOL) (c' :: BOOL). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasCoequalizers COST Source Github #	Dual to the `HasEqualizers` instance above.
Instance details Defined in Proarrow.Category.Instance.Cost Methods coequalize :: forall (a :: COST) (b :: COST) r. (a ~> b) -> (a ~> b) -> (forall (c :: COST). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: COST) (x :: COST) (c' :: COST). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasCoequalizers FINHASK Source Github #
Instance details Defined in Proarrow.Category.Instance.FinHask Methods coequalize :: forall (a :: FINHASK) (b :: FINHASK) r. (a ~> b) -> (a ~> b) -> (forall (c :: FINHASK). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: FINHASK) (x :: FINHASK) (c' :: FINHASK). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasCoequalizers FINSET Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods coequalize :: forall (a :: FINSET) (b :: FINSET) r. (a ~> b) -> (a ~> b) -> (forall (c :: FINSET). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: FINSET) (x :: FINSET) (c' :: FINSET). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasCoequalizers () Source Github #
Instance details Defined in Proarrow.Colimit.Coequalizer Methods coequalize :: forall (a :: ()) (b :: ()) r. (a ~> b) -> (a ~> b) -> (forall (c :: ()). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: ()) (x :: ()) (c' :: ()). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
Indexed k => HasCoequalizers (CODISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods coequalize :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. (a ~> b) -> (a ~> b) -> (forall (c :: CODISCRETE k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: CODISCRETE k) (x :: CODISCRETE k) (c' :: CODISCRETE k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
Indexed k => HasCoequalizers (DISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods coequalize :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (a ~> b) -> (a ~> b) -> (forall (c :: DISCRETE k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: DISCRETE k) (x :: DISCRETE k) (c' :: DISCRETE k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
(Fractional a, Eq a) => HasCoequalizers (MatK a) Source Github #	The coequalizer of `f, g :: M m ~> M n` is the cokernel of `f - g`. Since `dagger` is a contravariant involution on `Mat`, it is the equalizer of `dagger f, dagger g` transported back. `>>>` `let f = Mat @(S Z) @(S (S Z)) ((2 ::: VNil) ::: (0 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)``>>>` `let g = Mat @(S Z) @(S (S Z)) ((0 ::: VNil) ::: (3 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)``>>>` `let w = Mat @(S (S Z)) @(S Z) ((3 ::: 2 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)``>>>` `(coequalize f g \q@(Mat qv) -> case factorCoequalizer q w of s@(Mat sv) -> P.show (qv, sv, unMat (s . q))) :: P.String`"((1.5 ::: 1.0 ::: VNil) ::: VNil,(2.0 ::: VNil) ::: VNil,(3.0 ::: 2.0 ::: VNil) ::: VNil)"
Instance details Defined in Proarrow.Category.Instance.Mat Methods coequalize :: forall (a0 :: MatK a) (b :: MatK a) r. (a0 ~> b) -> (a0 ~> b) -> (forall (c :: MatK a). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: MatK a) (x :: MatK a) (c' :: MatK a). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasEqualizers k => HasCoequalizers (OPPOSITE k) Source Github #
Instance details Defined in Proarrow.Colimit.Coequalizer Methods coequalize :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r. (a ~> b) -> (a ~> b) -> (forall (c :: OPPOSITE k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: OPPOSITE k) (x :: OPPOSITE k) (c' :: OPPOSITE k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasCoequalizers (ORDINAL n) Source Github #	Dual to the `HasEqualizers` instance above.
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods coequalize :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. (a ~> b) -> (a ~> b) -> (forall (c :: ORDINAL n). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: ORDINAL n) (x :: ORDINAL n) (c' :: ORDINAL n). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
HasCoequalizers k => HasCoequalizers (PROD k) Source Github #	Coequalizers are unchanged by making the tensor the product.
Instance details Defined in Proarrow.Colimit.Coequalizer Methods coequalize :: forall (a :: PROD k) (b :: PROD k) r. (a ~> b) -> (a ~> b) -> (forall (c :: PROD k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: PROD k) (x :: PROD k) (c' :: PROD k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
(Enumerable j, Enumerable k) => HasCoequalizers (FINITARY j k) Source Github #	Coequalizers: at each pair of objects, partition the indices by the equivalence relation the two natural transformations generate, and reify the table. Naturality makes the partition a congruence, so the quotient is again a profunctor.
Instance details Defined in Proarrow.Category.Enriched.Finitary.Topos Methods coequalize :: forall (a :: FINITARY j k) (b :: FINITARY j k) r. (a ~> b) -> (a ~> b) -> (forall (c :: FINITARY j k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: FINITARY j k) (x :: FINITARY j k) (c' :: FINITARY j k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
(HasCoequalizers j, HasCoequalizers k) => HasCoequalizers (COPRODUCT j k) Source Github #	Dual to the `HasEqualizers` instance above.
Instance details Defined in Proarrow.Category.Instance.Coproduct Methods coequalize :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k) r. (a ~> b) -> (a ~> b) -> (forall (c :: COPRODUCT j k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: COPRODUCT j k) (x :: COPRODUCT j k) (c' :: COPRODUCT j k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
(HasCoequalizers k1, HasCoequalizers k2) => HasCoequalizers (k1, k2) Source Github #
Instance details Defined in Proarrow.Colimit.Coequalizer Methods coequalize :: forall (a :: (k1, k2)) (b :: (k1, k2)) r. (a ~> b) -> (a ~> b) -> (forall (c :: (k1, k2)). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: (k1, k2)) (x :: (k1, k2)) (c' :: (k1, k2)). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) => HasCoequalizers (SHEAVES t j k) Source Github #	The quotient a coequalizer takes is `coequalizeNat`'s, sheafified. Its projection is epi in the sheaves but need not be onto (the sheafification unit is not), so `factorCoequalizer` is not `FINITARY`'s. It descends, by `factorThroughLocalEpi`.
Instance details Defined in Proarrow.Category.Enriched.Finitary.Sheaf Methods coequalize :: forall (a :: SHEAVES t j k) (b :: SHEAVES t j k) r. (a ~> b) -> (a ~> b) -> (forall (c :: SHEAVES t j k). (b ~> c) -> r) -> r Source Github # factorCoequalizer :: forall (c :: SHEAVES t j k) (x :: SHEAVES t j k) (c' :: SHEAVES t j k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

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

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

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

Standalone helper (not a class method) usable as the default implementation of pushout wherever (HasCoequalizers k, HasCoproducts k) happen to hold. Not every HasPushouts instance needs it or is required to have it.

factorPushoutDefault :: forall {k} (a :: k) (b :: k) (p :: k) (q :: k). (HasCoequalizers k, HasCoproducts k) => (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

Given a pushout's own legs p1, p2 and a compatible cocone k1, k2 out of some q (with k1 . f == k2 . g for whichever cospan p1, p2 are a pushout of), produces the unique p ~> q through which the cocone factors. Standalone helper (not a class method), usable as the default implementation of factorPushout, dual to factorPullbackDefault.

cokernel :: forall k (a :: k) (b :: k) r. (HasCoequalizers k, HasZeroObject k) => (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r Source Github #

Orphan instances

HasCoequalizers k => HasEqualizers (OPPOSITE k) Source Github #
Instance details 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 (e :: OPPOSITE k) (x :: OPPOSITE k) (e' :: OPPOSITE k). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #