Safe Haskell	None
Language	GHC2024

Proarrow.Profunctor.Corepresentable

Documentation

class Profunctor p => Corepresentable (p :: j +-> k) where Source Github #

Associated Types

type (p :: j +-> k) %% (a :: k) :: j infixl 8 Source Github #

Methods

coindex :: forall (a :: k) (b :: j). p a b -> (p %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (p %% a) ~> (p %% b) Source Github #

Instances

Instances details

Corepresentable Booleans Source Github #

Instance details

Defined in Proarrow.Category.Instance.Bool

Associated Types

type Booleans %% (x :: BOOL)
Instance details Defined in Proarrow.Category.Instance.Bool type Booleans %% (x :: BOOL) = x

Methods

coindex :: forall (a :: BOOL) (b :: BOOL). Booleans a b -> (Booleans %% a) ~> b Source Github #

cotabulate :: forall (a :: BOOL) (b :: BOOL). Ob a => ((Booleans %% a) ~> b) -> Booleans a b Source Github #

corepMap :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> (Booleans %% a) ~> (Booleans %% b) Source Github #

Corepresentable (Fold :: Type -> Type -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Fold

Associated Types

type (Fold :: Type -> Type -> Type) %% (a :: Type)
Instance details Defined in Proarrow.Profunctor.Fold type (Fold :: Type -> Type -> Type) %% (a :: Type) = [a]

Methods

coindex :: Fold a b -> ((Fold :: Type -> Type -> Type) %% a) ~> b Source Github #

cotabulate :: Ob a => (((Fold :: Type -> Type -> Type) %% a) ~> b) -> Fold a b Source Github #

corepMap :: (a ~> b) -> ((Fold :: Type -> Type -> Type) %% a) ~> ((Fold :: Type -> Type -> Type) %% b) Source Github #

CategoryOf k => Corepresentable (Id :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Identity

Methods

coindex :: forall (a :: k) (b :: k). Id a b -> ((Id :: k -> k -> Type) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: k). Ob a => (((Id :: k -> k -> Type) %% a) ~> b) -> Id a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((Id :: k -> k -> Type) %% a) ~> ((Id :: k -> k -> Type) %% b) Source Github #

Corepresentable (->) Source Github #

Instance details

Defined in Proarrow.Profunctor.Corepresentable

Associated Types

type (->) %% (a :: Type)
Instance details Defined in Proarrow.Profunctor.Corepresentable type (->) %% (a :: Type) = a

Methods

coindex :: (a -> b) -> ((->) %% a) ~> b Source Github #

cotabulate :: Ob a => (((->) %% a) ~> b) -> a -> b Source Github #

corepMap :: (a ~> b) -> ((->) %% a) ~> ((->) %% b) Source Github #

(HasInitialObject j, CategoryOf k) => Corepresentable (TerminalProfunctor :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Object.Initial

Methods

coindex :: forall (a :: k) (b :: j). TerminalProfunctor a b -> ((TerminalProfunctor :: k -> j -> Type) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => (((TerminalProfunctor :: k -> j -> Type) %% a) ~> b) -> TerminalProfunctor a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((TerminalProfunctor :: k -> j -> Type) %% a) ~> ((TerminalProfunctor :: k -> j -> Type) %% b) Source Github #

(Ob r, Monoidal k) => Corepresentable (Reader ('OP r) :: k -> k -> Type) Source Github #

The coreader comonad given the Promonad instance. Together with the Representable instance this gives the curry/uncurry adjunction.

Instance details

Defined in Proarrow.Promonad.Reader

Methods

coindex :: forall (a :: k) (b :: k). Reader ('OP r) a b -> (Reader ('OP r) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: k). Ob a => ((Reader ('OP r) %% a) ~> b) -> Reader ('OP r) a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Reader ('OP r) %% a) ~> (Reader ('OP r) %% b) Source Github #

(Ob w, SelfAction k, CompactClosed k) => Corepresentable (Writer w :: k -> k -> Type) Source Github #

The cowriter comonad given the Promonad instance.

Instance details

Defined in Proarrow.Promonad.Writer

Methods

coindex :: forall (a :: k) (b :: k). Writer w a b -> (Writer w %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: k). Ob a => ((Writer w %% a) ~> b) -> Writer w a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Writer w %% a) ~> (Writer w %% b) Source Github #

Corepresentable (Rep Forget) Source Github #

By creating the left adjoint to the forgetful functor, we obtain the free-forgetful adjunction between Hask and LINEAR

Instance details

Defined in Proarrow.Category.Instance.Linear

Associated Types

type (Rep Forget) %% (a :: Type)
Instance details Defined in Proarrow.Category.Instance.Linear type (Rep Forget) %% (a :: Type) = 'L (Ur a)

Methods

coindex :: forall a (b :: LINEAR). Rep Forget a b -> (Rep Forget %% a) ~> b Source Github #

cotabulate :: forall a (b :: LINEAR). Ob a => ((Rep Forget %% a) ~> b) -> Rep Forget a b Source Github #

corepMap :: (a ~> b) -> (Rep Forget %% a) ~> (Rep Forget %% b) Source Github #

Corepresentable (Star ((->) a) :: Type -> Type -> Type) Source Github #

The left adjoint of ((->) a) is (,) a.

Instance details

Defined in Proarrow.Adjunction

Methods

coindex :: Star ((->) a) a0 b -> (Star ((->) a) %% a0) ~> b Source Github #

cotabulate :: Ob a0 => ((Star ((->) a) %% a0) ~> b) -> Star ((->) a) a0 b Source Github #

corepMap :: (a0 ~> b) -> (Star ((->) a) %% a0) ~> (Star ((->) a) %% b) Source Github #

Corepresentable p => Corepresentable (Adj p :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Adjunction

Methods

coindex :: forall (a :: k) (b :: j). Adj p a b -> (Adj p %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((Adj p %% a) ~> b) -> Adj p a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Adj p %% a) ~> (Adj p %% b) 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 #

FunctorForRep f => Corepresentable (Corep f :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Corepresentable

Methods

coindex :: forall (a :: k) (b :: j). Corep f a b -> (Corep f %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((Corep f %% a) ~> b) -> Corep f a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Corep f %% a) ~> (Corep f %% b) Source Github #

Functor f => Corepresentable (Costar f :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Costar

Methods

coindex :: forall (a :: k) (b :: j). Costar f a b -> (Costar f %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((Costar f %% a) ~> b) -> Costar f a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Costar f %% a) ~> (Costar f %% b) Source Github #

Representable p => Corepresentable (RepCostar p :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Representable

Methods

coindex :: forall (a :: k) (b :: j). RepCostar p a b -> (RepCostar p %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((RepCostar p %% a) ~> b) -> RepCostar p a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (RepCostar p %% a) ~> (RepCostar p %% b) Source Github #

Corepresentable p => Corepresentable (Wrapped p :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Wrapped

Methods

coindex :: forall (a :: k) (b :: j). Wrapped p a b -> (Wrapped p %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((Wrapped p %% a) ~> b) -> Wrapped p a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Wrapped p %% a) ~> (Wrapped p %% b) Source Github #

Corepresentable l => Corepresentable (AsLeftAdjoint l :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Universal

Methods

coindex :: forall (a :: k) (b :: j). AsLeftAdjoint l a b -> (AsLeftAdjoint l %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((AsLeftAdjoint l %% a) ~> b) -> AsLeftAdjoint l a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (AsLeftAdjoint l %% a) ~> (AsLeftAdjoint l %% b) Source Github #

(forall (a :: k). Ob a => InitUniversal r a, Representable r) => Corepresentable (AsRightAdjoint r :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Universal

Methods

coindex :: forall (a :: k) (b :: j). AsRightAdjoint r a b -> (AsRightAdjoint r %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((AsRightAdjoint r %% a) ~> b) -> AsRightAdjoint r a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (AsRightAdjoint r %% a) ~> (AsRightAdjoint r %% b) Source Github #

Corepresentable p => Corepresentable (FromAdjunction p :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Universal

Methods

coindex :: forall (a :: k) (b :: j). FromAdjunction p a b -> (FromAdjunction p %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => ((FromAdjunction p %% a) ~> b) -> FromAdjunction p a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (FromAdjunction p %% a) ~> (FromAdjunction p %% b) Source Github #

(HasBinaryCoproducts j, Corepresentable p, Corepresentable q) => Corepresentable (p :*: q :: k -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Object.BinaryCoproduct

Methods

coindex :: forall (a :: k) (b :: j). (p :*: q) a b -> ((p :*: q) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: j). Ob a => (((p :*: q) %% a) ~> b) -> (p :*: q) a b Source Github #

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

(Corepresentable p, Corepresentable q) => Corepresentable (p :.: q :: k -> j2 -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Composition

Methods

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

cotabulate :: forall (a :: k) (b :: j2). Ob a => (((p :.: q) %% a) ~> b) -> (p :.: q) a b Source Github #

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

(HasColimits j k2, Corepresentable d) => Corepresentable (Rift ('OP j) d :: k1 -> k2 -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Rift

Methods

coindex :: forall (a :: k1) (b :: k2). Rift ('OP j) d a b -> (Rift ('OP j) d %% a) ~> b Source Github #

cotabulate :: forall (a :: k1) (b :: k2). Ob a => ((Rift ('OP j) d %% a) ~> b) -> Rift ('OP j) d a b Source Github #

corepMap :: forall (a :: k1) (b :: k1). (a ~> b) -> (Rift ('OP j) d %% a) ~> (Rift ('OP j) d %% b) Source Github #

HasCofree ob => Corepresentable (Rep (CofreeSub ob) :: SUBCAT ob -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Cofree

Methods

coindex :: forall (a :: SUBCAT ob) (b :: k). Rep (CofreeSub ob) a b -> (Rep (CofreeSub ob) %% a) ~> b Source Github #

cotabulate :: forall (a :: SUBCAT ob) (b :: k). Ob a => ((Rep (CofreeSub ob) %% a) ~> b) -> Rep (CofreeSub ob) a b Source Github #

corepMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (a ~> b) -> (Rep (CofreeSub ob) %% a) ~> (Rep (CofreeSub ob) %% b) Source Github #

Representable p => Corepresentable (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github #

Instance details

Defined in Proarrow.Profunctor.Representable

Methods

coindex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Op p %% a) ~> b Source Github #

cotabulate :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Ob a => ((Op p %% a) ~> b) -> Op p a b Source Github #

corepMap :: forall (a :: OPPOSITE j) (b :: OPPOSITE j). (a ~> b) -> (Op p %% a) ~> (Op p %% b) Source Github #

HasFree ob => Corepresentable (Rep (Forget ob) :: k -> SUBCAT ob -> Type) Source Github #

By creating the left adjoint to the forgetful functor, we obtain the free-forgetful adjunction.

Instance details

Defined in Proarrow.Profunctor.Free

Methods

coindex :: forall (a :: k) (b :: SUBCAT ob). Rep (Forget ob) a b -> (Rep (Forget ob) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: SUBCAT ob). Ob a => ((Rep (Forget ob) %% a) ~> b) -> Rep (Forget ob) a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Rep (Forget ob) %% a) ~> (Rep (Forget ob) %% b) Source Github #

(Corepresentable l, Corepresentable r, CategoryOf k) => Corepresentable (l :&&: r :: k -> (x, y) -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

coindex :: forall (a :: k) (b :: (x, y)). (l :&&: r) a b -> ((l :&&: r) %% a) ~> b Source Github #

cotabulate :: forall (a :: k) (b :: (x, y)). Ob a => (((l :&&: r) %% a) ~> b) -> (l :&&: r) a b Source Github #

corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((l :&&: r) %% a) ~> ((l :&&: r) %% b) Source Github #

Profunctor j2 => Corepresentable (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) :: (k -> j1 -> Type) -> (i +-> k) -> Type) Source Github #

The right Kan extension is the right adjoint of the precomposition functor.

Instance details

Defined in Proarrow.Profunctor.Ran

Methods

coindex :: forall (a :: k -> j1 -> Type) (b :: i +-> k). Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) a b -> (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) %% a) ~> b Source Github #

cotabulate :: forall (a :: k -> j1 -> Type) (b :: i +-> k). Ob a => ((Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) %% a) ~> b) -> Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) a b Source Github #

corepMap :: forall (a :: k -> j1 -> Type) (b :: k -> j1 -> Type). (a ~> b) -> (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) %% a) ~> (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) %% b) Source Github #

Profunctor j2 => Corepresentable (Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) :: (k -> j1 -> Type) -> (j1 +-> i) -> Type) Source Github #

The right Kan lift is the right adjoint of the postcomposition functor.

Instance details

Defined in Proarrow.Profunctor.Rift

Methods

coindex :: forall (a :: k -> j1 -> Type) (b :: j1 +-> i). Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) a b -> (Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) %% a) ~> b Source Github #

cotabulate :: forall (a :: k -> j1 -> Type) (b :: j1 +-> i). Ob a => ((Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) %% a) ~> b) -> Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) a b Source Github #

corepMap :: forall (a :: k -> j1 -> Type) (b :: k -> j1 -> Type). (a ~> b) -> (Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) %% a) ~> (Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) %% b) Source Github #

HasColimits j k => Corepresentable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Github #

Instance details

Defined in Proarrow.Adjunction

Methods

coindex :: forall (a0 :: COREPK b k) (b0 :: REPK a k). LimitAdj j a0 b0 -> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) ~> b0 Source Github #

cotabulate :: forall (a0 :: COREPK b k) (b0 :: REPK a k). Ob a0 => (((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) ~> b0) -> LimitAdj j a0 b0 Source Github #

corepMap :: forall (a0 :: COREPK b k) (b0 :: COREPK b k). (a0 ~> b0) -> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) ~> ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% b0) Source Github #

corepObj :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2). (Corepresentable p, Ob a) => Obj (p %% a) Source Github #

withCorepOb :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r. (Corepresentable p, Ob a) => (Ob (p %% a) => r) -> r Source Github #

dimapCorep :: forall {j} {k} p (a :: k) (b :: j) (c :: k) (d :: j). Corepresentable p => (c ~> a) -> (b ~> d) -> p a b -> p c d Source Github #

trivialCorep :: forall {j} {k} p (a :: k). (Corepresentable p, Ob a) => p a (p %% a) Source Github #

data Corep (f :: j +-> k) (a :: j) (b :: k) where Source Github #

Constructors

Corep
Fields :: forall {j} {k} (f :: j +-> k) (a :: j) (b :: k). Ob a => { unCorep :: (f @ a) ~> b } -> Corep f a b

Instances

Instances details

MonoidalProfunctor (Corep Forget) Source Github #	Forget is also a colax monoidal functor
Instance details Defined in Proarrow.Category.Instance.Linear Methods par0 :: Corep Forget (Unit :: LINEAR) (Unit :: Type) Source Github # par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2. Corep Forget x1 x2 -> Corep Forget y1 y2 -> Corep Forget (x1 y1) (x2 y2) Source Github #
(Monoidal k, Comonoid r) => MonoidalProfunctor (Corep (Constant r) :: k -> k -> Type) Source Github #
Instance details Defined in Proarrow.Monoid Methods par0 :: Corep (Constant r) (Unit :: k) (Unit :: k) Source Github # par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k). Corep (Constant r) x1 x2 -> Corep (Constant r) y1 y2 -> Corep (Constant r) (x1 y1) (x2 y2) Source Github #
FunctorForRep f => Profunctor (Corep f :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Corepresentable Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Corep f a b -> Corep f c d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Corep f a b -> r Source Github #
FunctorForRep f => Corepresentable (Corep f :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Corepresentable Methods coindex :: forall (a :: k) (b :: j). Corep f a b -> (Corep f %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: j). Ob a => ((Corep f %% a) ~> b) -> Corep f a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Corep f %% a) ~> (Corep f %% b) Source Github #
FunctorForRep f => HasLimits (Corep f :: a -> i -> Type) k Source Github #
Instance details Defined in Proarrow.Category.Limit Methods limit :: forall (d :: i +-> k). Representable d => (Limit (Corep f) d :.: Corep f) :~> d Source Github # limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Profunctor p) => ((p :.: Corep f) :~> d) -> p :~> Limit (Corep f) d Source Github #
FunctorForRep f => Proadjunction (Rep f :: k -> j -> Type) (Corep f :: j -> k -> Type) Source Github #
Instance details Defined in Proarrow.Adjunction Methods unit :: forall (a :: j). Ob a => (Corep f :.: Rep f) a a Source Github # counit :: (Rep f :.: Corep f) :~> ((~>) :: CAT k) Source Github #
(Closed k, SymMonoidal k, Ob r) => Representable (Corep (Not r) :: k -> OPPOSITE k -> Type) Source Github #	The Op-Op adjunction, giving rise to the continuation monad.
Instance details Defined in Proarrow.Object.Exponential Methods index :: forall (a :: k) (b :: OPPOSITE k). Corep (Not r) a b -> a ~> (Corep (Not r) % b) Source Github # tabulate :: forall (b :: OPPOSITE k) (a :: k). Ob b => (a ~> (Corep (Not r) % b)) -> Corep (Not r) a b Source Github # repMap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k). (a ~> b) -> (Corep (Not r) % a) ~> (Corep (Not r) % b) Source Github #
type Limit (Corep f :: a -> i -> Type) (d :: i +-> k) Source Github #
Instance details Defined in Proarrow.Category.Limit type Limit (Corep f :: a -> i -> Type) (d :: i +-> k) = d :.: Rep f
type (Corep f :: k -> j -> Type) %% (a :: k) Source Github #
Instance details Defined in Proarrow.Profunctor.Corepresentable type (Corep f :: k -> j -> Type) %% (a :: k) = f @ a
type (Corep (Not r) :: k -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) Source Github #
Instance details Defined in Proarrow.Object.Exponential type (Corep (Not r) :: k -> OPPOSITE k -> Type) % ('OP a :: OPPOSITE k) = a ~~> r

corep :: forall {j} {k} (f :: j +-> k) (a :: j) (b :: k) (a' :: j) (b' :: k). Ob a => Iso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b') Source Github #

type Comonad (w :: j +-> j) = (Promonad w, Corepresentable w) Source Github #

extract :: forall {k} (w :: k +-> k) (a :: k). (Comonad w, Ob a) => (w %% a) ~> a Source Github #

extend :: forall {j} (w :: j +-> j) (a :: j) (b :: j). (Comonad w, Ob a) => ((w %% a) ~> b) -> (w %% a) ~> (w %% b) Source Github #