proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Colimit.Pushout

Description

given arrows, so it is hidden behind an existential), and factorPushout for the universal property, defaulting to coproduct-then-coequalizer where those exist.

Synopsis

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.

Minimal complete definition

Nothing

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 #

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

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

factorPushout p1 p2 k1 k2 requires k1, k2 to be a compatible cocone for whichever cospan p1, p2 happen to be a pushout of. p1, p2 need not literally be pushout's own output.

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

Instances

Instances details
HasPushouts BOOL Source Github # 
Instance details

Defined in Proarrow.Colimit.Pushout

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 #

factorPushout :: forall (a :: BOOL) (b :: BOOL) (p :: BOOL) (q :: BOOL). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

HasPushouts COST Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cost

Methods

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

factorPushout :: forall (a :: COST) (b :: COST) (p :: COST) (q :: COST). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

HasPushouts FINHASK Source Github #

Exercise 6.22 of Seven Sketches >>> let l :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,0), (2,1), (3,2)] >>> let r :: FinHask (FH (Fin 4)) (FH (Fin 5)) = fromList [(0,0), (1,2), (2,4), (3,4)] >>> (pushout l r l' r' -> P.show (l', r')) :: P.String "(fromList [(0,1),(1,3),(2,3)],fromList [(0,1),(1,0),(2,1),(3,2),(4,3)])"

Instance details

Defined in Proarrow.Category.Instance.FinHask

Methods

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

factorPushout :: forall (a :: FINHASK) (b :: FINHASK) (p :: FINHASK) (q :: FINHASK). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

HasPushouts FINSET Source Github #
>>> import Data.Fin
>>> import Data.Type.Nat
>>> let l :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin0 ::: fin1 ::: fin2 ::: VNil
>>> let r :: FinSet (FS Nat4) (FS Nat5) = FinSet $ fin0 ::: fin2 ::: fin4 ::: fin4 ::: VNil
>>> (pushout l r \(FinSet l') (FinSet r') -> P.show (l', r')) :: P.String
"(1 ::: 3 ::: 3 ::: VNil,1 ::: 0 ::: 1 ::: 2 ::: 3 ::: VNil)"
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 #

factorPushout :: forall (a :: FINSET) (b :: FINSET) (p :: FINSET) (q :: FINSET). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q 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 #

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

Indexed k => HasPushouts (CODISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

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

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

Indexed k => HasPushouts (DISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

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

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

(Fractional a, Eq a) => HasPushouts (MatK a) Source Github #

Pushouts are computed via pushoutDefault, as the coequalizer of lft . f and rgt . g on the coproduct a || b, the standard linear-algebra construction of a cofiber 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)
>>> (pushout 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

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

factorPushout :: forall (a0 :: MatK a) (b :: MatK a) (p :: MatK a) (q :: MatK a). (a0 ~> p) -> (b ~> p) -> (a0 ~> q) -> (b ~> q) -> p ~> q 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 #

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

HasPushouts (ORDINAL n) Source Github #

Dual to the HasPullbacks instance above: pushouts in a thin category are joins.

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

factorPushout :: forall (a :: ORDINAL n) (b :: ORDINAL n) (p :: ORDINAL n) (q :: ORDINAL n). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

HasPushouts k => HasPushouts (PROD k) Source Github #

Pushouts are unchanged by making the tensor the product.

Instance details

Defined in Proarrow.Colimit.Pushout

Methods

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

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

(Enumerable j, Enumerable k) => HasPushouts (FINITARY j k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

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

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

(HasPushouts j, HasPushouts k) => HasPushouts (COPRODUCT j k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Coproduct

Methods

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

factorPushout :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k) (p :: COPRODUCT j k) (q :: COPRODUCT j k). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q 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 #

factorPushout :: forall (a :: (k1, k2)) (b :: (k1, k2)) (p :: (k1, k2)) (q :: (k1, k2)). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

(HasFiniteCovers t k, FiniteCat j, FiniteCat k) => HasPushouts (SHEAVES t j k) Source Github #

Not the default coproduct-then-coequalizer, which would sheafify the coproduct and then sheafify the quotient of that. Each Sheafify pays for the one under it, since the plus construction re-runs on every toIndex. Taking both steps in FINITARY and sheafifying once at the end gives the same object, since sheafification is a left adjoint and preserves the pushout, and it avoids stacking one plus construction on another.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Sheaf

Methods

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

factorPushout :: forall (a :: SHEAVES t j k) (b :: SHEAVES t j k) (p :: SHEAVES t j k) (q :: SHEAVES t j k). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q 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 #

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 #