Safe Haskell	None
Language	GHC2024

Proarrow.Limit.Pullback

Description

type depends on the given arrows, so it is hidden behind an existential) and factorPullback for the universal property, defaulting to product-then-equalizer where those exist.

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
- factorPullback :: forall (a :: k) (b :: k) (p :: k) (q :: k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
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.

Minimal complete definition

Nothing

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 #

default pullback :: forall (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 #

factorPullback :: forall (a :: k) (b :: k) (p :: k) (q :: k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

factorPullback p1 p2 k1 k2 requires k1, k2 to be a compatible cone for whichever cospan p1, p2 happen to be a pullback of. p1, p2 need not be pullback's own output.

default factorPullback :: forall (a :: k) (b :: k) (p :: k) (q :: k). (HasEqualizers k, HasProducts k) => (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

Instances

Instances details

HasPullbacks BOOL Source Github #
Instance details Defined in Proarrow.Limit.Pullback 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 # factorPullback :: forall (a :: BOOL) (b :: BOOL) (p :: BOOL) (q :: BOOL). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
HasPullbacks COST Source Github #
Instance details Defined in Proarrow.Category.Instance.Cost Methods pullback :: forall (o :: COST) (a :: COST) (b :: COST) r. (a ~> o) -> (b ~> o) -> (forall (p :: COST). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: COST) (b :: COST) (p :: COST) (q :: COST). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
HasPullbacks FINHASK Source Github #	Example 3.84 of Seven Sketches (A: 0=red, 1=blue, 2=black) >>> data Color = Red \| Blue \| Black deriving (P.Eq, P.Ord, P.Show, P.Enum, P.Bounded, Universe, Finite) >>> let f :: FinHask (FH (Fin 6)) (FH Color) = fromList [(0,Red), (1,Blue), (2,Red), (3,Red), (4,Black), (5,Blue)] >>> let g :: FinHask (FH (Fin 4)) (FH Color) = fromList [(0,Black), (1,Red), (2,Blue), (3,Red)] >>> (pullback f g (FinHask l) (FinHask r) -> P.show (P.zip (M.elems l) (M.elems r))) :: P.String "[(0,1),(0,3),(1,2),(2,1),(2,3),(3,1),(3,3),(4,0),(5,2)]"
Instance details Defined in Proarrow.Category.Instance.FinHask Methods pullback :: forall (o :: FINHASK) (a :: FINHASK) (b :: FINHASK) r. (a ~> o) -> (b ~> o) -> (forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: FINHASK) (b :: FINHASK) (p :: FINHASK) (q :: FINHASK). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
HasPullbacks FINSET Source Github #	`>>>` `import Data.Fin``>>>` `import Data.Type.Nat``>>>` `import Data.Vec.Lazy``>>>` `let f :: FinSet (FS Nat6) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin0 ::: fin0 ::: fin2 ::: fin1 ::: VNil``>>>` `let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil``>>>` `(pullback f g \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String`"(0 ::: 0 ::: 1 ::: 2 ::: 2 ::: 3 ::: 3 ::: 4 ::: 5 ::: VNil,1 ::: 3 ::: 2 ::: 1 ::: 3 ::: 1 ::: 3 ::: 0 ::: 2 ::: VNil)"
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 # factorPullback :: forall (a :: FINSET) (b :: FINSET) (p :: FINSET) (q :: FINSET). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p 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 # factorPullback :: forall (a :: ()) (b :: ()) (p :: ()) (q :: ()). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
Indexed k => HasPullbacks (CODISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods pullback :: forall (o :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k) r. (a ~> o) -> (b ~> o) -> (forall (p :: CODISCRETE k). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) (p :: CODISCRETE k) (q :: CODISCRETE k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
Indexed k => HasPullbacks (DISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods pullback :: forall (o :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) r. (a ~> o) -> (b ~> o) -> (forall (p :: DISCRETE k). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: DISCRETE k) (b :: DISCRETE k) (p :: DISCRETE k) (q :: DISCRETE k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
(Fractional a, Eq a) => HasPullbacks (MatK a) Source Github #	Pullbacks are computed via `pullbackDefault`, as the equalizer of `f . fst` and `g . snd` on the product `a && b`, the standard linear-algebra construction of a fiber product of vector spaces. `>>>` `let f = Mat @(S Z) @(S Z) ((2 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)``>>>` `let g = Mat @(S Z) @(S Z) ((3 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)``>>>` `(pullback f g \p q -> case (p, q) of (Mat pv, Mat qv) -> P.show (pv, qv)) :: P.String`"((1.5 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil)"
Instance details Defined in Proarrow.Category.Instance.Mat Methods pullback :: forall (o :: MatK a) (a0 :: MatK a) (b :: MatK a) r. (a0 ~> o) -> (b ~> o) -> (forall (p :: MatK a). (p ~> a0) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a0 :: MatK a) (b :: MatK a) (p :: MatK a) (q :: MatK a). (p ~> a0) -> (p ~> b) -> (q ~> a0) -> (q ~> b) -> q ~> p 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 # factorPullback :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (p :: OPPOSITE k) (q :: OPPOSITE k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
HasPullbacks (ORDINAL n) Source Github #	Pullbacks in a thin category are just meets. Computed directly, not via `thinPullback`, which would need `HasProducts (ORDINAL n)`. That is unavailable for an abstract `n`, since `HasBinaryProducts` and `HasTerminalObject` are only resolvable for a syntactically concrete `n`.
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods pullback :: forall (o :: ORDINAL n) (a :: ORDINAL n) (b :: ORDINAL n) r. (a ~> o) -> (b ~> o) -> (forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: ORDINAL n) (b :: ORDINAL n) (p :: ORDINAL n) (q :: ORDINAL n). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
HasPullbacks k => HasPullbacks (PROD k) Source Github #	Pullbacks are unchanged by making the tensor the product.
Instance details Defined in Proarrow.Limit.Pullback Methods pullback :: forall (o :: PROD k) (a :: PROD k) (b :: PROD k) r. (a ~> o) -> (b ~> o) -> (forall (p :: PROD k). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: PROD k) (b :: PROD k) (p :: PROD k) (q :: PROD k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
(Enumerable j, Enumerable k) => HasPullbacks (FINITARY j k) Source Github #	Pullbacks are equalizers of products, and pushouts coequalizers of coproducts, all of which finitary profunctors have.
Instance details Defined in Proarrow.Category.Enriched.Finitary.Topos Methods pullback :: forall (o :: FINITARY j k) (a :: FINITARY j k) (b :: FINITARY j k) r. (a ~> o) -> (b ~> o) -> (forall (p :: FINITARY j k). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: FINITARY j k) (b :: FINITARY j k) (p :: FINITARY j k) (q :: FINITARY j k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
(HasPullbacks j, HasPullbacks k) => HasPullbacks (COPRODUCT j k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Coproduct Methods pullback :: forall (o :: COPRODUCT j k) (a :: COPRODUCT j k) (b :: COPRODUCT j k) r. (a ~> o) -> (b ~> o) -> (forall (p :: COPRODUCT j k). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k) (p :: COPRODUCT j k) (q :: COPRODUCT j k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p 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 # factorPullback :: forall (a :: (k1, k2)) (b :: (k1, k2)) (p :: (k1, k2)) (q :: (k1, k2)). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #
(Site t k, Enumerable j, Enumerable k) => HasPullbacks (SHEAVES t j k) Source Github #
Instance details Defined in Proarrow.Category.Enriched.Finitary.Sheaf Methods pullback :: forall (o :: SHEAVES t j k) (a :: SHEAVES t j k) (b :: SHEAVES t j k) r. (a ~> o) -> (b ~> o) -> (forall (p :: SHEAVES t j k). (p ~> a) -> (p ~> b) -> r) -> r Source Github # factorPullback :: forall (a :: SHEAVES t j k) (b :: SHEAVES t j k) (p :: SHEAVES t j k) (q :: SHEAVES t j k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p 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 #