Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Graph

Synopsis

data GRAPH (p :: k +-> j) = GR j k
data family ProjJ :: forall (p :: k +-> j) -> GRAPH p +-> j
data family ProjK :: forall (p :: k +-> j) -> GRAPH p +-> k
data Graph (a :: GRAPH p) (b :: GRAPH p) where
- Graph :: forall {k} {k1} {p :: k +-> k1} (aj :: k1) (ak :: k) (bj :: k1) (bk :: k). (HasArrow p aj ak, HasArrow p bj bk) => (aj ~> bj) -> (ak ~> bk) -> Graph ('GR aj ak :: GRAPH p) ('GR bj bk :: GRAPH p)
diagonalElement :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j) (bk :: k) r. ThinProfunctor p => (('GR aj ak :: GRAPH p) ~> ('GR bj bk :: GRAPH p)) -> ((HasArrow p aj bk, Ob aj, Ob bk) => r) -> r
graphUniv :: forall {j} {k} (p :: k +-> j). ThinProfunctor p => Iso' p (Rep (ProjJ p) :.: Corep (ProjK p))
data family ProdAsGraph :: (j, k) +-> GRAPH p
type ARROW k = GRAPH (Id :: k -> k -> Type)
type ELEMENTS (f :: k +-> j) = GRAPH (Rep f)
type COMMA (f :: j +-> k) (g :: k1 +-> k) = GRAPH (Direp f g)

Documentation

data GRAPH (p :: k +-> j) Source Github #

Constructors

GR j k

Instances

Instances details

