Safe Haskell	None
Language	GHC2024

Proarrow.Profunctor.Instance.Exponential

Contents

Orphan instances

Description

The internal hom of the category of profunctors under the product: a (p :~>: q) a b is a natural family of maps p c d -> q c d available at a/b, making PROD (j +-> k) Closed. j +-> k itself is Closed too, but for Day convolution and with a different hom (see Proarrow.Profunctor.Instance.Day). The PROD wrapper keeps the two apart.

Synopsis

data ((p :: k -> k1 -> Type) :~>: (q :: k -> k1 -> Type)) (a :: k) (b :: k1) where
- Exp :: forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type). (Ob a, Ob b) => (forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (p :~>: q) a b
class ob (p :~>: q) => IsObExp (ob :: OB (j +-> k)) (p :: k -> j -> Type) (q :: k -> j -> Type)

Documentation

data ((p :: k -> k1 -> Type) :~>: (q :: k -> k1 -> Type)) (a :: k) (b :: k1) where Source Github #

Constructors

Exp :: forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type). (Ob a, Ob b) => (forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d) -> (p :~>: q) a b

Instances

Instances details

(StableSite t k, Sheaf t q, Profunctor p, CategoryOf j) => Sheaf t (p :~>: q :: k -> j -> Type) Source Github #	The presheaf internal hom into a sheaf is already a sheaf: a matching family of maps `p -> q` over a cover glues pointwise, because the values glue in `q`. `p` needs no condition. The glued map, at an arrow `g` into `a`, pulls the cover back along `g` (`StableSite`). Each pulled-back leg factors through an original leg, whose map is asked, and the answers are glued in `q`. Neither `p` nor `q` has to be `Finitary`. The generic `glueBySearch` would be exponential in the size of `p`.
Instance details Defined in Proarrow.Category.Enriched.Finitary.Sheaf Methods glue :: forall (a :: k) c (b :: j). (Ob a, Ob b) => Cover t k a c -> (forall (x :: k). Leg t k a c x -> (p :~>: q) x b) -> (p :~>: q) a b Source Github #
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) => Finitary (p :~>: q :: k -> j -> Type) Source Github #	The internal hom of finitary profunctors is finitary: its elements are the natural transformations out of `ExpWeight`, enumerated. The count is not a formula in the sizes of `p` and `q`, since it depends on how the arrows of `j` and `k` compose. So `size` is a value and not a type family.
Instance details Defined in Proarrow.Category.Enriched.Finitary.Topos Methods size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => (p :~>: q) a b -> Natural Source Github # fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> (p :~>: q) a b Source Github # elements :: forall (a :: k) (b :: j). (Ob a, Ob b) => [(p :~>: q) a b] Source Github #
(DecidableProfunctor p, DecidableProfunctor q, Discrete j, Discrete k) => DecidableProfunctor (p :~>: q :: k -> j -> Type) Source Github #	Implication, decided: the exponential holds unless `p` holds and `q` does not. Against `p` an arrow of `p` is refuted by `noArrow`.
Instance details Defined in Proarrow.Profunctor.Instance.Exponential Methods decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (p :~>: q) a b (Holds (p :~>: q) a b) Source Github # toHolds :: forall (a :: k) (b :: j) r. (p :~>: q) a b -> ((Holds (p :~>: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
(ThinProfunctor p, ThinProfunctor q, Discrete j, Discrete k) => ThinProfunctor (p :~>: q :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Exponential Methods arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (p :~>: q) a b) => (p :~>: q) a b Source Github # withArr :: forall (a :: k) (b :: j) r. (p :~>: q) a b -> ((HasArrow (p :~>: q) a b, Ob a, Ob b) => r) -> r Source Github #
(Profunctor p, Profunctor q) => Profunctor (p :~>: q :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Exponential Methods dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> (p :~>: q) a b -> (p :~>: q) c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j). (c ~> a) -> (p :~>: q) a b -> (p :~>: q) c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: k). (b ~> d) -> (p :~>: q) a b -> (p :~>: q) a d Source Github # (\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> (p :~>: q) a b -> r Source Github #
type HasArrow (p :~>: q :: k -> j -> Type) (a :: k) (b :: j) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Exponential type HasArrow (p :~>: q :: k -> j -> Type) (a :: k) (b :: j) = HasArrow p a b :=> HasArrow q a b
type Holds (p :~>: q :: k -> j -> Type) (a :: k) (b :: j) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Exponential type Holds (p :~>: q :: k -> j -> Type) (a :: k) (b :: j) = BoolLeq (Holds p a b) (Holds q a b)

class ob (p :~>: q) => IsObExp (ob :: OB (j +-> k)) (p :: k -> j -> Type) (q :: k -> j -> Type) Source Github #

That a full subcategory of the profunctors contains the internal homs of its objects, as a class with a single instance, so that it can be the head of the quantified constraint below. IsObProd has the same shape for the product.

Instances

Instances details

ob (p :~>: q) => IsObExp (ob :: (k -> j -> Type) -> Constraint) (p :: k -> j -> Type) (q :: k -> j -> Type) Source Github #
Instance details Defined in Proarrow.Profunctor.Instance.Exponential

Orphan instances

(CategoryOf j, CategoryOf k, HasTerminalObject (SUBCAT ob), HasBinaryProducts (SUBCAT ob), forall (p :: j +-> k) (q :: j +-> k). (ob p, ob q) => IsObProd ob p q, forall (p :: j +-> k) (q :: j +-> k). (ob p, ob q) => IsObExp ob p q) => Closed (PROD (SUBCAT ob)) Source Github #	And then the subcategory is closed, with the ambient exponential and nothing of its own, just as its products are the ambient ones. `FINITARY j k` is one instance, `SHEAVES` another. For the first, a hom-set of natural transformations is finitary. For the second, an internal hom into a sheaf is a sheaf.
Instance details Methods withObExp :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github # curry :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob)) (c :: PROD (SUBCAT ob)). (Ob a, Ob b) => ((a b) ~> c) -> a ~> (b ~~> c) Source Github # apply :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob)). (Ob a, Ob b) => ((a ~~> b) a) ~> b Source Github # (^^^) :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob)) (x :: PROD (SUBCAT ob)) (y :: PROD (SUBCAT ob)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #
(CategoryOf j, CategoryOf k) => Closed (PROD (j +-> k)) Source Github #
Instance details Methods withObExp :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github # curry :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (c :: PROD (j +-> k)). (Ob a, Ob b) => ((a b) ~> c) -> a ~> (b ~~> c) Source Github # apply :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)). (Ob a, Ob b) => ((a ~~> b) a) ~> b Source Github # (^^^) :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) (x :: PROD (j +-> k)) (y :: PROD (j +-> k)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #