Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Rel

Description

Relations as profunctors: a Relation is a thin profunctor between discrete categories, and this module collects the standard vocabulary of properties (Functional, Total, Injective, Surjective, Reflexive, Transitive, Symmetric, up to Preorder and Equivalence), together with the Converse relation.

Synopsis

class (ThinProfunctor p, Discrete j, Discrete k) => Relation (p :: j +-> k)
data Converse (p :: j +-> k) (a :: j) (b :: k) where
- Converse :: forall {j} {k} (p :: j +-> k) (b :: k) (a :: j). p b a -> Converse p a b
asImplication :: forall {k1} {k2} (a :: k1) (b :: k2) (p :: k2 +-> k1) (q :: k2 +-> k1) r. (Relation p, Relation q) => (p :~> q) -> (Ob a, Ob b, HasArrow p a b) => ((HasArrow q a b, Ob a, Ob b) => r) -> r
class Relation p => Functional (p :: j +-> k1) where
- isFunctional :: (p :.: Converse p) :~> ((~>) :: CAT k1)
reprIsFunctional :: forall {j} {k1} (p :: j +-> k1). (Relation p, Representable p) => (p :.: Converse p) :~> ((~>) :: CAT k1)
class Relation p => Total (p :: k1 +-> j) where
- isTotal :: ((~>) :: CAT k1) :~> (Converse p :.: p)
reprIsTotal :: forall {k1} {j} (p :: k1 +-> j). (Relation p, Representable p) => ((~>) :: CAT k1) :~> (Converse p :.: p)
class Relation p => Injective (p :: k1 +-> j) where
- isInjective :: (Converse p :.: p) :~> ((~>) :: CAT k1)
class Relation p => Surjective (p :: j +-> k1) where
- isSurjective :: ((~>) :: CAT k1) :~> (p :.: Converse p)
class Relation p => Reflexive (p :: k1 +-> k1) where
- isReflexive :: ((~>) :: CAT k1) :~> p
class Relation p => Transitive (p :: k1 +-> k1) where
- isTransitive :: (p :.: p) :~> p
adjToConverse :: forall {j} {k} (p :: j +-> k) (q :: k +-> j). (Relation p, Relation q, Proadjunction p q) => q :~> Converse p
adjFromConverse :: forall {k} {k1} (p :: k +-> k1) (q :: k1 +-> k). (Relation p, Relation q, Proadjunction p q) => Converse p :~> q
class (Relation p, Promonad p) => Preorder (p :: k +-> k)
class (Relation p, DaggerProfunctor p) => Symmetric (p :: k +-> k)
class (Preorder p, Symmetric p) => Equivalence (p :: k +-> k)

Documentation

class (ThinProfunctor p, Discrete j, Discrete k) => Relation (p :: j +-> k) Source Github #

Instances

Instances details

(ThinProfunctor p, Discrete j, Discrete k) => Relation (p :: j +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel

data Converse (p :: j +-> k) (a :: j) (b :: k) where Source Github #

The converse relation: Converse p a b relates a to b exactly when p relates b to a.

Constructors

Converse :: forall {j} {k} (p :: j +-> k) (b :: k) (a :: j). p b a -> Converse p a b

Instances

Instances details

(Relation p, DecidableProfunctor p) => DecidableProfunctor (Converse p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel Methods decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (Converse p) a b (Holds (Converse p) a b) Source Github # toHolds :: forall (a :: k) (b :: j) r. Converse p a b -> ((Holds (Converse p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
Relation p => ThinProfunctor (Converse p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel Methods arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (Converse p) a b) => Converse p a b Source Github # withArr :: forall (a :: k) (b :: j) r. Converse p a b -> ((HasArrow (Converse p) a b, Ob a, Ob b) => r) -> r Source Github #
Relation p => Profunctor (Converse p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Converse p a b -> Converse p c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> Converse p a b -> Converse p c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> Converse p a b -> Converse p a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Converse p a b -> r Source Github #
(Relation p, Representable p) => Corepresentable (Converse p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel Methods coindex :: forall (a :: k) (b :: j). Converse p a b -> (Converse p %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: j). Ob a => ((Converse p %% a) ~> b) -> Converse p a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Converse p %% a) ~> (Converse p %% b) Source Github # corepUniv :: forall (a :: k). Ob a => Converse p a (Converse p %% a) Source Github #
type (Converse p :: k -> j -> Type) %% (a :: k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel type (Converse p :: k -> j -> Type) %% (a :: k) = p % a
type HasArrow (Converse p :: k -> j -> Type) (a :: k) (b :: j) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel type HasArrow (Converse p :: k -> j -> Type) (a :: k) (b :: j) = HasArrow p b a
type Holds (Converse p :: k -> j -> Type) (a :: k) (b :: j) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel type Holds (Converse p :: k -> j -> Type) (a :: k) (b :: j) = Holds p b a

asImplication :: forall {k1} {k2} (a :: k1) (b :: k2) (p :: k2 +-> k1) (q :: k2 +-> k1) r. (Relation p, Relation q) => (p :~> q) -> (Ob a, Ob b, HasArrow p a b) => ((HasArrow q a b, Ob a, Ob b) => r) -> r Source Github #

class Relation p => Functional (p :: j +-> k1) where Source Github #

Methods

isFunctional :: (p :.: Converse p) :~> ((~>) :: CAT k1) Source Github #

reprIsFunctional :: forall {j} {k1} (p :: j +-> k1). (Relation p, Representable p) => (p :.: Converse p) :~> ((~>) :: CAT k1) Source Github #

class Relation p => Total (p :: k1 +-> j) where Source Github #

Methods

isTotal :: ((~>) :: CAT k1) :~> (Converse p :.: p) Source Github #

reprIsTotal :: forall {k1} {j} (p :: k1 +-> j). (Relation p, Representable p) => ((~>) :: CAT k1) :~> (Converse p :.: p) Source Github #

class Relation p => Injective (p :: k1 +-> j) where Source Github #

Methods

isInjective :: (Converse p :.: p) :~> ((~>) :: CAT k1) Source Github #

class Relation p => Surjective (p :: j +-> k1) where Source Github #

Methods

isSurjective :: ((~>) :: CAT k1) :~> (p :.: Converse p) Source Github #

class Relation p => Reflexive (p :: k1 +-> k1) where Source Github #

Methods

isReflexive :: ((~>) :: CAT k1) :~> p Source Github #

class Relation p => Transitive (p :: k1 +-> k1) where Source Github #

Methods

isTransitive :: (p :.: p) :~> p Source Github #

adjToConverse :: forall {j} {k} (p :: j +-> k) (q :: k +-> j). (Relation p, Relation q, Proadjunction p q) => q :~> Converse p Source Github #

adjFromConverse :: forall {k} {k1} (p :: k +-> k1) (q :: k1 +-> k). (Relation p, Relation q, Proadjunction p q) => Converse p :~> q Source Github #

class (Relation p, Promonad p) => Preorder (p :: k +-> k) Source Github #

Instances

Instances details

(Relation p, Promonad p) => Preorder (p :: k +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel

class (Relation p, DaggerProfunctor p) => Symmetric (p :: k +-> k) Source Github #

Instances

Instances details

(Relation p, DaggerProfunctor p) => Symmetric (p :: k +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel

class (Preorder p, Symmetric p) => Equivalence (p :: k +-> k) Source Github #

Instances

Instances details

(Preorder p, Symmetric p) => Equivalence (p :: k +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Rel