(CategoryOf j, CategoryOf k, CodiscreteProfunctor p) => FunctorForRep (ProdAsGraph :: (j, k) +-> GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

fmap :: forall (a :: (j, k)) (b :: (j, k)). (a ~> b) -> ((ProdAsGraph :: (j, k) +-> GRAPH p) @ a) ~> ((ProdAsGraph :: (j, k) +-> GRAPH p) @ b) Source Github #

ThinProfunctor p => CategoryOf (GRAPH p) Source Github #

The graph of a thin profunctor. Doing this for any profunctor would need dependent types.

Instance details

Defined in Proarrow.Category.Instance.Graph

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Graph type (~>) = Graph :: GRAPH p -> GRAPH p -> Type

ThinProfunctor p => FunctorForRep (ProjK p :: GRAPH p +-> k) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> (ProjK p @ a) ~> (ProjK p @ b) Source Github #

ThinProfunctor p => FunctorForRep (ProjJ p :: GRAPH p +-> k2) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> (ProjJ p @ a) ~> (ProjJ p @ b) Source Github #

ThinProfunctor p => Promonad (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

id :: forall (a :: GRAPH p). Ob a => Graph a a Source Github #

(.) :: forall (b :: GRAPH p) (c :: GRAPH p) (a :: GRAPH p). Graph b c -> Graph a b -> Graph a c Source Github #

ThinProfunctor p => Profunctor (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

Methods

dimap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p) (d :: GRAPH p). (c ~> a) -> (b ~> d) -> Graph a b -> Graph c d Source Github #

lmap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p). (c ~> a) -> Graph a b -> Graph c b Source Github #

rmap :: forall (b :: GRAPH p) (d :: GRAPH p) (a :: GRAPH p). (b ~> d) -> Graph a b -> Graph a d Source Github #

(\\) :: forall (a :: GRAPH p) (b :: GRAPH p) r. ((Ob a, Ob b) => r) -> Graph a b -> r Source Github #

type (ProdAsGraph :: (j, k) +-> GRAPH p) @ ('(a, b) :: (j, k)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (ProdAsGraph :: (j, k) +-> GRAPH p) @ ('(a, b) :: (j, k)) = 'GR a b :: GRAPH p

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (~>) = Graph :: GRAPH p -> GRAPH p -> Type

type Ob (ab :: GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type Ob (ab :: GRAPH p) = (ab ~ ('GR (ProjJ p @ ab) (ProjK p @ ab) :: GRAPH p), Ob (ProjJ p @ ab), Ob (ProjK p @ ab), HasArrow p (ProjJ p @ ab) (ProjK p @ ab))

type (ProjK p :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (ProjK p :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) = y

type (ProjJ p :: GRAPH p +-> k1) @ ('GR x y :: GRAPH p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Graph

type (ProjJ p :: GRAPH p +-> k1) @ ('GR x y :: GRAPH p) = x

data family ProjJ :: forall (p :: k +-> j) -> GRAPH p +-> j Source Github #

Instances

Instances details

ThinProfunctor p => FunctorForRep (ProjJ p :: GRAPH p +-> k2) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> (ProjJ p @ a) ~> (ProjJ p @ b) Source Github #
type (ProjJ p :: GRAPH p +-> k1) @ ('GR x y :: GRAPH p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph type (ProjJ p :: GRAPH p +-> k1) @ ('GR x y :: GRAPH p) = x

data family ProjK :: forall (p :: k +-> j) -> GRAPH p +-> k Source Github #

Instances

Instances details

ThinProfunctor p => FunctorForRep (ProjK p :: GRAPH p +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods fmap :: forall (a :: GRAPH p) (b :: GRAPH p). (a ~> b) -> (ProjK p @ a) ~> (ProjK p @ b) Source Github #
type (ProjK p :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph type (ProjK p :: GRAPH p +-> k) @ ('GR x y :: GRAPH p) = y

data Graph (a :: GRAPH p) (b :: GRAPH p) where Source Github #

Constructors

Graph :: forall {k} {k1} {p :: k +-> k1} (aj :: k1) (ak :: k) (bj :: k1) (bk :: k). (HasArrow p aj ak, HasArrow p bj bk) => (aj ~> bj) -> (ak ~> bk) -> Graph ('GR aj ak :: GRAPH p) ('GR bj bk :: GRAPH p)

Instances

Instances details

ThinProfunctor p => Promonad (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods id :: forall (a :: GRAPH p). Ob a => Graph a a Source Github # (.) :: forall (b :: GRAPH p) (c :: GRAPH p) (a :: GRAPH p). Graph b c -> Graph a b -> Graph a c Source Github #
ThinProfunctor p => Profunctor (Graph :: GRAPH p -> GRAPH p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods dimap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p) (d :: GRAPH p). (c ~> a) -> (b ~> d) -> Graph a b -> Graph c d Source Github # lmap :: forall (c :: GRAPH p) (a :: GRAPH p) (b :: GRAPH p). (c ~> a) -> Graph a b -> Graph c b Source Github # rmap :: forall (b :: GRAPH p) (d :: GRAPH p) (a :: GRAPH p). (b ~> d) -> Graph a b -> Graph a d Source Github # (\\) :: forall (a :: GRAPH p) (b :: GRAPH p) r. ((Ob a, Ob b) => r) -> Graph a b -> r Source Github #

diagonalElement :: forall {j} {k} (p :: k +-> j) (aj :: j) (ak :: k) (bj :: j) (bk :: k) r. ThinProfunctor p => (('GR aj ak :: GRAPH p) ~> ('GR bj bk :: GRAPH p)) -> ((HasArrow p aj bk, Ob aj, Ob bk) => r) -> r Source Github #

A morphism gives two equal ways to compute the "diagonal", which is an element of the profunctor.

graphUniv :: forall {j} {k} (p :: k +-> j). ThinProfunctor p => Iso' p (Rep (ProjJ p) :.: Corep (ProjK p)) Source Github #

data family ProdAsGraph :: (j, k) +-> GRAPH p Source Github #

Instances

Instances details

(CategoryOf j, CategoryOf k, CodiscreteProfunctor p) => FunctorForRep (ProdAsGraph :: (j, k) +-> GRAPH p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph Methods fmap :: forall (a :: (j, k)) (b :: (j, k)). (a ~> b) -> ((ProdAsGraph :: (j, k) +-> GRAPH p) @ a) ~> ((ProdAsGraph :: (j, k) +-> GRAPH p) @ b) Source Github #
type (ProdAsGraph :: (j, k) +-> GRAPH p) @ ('(a, b) :: (j, k)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Graph type (ProdAsGraph :: (j, k) +-> GRAPH p) @ ('(a, b) :: (j, k)) = 'GR a b :: GRAPH p

type ARROW k = GRAPH (Id :: k -> k -> Type) Source Github #

The arrow category is the graph of the hom-functor. Here we require the category to be thin.

type ELEMENTS (f :: k +-> j) = GRAPH (Rep f) Source Github #

The category of elements of a functor.

type COMMA (f :: j +-> k) (g :: k1 +-> k) = GRAPH (Direp f g) Source Github #

The comma category f/g is the graph of C(f(-), g(=)).