Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Discrete

Description

The discrete category on an Indexed kind k (DISCRETE k): the numbered inhabitants of k are the objects and the only arrows are identities (Refl). The numbering makes the category decidable, and a Finite kind gives an enumerable one, so that reachability along a graph on a bare set of points can be computed. Its mirror image, the codiscrete category CODISCRETE k, has exactly one arrow between any two objects. All (co)limits that exist are trivially computed.

Synopsis

data DISCRETE k = D k
data Discrete (a :: DISCRETE k) (b :: DISCRETE k) where
- Refl :: forall {k} (a :: DISCRETE k). Ob a => Discrete a a
withEq :: forall {k} (a :: DISCRETE k) (b :: DISCRETE k) r. Indexed k => Discrete a b -> (a ~~ b => r) -> r
type Delta v (c :: BOOL) = If c (Unit :: v) (InitialObject :: v)
deltaAct :: forall {k} {v} (x :: k) (y :: k) (w :: v) (w' :: v). (Quantale v, KnownIndex x, KnownIndex y, Ob w, Ob w') => (x ~ y => w :~: w') -> (Delta v (Equal x y) ** w) ~> w'
data CODISCRETE k = CD k
data Codiscrete (a :: CODISCRETE k) (b :: CODISCRETE k) where
- Arr :: forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => Codiscrete a b
anyArr :: forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). (Indexed k, Ob a, Ob b) => Codiscrete a b

Documentation

data DISCRETE k Source Github #

Constructors

D k

Instances

Instances details

Finite k => Enumerable (DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withIndex :: forall (a :: DISCRETE k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: DISCRETE k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (DISCRETE k) (At (DISCRETE k) i) Source Github #

Finite k => Finite (DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Associated Types

type Objects (DISCRETE k)
Instance details Defined in Proarrow.Category.Instance.Discrete type Objects (DISCRETE k) = MapWrap ('D :: k -> DISCRETE k) (Objects k)

Methods

finite :: IndexedList (Objects (DISCRETE k)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (DISCRETE k)) i ~ At (DISCRETE k) i => r) -> r Source Github #

Indexed k => Indexed (DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Indexed k => HasEpiMonoFactorization (DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

factorize :: forall (a :: DISCRETE k) (b :: DISCRETE k). (a ~> b) -> (Hom (DISCRETE k) :.: Hom (DISCRETE k)) a b 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 #

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 #

Indexed k => CategoryOf (DISCRETE k) Source Github #

The discrete category with only identity arrows on the numbered inhabitants of k.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Discrete type (~>) = Discrete :: DISCRETE k -> DISCRETE k -> Type

Indexed k => HasEqualizers (DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

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

factorEqualizer :: forall (e :: DISCRETE k) (x :: DISCRETE k) (e' :: DISCRETE k). (e ~> x) -> (e' ~> x) -> e' ~> e 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 #

Indexed k => DaggerProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

dagger :: forall (a :: DISCRETE k) (b :: DISCRETE k). Discrete a b -> Discrete b a Source Github #

Indexed k => Promonad (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

id :: forall (a :: DISCRETE k). Ob a => Discrete a a Source Github #

(.) :: forall (b :: DISCRETE k) (c :: DISCRETE k) (a :: DISCRETE k). Discrete b c -> Discrete a b -> Discrete a c Source Github #

Indexed k => EnrichedProfunctor COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => r) -> r Source Github #

underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Discrete a b -> (Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b Source Github #

enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) -> Discrete a b Source Github #

rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST b c ** ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a c Source Github #

lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST c a ** ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) c b Source Github #

(Indexed k, KnownEdges es) => EnrichedProfunctor COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #

A graph with COST weights: a weighted graph, whose closure is shortest paths.

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Edges es) a b) => r) -> r Source Github #

underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Edges es a b -> (Unit :: COST) ~> ProObj COST (Edges es) a b Source Github #

enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Edges es) a b) -> Edges es a b Source Github #

rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST b c ** ProObj COST (Edges es) a b) ~> ProObj COST (Edges es) a c Source Github #

lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST c a ** ProObj COST (Edges es) a b) ~> ProObj COST (Edges es) c b Source Github #

Indexed k => DecidableProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Two points are equal exactly when their indices are.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b (Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) Source Github #

toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Discrete a b -> ((Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

Indexed k => ThinProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => Discrete a b Source Github #

withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Discrete a b -> ((HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Indexed k => Profunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

dimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) (d :: DISCRETE k). (c ~> a) -> (b ~> d) -> Discrete a b -> Discrete c d Source Github #

lmap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k). (c ~> a) -> Discrete a b -> Discrete c b Source Github #

rmap :: forall (b :: DISCRETE k) (d :: DISCRETE k) (a :: DISCRETE k). (b ~> d) -> Discrete a b -> Discrete a d Source Github #

(\\) :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. ((Ob a, Ob b) => r) -> Discrete a b -> r Source Github #

(Indexed k, KnownEdges es) => DecidableProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Edges es) a b (Holds (Edges es) a b) Source Github #

toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((Holds (Edges es) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Indexed k, KnownEdges es) => ThinProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #

A graph with BOOL weights is a relation on the points: decided by walking the edge list.

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Edges es) a b) => Edges es a b Source Github #

withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((HasArrow (Edges es) a b, Ob a, Ob b) => r) -> r Source Github #

Indexed k => Profunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

dimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) (d :: DISCRETE k). (c ~> a) -> (b ~> d) -> Edges es a b -> Edges es c d Source Github #

lmap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k). (c ~> a) -> Edges es a b -> Edges es c b Source Github #

rmap :: forall (b :: DISCRETE k) (d :: DISCRETE k) (a :: DISCRETE k). (b ~> d) -> Edges es a b -> Edges es a d Source Github #

(\\) :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. ((Ob a, Ob b) => r) -> Edges es a b -> r Source Github #

type Objects (DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Objects (DISCRETE k) = MapWrap ('D :: k -> DISCRETE k) (Objects k)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type (~>) = Discrete :: DISCRETE k -> DISCRETE k -> Type

type At (DISCRETE k) i Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type At (DISCRETE k) i = FmapWrap ('D :: k -> DISCRETE k) (At k i)

type Index (a :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Index (a :: DISCRETE k) = Index (UN ('D :: k -> DISCRETE k) a)

type Ob (a :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Ob (a :: DISCRETE k) = KnownIndex a

type ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Delta COST (Equal a b)

type ProObj COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

type ProObj COST (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = WeightOf es a b

type HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = a ~~ b

type Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Equal a b

type HasArrow (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

type HasArrow (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Holds (Edges es) a b ~ 'TRU

type Holds (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

type Holds (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = WeightOf es a b

data Discrete (a :: DISCRETE k) (b :: DISCRETE k) where Source Github #

Constructors

Refl :: forall {k} (a :: DISCRETE k). Ob a => Discrete a a

Instances

Instances details

Indexed k => DaggerProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods dagger :: forall (a :: DISCRETE k) (b :: DISCRETE k). Discrete a b -> Discrete b a Source Github #
Indexed k => Promonad (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods id :: forall (a :: DISCRETE k). Ob a => Discrete a a Source Github # (.) :: forall (b :: DISCRETE k) (c :: DISCRETE k) (a :: DISCRETE k). Discrete b c -> Discrete a b -> Discrete a c Source Github #
Indexed k => EnrichedProfunctor COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. (Ob a, Ob b) => (Ob (ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => r) -> r Source Github # underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k). Discrete a b -> (Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b Source Github # enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => ((Unit :: COST) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) -> Discrete a b Source Github # rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST b c ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a c Source Github # lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k). (Ob a, Ob b, Ob c) => (HomObj COST c a ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) ~> ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) c b Source Github #
Indexed k => DecidableProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #	Two points are equal exactly when their indices are.
Instance details Defined in Proarrow.Category.Instance.Discrete Methods decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b (Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) Source Github # toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Discrete a b -> ((Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
Indexed k => ThinProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => Discrete a b Source Github # withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Discrete a b -> ((HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
Indexed k => Profunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods dimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) (d :: DISCRETE k). (c ~> a) -> (b ~> d) -> Discrete a b -> Discrete c d Source Github # lmap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k). (c ~> a) -> Discrete a b -> Discrete c b Source Github # rmap :: forall (b :: DISCRETE k) (d :: DISCRETE k) (a :: DISCRETE k). (b ~> d) -> Discrete a b -> Discrete a d Source Github # (\\) :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. ((Ob a, Ob b) => r) -> Discrete a b -> r Source Github #
type ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete type ProObj COST (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Delta COST (Equal a b)
type HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete type HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = a ~~ b
type Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete type Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Equal a b

withEq :: forall {k} (a :: DISCRETE k) (b :: DISCRETE k) r. Indexed k => Discrete a b -> (a ~~ b => r) -> r Source Github #

An arrow of DISCRETE k is an equality. This also witnesses that the category is discrete: it only typechecks because withEq demands it.

type Delta v (c :: BOOL) = If c (Unit :: v) (InitialObject :: v) Source Github #

The hom-object of the discrete category in a quantale: the unit on the diagonal, the bottom off it. Points are at distance 0 from themselves and infinitely far from each other: the discrete category is a (discrete) Lawvere metric space, the base for shortest paths on a bare set of points.

deltaAct :: forall {k} {v} (x :: k) (y :: k) (w :: v) (w' :: v). (Quantale v, KnownIndex x, KnownIndex y, Ob w, Ob w') => (x ~ y => w :~: w') -> (Delta v (Equal x y) ** w) ~> w' Source Github #

The action of the discrete base on a matrix over the points: on the diagonal the Delta is the unit and the action is the unitor, off it the Delta is the bottom and the action absorbs. The argument says how the matrix is reindexed on the diagonal.

data CODISCRETE k Source Github #

Constructors

CD k

Instances

Instances details

Finite k => Enumerable (CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withIndex :: forall (a :: CODISCRETE k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: CODISCRETE k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (CODISCRETE k) (At (CODISCRETE k) i) Source Github #

Finite k => Finite (CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Associated Types

type Objects (CODISCRETE k)
Instance details Defined in Proarrow.Category.Instance.Discrete type Objects (CODISCRETE k) = MapWrap ('CD :: k -> CODISCRETE k) (Objects k)

Methods

finite :: IndexedList (Objects (CODISCRETE k)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (CODISCRETE k)) i ~ At (CODISCRETE k) i => r) -> r Source Github #

Indexed k => Indexed (CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Indexed k => HasEpiMonoFactorization (CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

factorize :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (a ~> b) -> (Hom (CODISCRETE k) :.: Hom (CODISCRETE k)) a b Source Github #

Indexed k => HasBinaryCoproducts (CODISCRETE k) Source Github #

Dual to the HasBinaryProducts instance above.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withObCoprod :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: CODISCRETE k) (a :: CODISCRETE k) (y :: CODISCRETE k). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) (x :: CODISCRETE k) (y :: CODISCRETE k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) 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 => 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 => CategoryOf (CODISCRETE k) Source Github #

The codiscrete category has exactly one arrow between any two objects, the numbered inhabitants of k. The numbering makes it enumerable, so its closure can be computed.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Discrete type (~>) = Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type

Indexed k => HasBinaryProducts (CODISCRETE k) Source Github #

Any object works as the product of any two objects here, since every hom-set is a singleton.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withObProd :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: CODISCRETE k) (x :: CODISCRETE k) (y :: CODISCRETE k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) (x :: CODISCRETE k) (y :: CODISCRETE k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

Indexed k => HasEqualizers (CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

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

factorEqualizer :: forall (e :: CODISCRETE k) (x :: CODISCRETE k) (e' :: CODISCRETE k). (e ~> x) -> (e' ~> x) -> e' ~> e 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 => DaggerProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

dagger :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b -> Codiscrete b a Source Github #

Indexed k => Promonad (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

id :: forall (a :: CODISCRETE k). Ob a => Codiscrete a a Source Github #

(.) :: forall (b :: CODISCRETE k) (c :: CODISCRETE k) (a :: CODISCRETE k). Codiscrete b c -> Codiscrete a b -> Codiscrete a c Source Github #

Indexed k => DecidableProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

decide :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => Decision (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b (Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b) Source Github #

toHolds :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. Codiscrete a b -> ((Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

Indexed k => ThinProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

arr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b, HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b) => Codiscrete a b Source Github #

withArr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. Codiscrete a b -> ((HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Indexed k => Profunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

dimap :: forall (c :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k) (d :: CODISCRETE k). (c ~> a) -> (b ~> d) -> Codiscrete a b -> Codiscrete c d Source Github #

lmap :: forall (c :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k). (c ~> a) -> Codiscrete a b -> Codiscrete c b Source Github #

rmap :: forall (b :: CODISCRETE k) (d :: CODISCRETE k) (a :: CODISCRETE k). (b ~> d) -> Codiscrete a b -> Codiscrete a d Source Github #

(\\) :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. ((Ob a, Ob b) => r) -> Codiscrete a b -> r Source Github #

type Objects (CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Objects (CODISCRETE k) = MapWrap ('CD :: k -> CODISCRETE k) (Objects k)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type (~>) = Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type

type At (CODISCRETE k) i Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type At (CODISCRETE k) i = FmapWrap ('CD :: k -> CODISCRETE k) (At k i)

type Index (a :: CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Index (a :: CODISCRETE k) = Index (UN ('CD :: k -> CODISCRETE k) a)

type Ob (a :: CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Ob (a :: CODISCRETE k) = KnownIndex a

type (a :: CODISCRETE k) || (b :: CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type (a :: CODISCRETE k) || (b :: CODISCRETE k) = a

type (a :: CODISCRETE k) && (b :: CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type (a :: CODISCRETE k) && (b :: CODISCRETE k) = a

type HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) = Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b ~ 'TRU

type Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Discrete

type Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) = 'TRU

data Codiscrete (a :: CODISCRETE k) (b :: CODISCRETE k) where Source Github #

Constructors

Arr :: forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => Codiscrete a b

Instances

Instances details

Indexed k => DaggerProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods dagger :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). Codiscrete a b -> Codiscrete b a Source Github #
Indexed k => Promonad (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods id :: forall (a :: CODISCRETE k). Ob a => Codiscrete a a Source Github # (.) :: forall (b :: CODISCRETE k) (c :: CODISCRETE k) (a :: CODISCRETE k). Codiscrete b c -> Codiscrete a b -> Codiscrete a c Source Github #
Indexed k => DecidableProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods decide :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => Decision (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b (Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b) Source Github # toHolds :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. Codiscrete a b -> ((Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
Indexed k => ThinProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods arr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b, HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b) => Codiscrete a b Source Github # withArr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. Codiscrete a b -> ((HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
Indexed k => Profunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete Methods dimap :: forall (c :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k) (d :: CODISCRETE k). (c ~> a) -> (b ~> d) -> Codiscrete a b -> Codiscrete c d Source Github # lmap :: forall (c :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k). (c ~> a) -> Codiscrete a b -> Codiscrete c b Source Github # rmap :: forall (b :: CODISCRETE k) (d :: CODISCRETE k) (a :: CODISCRETE k). (b ~> d) -> Codiscrete a b -> Codiscrete a d Source Github # (\\) :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. ((Ob a, Ob b) => r) -> Codiscrete a b -> r Source Github #
type HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete type HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) = Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b ~ 'TRU
type Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Discrete type Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) (a :: CODISCRETE k) (b :: CODISCRETE k) = 'TRU

anyArr :: forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k). (Indexed k, Ob a, Ob b) => Codiscrete a b Source Github #

Witnesses that CODISCRETE k really is codiscrete: this only typechecks if Codiscrete is a CodiscreteProfunctor, so the definition is the check.