Safe Haskell	None
Language	GHC2024

Proarrow.Profunctor.Instance.Yoneda

Contents

Orphan instances

Description

The Yoneda construction: Yoneda p is the cofree profunctor on an arbitrary type of kind j +-> k (the HasCofree instance for Profunctor), and Yo is the Yoneda embedding. By the Yoneda lemma Yoneda p is equivalent to p when p is already a profunctor (yoneda/mkYoneda).

Synopsis

data Yoneda (p :: j +-> k) (a :: k) (b :: j) where
- Yoneda :: forall {k} {j} (a :: k) (b :: j) (p :: j +-> k). (Ob a, Ob b) => {..} -> Yoneda p a b
yoneda :: forall j k (p :: j +-> k). (CategoryOf j, CategoryOf k) => Yoneda p :~> p
mkYoneda :: forall {j} {k} (p :: j +-> k). Profunctor p => p :~> Yoneda p
data Yo (a :: k) (b :: OPPOSITE j) (c :: k) (d :: j) where
- Yo :: forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j). (c ~> a) -> (b1 ~> d) -> Yo a ('OP b1) c d

Documentation

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

The cofree profunctor on p (the HasCofree instance for Profunctor): natural transformations out of the Yoneda embedding Yo. Equivalent to p when p is already a profunctor (yoneda/mkYoneda).

Constructors

Yoneda
Fields :: forall {k} {j} (a :: k) (b :: j) (p :: j +-> k). (Ob a, Ob b) => { unYoneda :: Yo a ('OP b) :~> p } -> Yoneda p a b

Instances

Instances details

(CategoryOf j, CategoryOf k) => Profunctor (Yoneda p :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> Yoneda p a b -> Yoneda p c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> Yoneda p a b -> Yoneda p c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> Yoneda p a b -> Yoneda p a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Yoneda p a b -> r Source Github #
Functor (Yoneda :: (j +-> k) -> k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> Yoneda a ~> Yoneda b Source Github #
Promonad (Costar (Yoneda :: (j +-> k) -> k -> j -> Type) :: (j +-> k) -> (k -> j -> Type) -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods id :: forall (a :: j +-> k). Ob a => Costar (Yoneda :: (j +-> k) -> k -> j -> Type) a a Source Github # (.) :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k). Costar (Yoneda :: (j +-> k) -> k -> j -> Type) b c -> Costar (Yoneda :: (j +-> k) -> k -> j -> Type) a b -> Costar (Yoneda :: (j +-> k) -> k -> j -> Type) a c Source Github #
Promonad (Star (Yoneda :: (j +-> k) -> k -> j -> Type) :: (k -> j -> Type) -> (j +-> k) -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods id :: forall (a :: k -> j -> Type). Ob a => Star (Yoneda :: (j +-> k) -> k -> j -> Type) a a Source Github # (.) :: forall (b :: k -> j -> Type) (c :: k -> j -> Type) (a :: k -> j -> Type). Star (Yoneda :: (j +-> k) -> k -> j -> Type) b c -> Star (Yoneda :: (j +-> k) -> k -> j -> Type) a b -> Star (Yoneda :: (j +-> k) -> k -> j -> Type) a c Source Github #

yoneda :: forall j k (p :: j +-> k). (CategoryOf j, CategoryOf k) => Yoneda p :~> p Source Github #

mkYoneda :: forall {j} {k} (p :: j +-> k). Profunctor p => p :~> Yoneda p Source Github #

data Yo (a :: k) (b :: OPPOSITE j) (c :: k) (d :: j) where Source Github #

Yoneda embedding

Constructors

Yo :: forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j). (c ~> a) -> (b1 ~> d) -> Yo a ('OP b1) c d

Instances

Instances details

(CategoryOf k, forall (p :: k +-> k) (q :: k +-> k). w p q => Sub (IsoFl :: (k +-> k) -> (k +-> k) -> Constraint) p q) => Prostrong (w :: FLAVOR k k) (Yo a ('OP b) :: k -> k -> Type) Source Github #	Any flavor whose optics are isos has strength for the `Yo` profunctor.
Instance details Defined in Proarrow.Optic.Iso Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (w f g, Profunctor f, Profunctor g) => ((f :.: Yo a ('OP b)) :.: g) :~> Yo a ('OP b) Source Github #
CategoryOf k => Prostrong (Flip (IsoFl :: (k +-> k) -> (k +-> k) -> Constraint) :: (k +-> k) -> (k +-> k) -> Constraint) (Yo a ('OP b) :: k -> k -> Type) Source Github #	`re`-versed isos are still isos: the same carrier eliminates them by reading the witness pair backwards. This is a conversion the subtyping lattice cannot express (the entailment `IsoFl q p => IsoFl p q` doesn't hold), but the carrier can compute it.
Instance details Defined in Proarrow.Optic.Iso Methods proact :: forall (f :: k +-> k) (g :: k +-> k). (Flip (IsoFl :: (k +-> k) -> (k +-> k) -> Constraint) f g, Profunctor f, Profunctor g) => ((f :.: Yo a ('OP b)) :.: g) :~> Yo a ('OP b) Source Github #
(FiniteCat j, FiniteCat k, Ob a, Ob b) => Finitary (Yo a ('OP b) :: k -> j -> Type) Source Github #	The embedding is finitary when the arrows are: its elements over `c`/`d` are an arrow `c ~> a` paired with an arrow `b ~> d`, numbered with the first varying slowest. This is the weight of the ends in Proarrow.Category.Enriched.Finitary.Topos, so it shares that module's `pairIndex` instead of spelling the radix out again.
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods size :: forall (a0 :: k) (b0 :: j). (Ob a0, Ob b0) => Natural Source Github # toIndex :: forall (a0 :: k) (b0 :: j). (Ob a0, Ob b0) => Yo a ('OP b) a0 b0 -> Natural Source Github # fromIndex :: forall (a0 :: k) (b0 :: j). (Ob a0, Ob b0) => Natural -> Yo a ('OP b) a0 b0 Source Github # elements :: forall (a0 :: k) (b0 :: j). (Ob a0, Ob b0) => [Yo a ('OP b) a0 b0] Source Github #
(CategoryOf j, CategoryOf k) => Profunctor (Yo a ('OP b) :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods dimap :: forall (c :: k) (a0 :: k) (b0 :: j) (d :: j). (c ~> a0) -> (b0 ~> d) -> Yo a ('OP b) a0 b0 -> Yo a ('OP b) c d Source Github # lmap :: forall (c :: k) (a0 :: k) (b0 :: j). (c ~> a0) -> Yo a ('OP b) a0 b0 -> Yo a ('OP b) c b0 Source Github # rmap :: forall (b0 :: j) (d :: j) (a0 :: k). (b0 ~> d) -> Yo a ('OP b) a0 b0 -> Yo a ('OP b) a0 d Source Github # (\\) :: forall (a0 :: k) (b0 :: j) r. ((Ob a0, Ob b0) => r) -> Yo a ('OP b) a0 b0 -> r Source Github #
(CategoryOf j, CategoryOf k) => Functor (Yo :: k -> OPPOSITE j -> k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods map :: forall (a :: k) (b :: k). (a ~> b) -> (Yo a :: OPPOSITE j -> k -> j -> Type) ~> (Yo b :: OPPOSITE j -> k -> j -> Type) Source Github #
(Elem HasBinaryCoproducts cs, Elem HasInitialObject cs, CategoryOf j) => Sheaf Sums (Yo x ('OP b) :: FREE cs p -> j -> Type) Source Github #	Sums are colimits, so the representables are sheaves for `Sums`: gluing is `\|\|\|` on the contravariant component. The initial object is needed too. An element of `Yo x (OP b)` also has a covariant component `b ~> d`. A family over the two injections has one per leg, and the glued element only one. Matching forces the two to agree because the injections overlap at the initial object, `lft . initiate = rgt . initiate`. Without it every family matches vacuously, and restriction fails for any `j` with a hom-set bigger than one.
Instance details Defined in Proarrow.Category.Sheaf Methods glue :: forall (a :: FREE cs p) c (b0 :: j). (Ob a, Ob b0) => Cover Sums (FREE cs p) a c -> (forall (x0 :: FREE cs p). Leg Sums (FREE cs p) a c x0 -> Yo x ('OP b) x0 b0) -> Yo x ('OP b) a b0 Source Github #
(CategoryOf j, CategoryOf k) => Functor (Yo a :: OPPOSITE j -> k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Yoneda Methods map :: forall (a0 :: OPPOSITE j) (b :: OPPOSITE j). (a0 ~> b) -> Yo a a0 ~> Yo a b Source Github #

Orphan instances

HasCofree (Profunctor :: (j +-> k) -> Constraint) Source Github #
Instance details Methods lower :: forall (a :: j +-> k). Ob a => Cofree (Profunctor :: (j +-> k) -> Constraint) a ~> a Source Github # unfoldMap :: forall (a :: j +-> k) (b :: j +-> k). Profunctor a => (a ~> b) -> a ~> Cofree (Profunctor :: (j +-> k) -> Constraint) b Source Github #