| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Profunctor.Corepresentable
Synopsis
- class Profunctor p => Corepresentable (p :: j +-> k) where
- corepObj :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2). (Corepresentable p, Ob a) => Obj (p %% a)
- withObCorep :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r. (Corepresentable p, Ob a) => (Ob (p %% a) => r) -> r
- 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
- cotabulated :: forall {k1} {k2} p (a :: k2) (a' :: k2) (b :: k1) (b' :: k1). (Corepresentable p, Ob a) => Iso ((p %% a) ~> b) ((p %% a') ~> b') (p a b) (p a' b')
- type RepresentableCopresheaf (f :: Copresheaf k) = Corepresentable f
- type Key (f :: Copresheaf k) = f %% '()
- tabulatedCopresheaf :: forall {k} f (a :: k) (a' :: k). (RepresentableCopresheaf f, Ob a) => Iso (Key f ~> a) (Key f ~> a') (f '() a) (f '() a')
- data Corep (f :: j +-> k) (a :: j) (b :: k) where
- corep :: forall {j} {k} (f :: j +-> k) (a :: j) (b :: k) (a' :: j) (b' :: k). (FunctorForRep f, Ob a) => Iso ((f @ a) ~> b) ((f @ a') ~> b') (Corep f a b) (Corep f a' b')
Documentation
class Profunctor p => Corepresentable (p :: j +-> k) where Source Github #
A profunctor is corepresentable if p a ? as a copresheaf is representable in a functorial way over a.
Minimal complete definition
coindex, (cotabulate, corepMap | corepUniv)
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 #
corepUniv :: forall (a :: k). Ob a => p a (p %% a) Source Github #
Instances
| Corepresentable Booleans Source Github # | |||||
Defined in Proarrow.Category.Instance.Bool Associated Types
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 # corepUniv :: forall (a :: BOOL). Ob a => Booleans a (Booleans %% a) Source Github # | |||||
| Corepresentable (Fold :: Type -> Type -> Type) Source Github # | |||||
Defined in Proarrow.Profunctor.Instance.Fold 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 # corepUniv :: Ob a => Fold a ((Fold :: Type -> Type -> Type) %% a) Source Github # | |||||
| CategoryOf k => Corepresentable (Id :: k -> k -> Type) Source Github # | |||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k). Ob a => Id a ((Id :: k -> k -> Type) %% a) Source Github # | |||||
| Corepresentable (->) Source Github # | |||||
Defined in Proarrow.Profunctor.Corepresentable Associated Types
| |||||
| (HasInitialObject j, CategoryOf k) => Corepresentable (TerminalProfunctor :: k -> j -> Type) Source Github # | |||||
Defined in Proarrow.Colimit.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 # corepUniv :: forall (a :: k). Ob a => TerminalProfunctor a ((TerminalProfunctor :: k -> j -> Type) %% a) 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 | ||||
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 # corepUniv :: forall (a :: k). Ob a => Reader ('OP r) a (Reader ('OP r) %% a) Source Github # | |||||
| (Ob w, CompactClosed k) => Corepresentable (Writer w :: k -> k -> Type) Source Github # | The cowriter comonad given the Promonad instance. | ||||
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 # corepUniv :: forall (a :: k). Ob a => Writer w a (Writer w %% a) 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 | ||||
Defined in Proarrow.Category.Instance.Linear 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 # corepUniv :: Ob a => Rep Forget a (Rep Forget %% a) Source Github # | |||||
| Corepresentable (Star ((->) a) :: Type -> Type -> Type) Source Github # | The left adjoint of | ||||
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 # corepUniv :: Ob a0 => Star ((->) a) a0 (Star ((->) a) %% a0) Source Github # | |||||
| Corepresentable p => Corepresentable (Adj p :: k -> j -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: k). Ob a => Adj p a (Adj p %% a) Source Github # | |||||
| (Relation p, Representable p) => Corepresentable (Converse p :: k -> j -> Type) Source Github # | |||||
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 # | |||||
| FunctorForRep f => Corepresentable (Corep f :: k -> j -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: k). Ob a => Corep f a (Corep f %% a) Source Github # | |||||
| Functor f => Corepresentable (Costar f :: k -> j -> Type) Source Github # | |||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k). Ob a => Costar f a (Costar f %% a) Source Github # | |||||
| Corepresentable p => Corepresentable (Wrapped p :: k -> j -> Type) Source Github # | |||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k). Ob a => Wrapped p a (Wrapped p %% a) Source Github # | |||||
| Representable p => Corepresentable (RepCostar p :: k -> j -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: k). Ob a => RepCostar p a (RepCostar p %% a) Source Github # | |||||
| Corepresentable l => Corepresentable (AsLeftAdjoint l :: k -> j -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: k). Ob a => AsLeftAdjoint l a (AsLeftAdjoint l %% a) Source Github # | |||||
| (forall (a :: k). Ob a => InitUniversal a r, Representable r) => Corepresentable (AsRightAdjoint r :: k -> j -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: k). Ob a => AsRightAdjoint r a (AsRightAdjoint r %% a) Source Github # | |||||
| Corepresentable p => Corepresentable (FromAdjunction p :: k -> j -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: k). Ob a => FromAdjunction p a (FromAdjunction p %% a) Source Github # | |||||
| (Copowered v k, Ob n) => Corepresentable (GenArrow ('OP n) :: k -> k -> Type) Source Github # | |||||
Defined in Proarrow.Colimit.Copower Methods coindex :: forall (a :: k) (b :: k). GenArrow ('OP n) a b -> ((GenArrow ('OP n) :: k -> k -> Type) %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: k). Ob a => (((GenArrow ('OP n) :: k -> k -> Type) %% a) ~> b) -> GenArrow ('OP n) a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((GenArrow ('OP n) :: k -> k -> Type) %% a) ~> ((GenArrow ('OP n) :: k -> k -> Type) %% b) Source Github # corepUniv :: forall (a :: k). Ob a => GenArrow ('OP n) a ((GenArrow ('OP n) :: k -> k -> Type) %% a) Source Github # | |||||
| (Corepresentable p, Ob r, Monoidal k) => Corepresentable (ReaderT ('OP r) p :: k -> k -> Type) Source Github # | |||||
Defined in Proarrow.Promonad.Reader Methods coindex :: forall (a :: k) (b :: k). ReaderT ('OP r) p a b -> (ReaderT ('OP r) p %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: k). Ob a => ((ReaderT ('OP r) p %% a) ~> b) -> ReaderT ('OP r) p a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (ReaderT ('OP r) p %% a) ~> (ReaderT ('OP r) p %% b) Source Github # corepUniv :: forall (a :: k). Ob a => ReaderT ('OP r) p a (ReaderT ('OP r) p %% a) Source Github # | |||||
| (Corepresentable p, Ob s, Monoidal k, CompactClosed k) => Corepresentable (StateT s p :: k -> k -> Type) Source Github # | |||||
Defined in Proarrow.Promonad.State Methods coindex :: forall (a :: k) (b :: k). StateT s p a b -> (StateT s p %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: k). Ob a => ((StateT s p %% a) ~> b) -> StateT s p a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (StateT s p %% a) ~> (StateT s p %% b) Source Github # corepUniv :: forall (a :: k). Ob a => StateT s p a (StateT s p %% a) Source Github # | |||||
| (Corepresentable p, Ob w, CompactClosed k) => Corepresentable (WriterT w p :: k -> k -> Type) Source Github # | |||||
Defined in Proarrow.Promonad.Writer Methods coindex :: forall (a :: k) (b :: k). WriterT w p a b -> (WriterT w p %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: k). Ob a => ((WriterT w p %% a) ~> b) -> WriterT w p a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (WriterT w p %% a) ~> (WriterT w p %% b) Source Github # corepUniv :: forall (a :: k). Ob a => WriterT w p a (WriterT w p %% a) Source Github # | |||||
| (HasBinaryCoproducts j, Corepresentable p, Corepresentable q) => Corepresentable (p :*: q :: k -> j -> Type) Source Github # | |||||
Defined in Proarrow.Colimit.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 # corepUniv :: forall (a :: k). Ob a => (p :*: q) a ((p :*: q) %% a) Source Github # | |||||
| (Corepresentable p, Corepresentable q) => Corepresentable (p :.: q :: k -> j2 -> Type) Source Github # | |||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k). Ob a => (p :.: q) a ((p :.: q) %% a) Source Github # | |||||
| (HasColimits j k2, Corepresentable d) => Corepresentable (Rift ('OP j) d :: k1 -> k2 -> Type) Source Github # | |||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k1). Ob a => Rift ('OP j) d a (Rift ('OP j) d %% a) Source Github # | |||||
| HasBinaryCoproducts k => Corepresentable (Rep (Diag :: k +-> (k, k)) :: (k, k) -> k -> Type) Source Github # | The left adjoint to the diagonal functor. | ||||
Defined in Proarrow.Colimit.BinaryCoproduct Methods coindex :: forall (a :: (k, k)) (b :: k). Rep (Diag :: k +-> (k, k)) a b -> (Rep (Diag :: k +-> (k, k)) %% a) ~> b Source Github # cotabulate :: forall (a :: (k, k)) (b :: k). Ob a => ((Rep (Diag :: k +-> (k, k)) %% a) ~> b) -> Rep (Diag :: k +-> (k, k)) a b Source Github # corepMap :: forall (a :: (k, k)) (b :: (k, k)). (a ~> b) -> (Rep (Diag :: k +-> (k, k)) %% a) ~> (Rep (Diag :: k +-> (k, k)) %% b) Source Github # corepUniv :: forall (a :: (k, k)). Ob a => Rep (Diag :: k +-> (k, k)) a (Rep (Diag :: k +-> (k, k)) %% a) Source Github # | |||||
| (Closed k, SymMonoidal k, Ob r) => Corepresentable (Rep (Not r) :: k -> OPPOSITE k -> Type) Source Github # | The Op-Op adjunction, giving rise to the continuation monad. | ||||
Defined in Proarrow.Category.Monoidal.Closed Methods coindex :: forall (a :: k) (b :: OPPOSITE k). Rep (Not r) a b -> (Rep (Not r) %% a) ~> b Source Github # cotabulate :: forall (a :: k) (b :: OPPOSITE k). Ob a => ((Rep (Not r) %% a) ~> b) -> Rep (Not r) a b Source Github # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Rep (Not r) %% a) ~> (Rep (Not r) %% b) Source Github # corepUniv :: forall (a :: k). Ob a => Rep (Not r) a (Rep (Not r) %% a) Source Github # | |||||
| RealFloat a => Corepresentable (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) :: MatK (Complex a) -> MatK (Complex a) -> Type) Source Github # | Conjugation is a self-adjoint functor | ||||
Defined in Proarrow.Category.Instance.Mat Methods coindex :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 b -> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> b Source Github # cotabulate :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). Ob a0 => ((Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> b) -> Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 b Source Github # corepMap :: forall (a0 :: MatK (Complex a)) (b :: MatK (Complex a)). (a0 ~> b) -> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) ~> (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% b) Source Github # corepUniv :: forall (a0 :: MatK (Complex a)). Ob a0 => Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) a0 (Rep (Conjugate :: MatK (Complex a) +-> MatK (Complex a)) %% a0) Source Github # | |||||
| Representable p => Corepresentable (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # | |||||
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 # corepUniv :: forall (a :: OPPOSITE j). Ob a => Op p a (Op p %% a) 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. | ||||
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 # corepUniv :: forall (a :: k). Ob a => Rep (Forget ob) a (Rep (Forget ob) %% a) 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. | ||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k -> j1 -> Type). Ob a => Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) a (Star (Ran ('OP j2) :: (i +-> k) -> k -> j1 -> Type) %% a) 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. | ||||
Defined in Proarrow.Profunctor.Instance.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 # corepUniv :: forall (a :: k -> j1 -> Type). Ob a => Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) a (Star (Rift ('OP j2) :: (j1 +-> i) -> k -> j1 -> Type) %% a) Source Github # | |||||
| MonoidalAction t => Corepresentable (Star (Tambara t) :: (k -> k -> Type) -> (k +-> k) -> Type) Source Github # |
| ||||
Defined in Proarrow.Profunctor.Instance.PastroTambara Methods coindex :: forall (a :: k +-> k) (b :: k +-> k). Star (Tambara t) a b -> (Star (Tambara t) %% a) ~> b Source Github # cotabulate :: forall (a :: k +-> k) (b :: k +-> k). Ob a => ((Star (Tambara t) %% a) ~> b) -> Star (Tambara t) a b Source Github # corepMap :: forall (a :: k +-> k) (b :: k +-> k). (a ~> b) -> (Star (Tambara t) %% a) ~> (Star (Tambara t) %% b) Source Github # corepUniv :: forall (a :: k +-> k). Ob a => Star (Tambara t) a (Star (Tambara t) %% a) Source Github # | |||||
| HasColimits j k => Corepresentable (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Github # | |||||
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 # corepUniv :: forall (a0 :: COREPK b k). Ob a0 => LimitAdj j a0 ((LimitAdj j :: COREPK b k -> REPK a k -> Type) %% a0) Source Github # | |||||
| (Corepresentable p, Corepresentable q) => Corepresentable (p :++: q :: COPRODUCT k1 k2 -> COPRODUCT j1 j2 -> Type) Source Github # | |||||
Defined in Proarrow.Category.Instance.Coproduct Methods coindex :: forall (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2). (p :++: q) a b -> ((p :++: q) %% a) ~> b Source Github # cotabulate :: forall (a :: COPRODUCT k1 k2) (b :: COPRODUCT j1 j2). Ob a => (((p :++: q) %% a) ~> b) -> (p :++: q) a b Source Github # corepMap :: forall (a :: COPRODUCT k1 k2) (b :: COPRODUCT k1 k2). (a ~> b) -> ((p :++: q) %% a) ~> ((p :++: q) %% b) Source Github # corepUniv :: forall (a :: COPRODUCT k1 k2). Ob a => (p :++: q) a ((p :++: q) %% a) Source Github # | |||||
corepObj :: forall {k1} {k2} (p :: k1 +-> k2) (a :: k2). (Corepresentable p, Ob a) => Obj (p %% a) Source Github #
withObCorep :: 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 #
cotabulated :: forall {k1} {k2} p (a :: k2) (a' :: k2) (b :: k1) (b' :: k1). (Corepresentable p, Ob a) => Iso ((p %% a) ~> b) ((p %% a') ~> b') (p a b) (p a' b') Source Github #
type RepresentableCopresheaf (f :: Copresheaf k) = Corepresentable f Source Github #
A representable copresheaf is a representable functor in the Haskell sense.
tabulatedCopresheaf :: forall {k} f (a :: k) (a' :: k). (RepresentableCopresheaf f, Ob a) => Iso (Key f ~> a) (Key f ~> a') (f '() a) (f '() a') Source Github #
data Corep (f :: j +-> k) (a :: j) (b :: k) where Source Github #
Constructors
| Corep | |
Instances
| MonoidalProfunctor (Corep Forget) Source Github # | Forget is also a colax monoidal functor |
| (Monoidal k, Comonoid r) => MonoidalProfunctor (Corep (Constant r) :: k -> k -> Type) Source Github # | |
| FunctorForRep f => Profunctor (Corep f :: k -> j -> Type) Source Github # | |
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 # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> Corep f a b -> Corep f c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> Corep f a b -> Corep f a 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 # | |
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 # corepUniv :: forall (a :: k). Ob a => Corep f a (Corep f %% a) Source Github # | |
| FunctorForRep f => HasLimits (Corep f :: a -> i -> Type) k Source Github # | |
| FunctorForRep f => Proadjunction (Rep f :: k -> j -> Type) (Corep f :: j -> k -> Type) Source Github # | |
| HasCofree ob => Representable (Corep (Forget ob) :: SUBCAT ob -> k -> Type) Source Github # | By creating the right adjoint to the forgetful functor, we obtain the forgetful-cofree adjunction. |
Defined in Proarrow.Profunctor.Cofree Methods index :: forall (a :: SUBCAT ob) (b :: k). Corep (Forget ob) a b -> a ~> (Corep (Forget ob) % b) Source Github # tabulate :: forall (b :: k) (a :: SUBCAT ob). Ob b => (a ~> (Corep (Forget ob) % b)) -> Corep (Forget ob) a b Source Github # repMap :: forall (a :: k) (b :: k). (a ~> b) -> (Corep (Forget ob) % a) ~> (Corep (Forget ob) % b) Source Github # repUniv :: forall (a :: k). Ob a => Corep (Forget ob) (Corep (Forget ob) % a) a Source Github # | |
| HasBinaryProducts k => Representable (Corep (Diag :: k +-> (k, k)) :: k -> (k, k) -> Type) Source Github # | The right adjoint to the diagonal functor. |
Defined in Proarrow.Limit.BinaryProduct Methods index :: forall (a :: k) (b :: (k, k)). Corep (Diag :: k +-> (k, k)) a b -> a ~> (Corep (Diag :: k +-> (k, k)) % b) Source Github # tabulate :: forall (b :: (k, k)) (a :: k). Ob b => (a ~> (Corep (Diag :: k +-> (k, k)) % b)) -> Corep (Diag :: k +-> (k, k)) a b Source Github # repMap :: forall (a :: (k, k)) (b :: (k, k)). (a ~> b) -> (Corep (Diag :: k +-> (k, k)) % a) ~> (Corep (Diag :: k +-> (k, k)) % b) Source Github # repUniv :: forall (a :: (k, k)). Ob a => Corep (Diag :: k +-> (k, k)) (Corep (Diag :: k +-> (k, k)) % a) a Source Github # | |
| type Limit (Corep f :: a -> i -> Type) (d :: i +-> k) Source Github # | |
| type (Corep f :: k -> j -> Type) %% (a :: k) Source Github # | |
Defined in Proarrow.Profunctor.Corepresentable | |
| type (Corep (Forget ob) :: SUBCAT ob -> k -> Type) % (a :: k) Source Github # | |
| type (Corep (Diag :: k +-> (k, k)) :: k -> (k, k) -> Type) % ('(a, b) :: (k, k)) Source Github # | |