proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Monoidal.EndoProf

Description

The monoidal category of endo-profunctors on k under composition ((:.:)/Id), with functor composition as the tensor. This is the profunctor-specific counterpart of Proarrow.Category.Monoidal.Endo (in proarrow-equipment, which builds the analogous structure for an arbitrary Bicategory), hardcoded here to Prof/:.:/Id instead, and reusing Proarrow.Path's associators/unitors so they aren't proved twice.

Note this is a genuinely different monoidal structure on k +-> k than Proarrow.Profunctor.Instance.Day's Monoidal (j +-> k) instance (Day convolution) -- hence the need for a fresh wrapper type rather than another instance for the same kind.

Synopsis

Documentation

data ENDO k Source Github #

An object of ENDO k is an endo-profunctor k +-> k, i.e. (not necessarily representable) a functor k -> k under the profunctor encoding.

Constructors

E (k +-> k) 

Instances

Instances details
CategoryOf k => Monoidal (ENDO k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type Unit = 'E (Id :: k -> k -> Type)

Methods

withOb2 :: forall (a :: ENDO k) (b :: ENDO k) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: ENDO k). Ob a => ((Unit :: ENDO k) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: ENDO k). Ob a => a ~> ((Unit :: ENDO k) ** a) Source Github #

rightUnitor :: forall (a :: ENDO k). Ob a => (a ** (Unit :: ENDO k)) ~> a Source Github #

rightUnitorInv :: forall (a :: ENDO k). Ob a => a ~> (a ** (Unit :: ENDO k)) Source Github #

associator :: forall (a :: ENDO k) (b :: ENDO k) (c :: ENDO k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: ENDO k) (b :: ENDO k) (c :: ENDO k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

CategoryOf k => CategoryOf (ENDO k) Source Github #

The category of endoprofunctors on k and natural transformations between them.

Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (~>) = Endo :: ENDO k -> ENDO k -> Type
CategoryOf k => MonoidalAction (RepAction :: k -> (RepSub k, k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

unitor :: forall (x :: k). Ob x => Act (RepAction :: k -> (RepSub k, k) -> Type) (Unit :: RepSub k) x ~> x Source Github #

unitorInv :: forall (x :: k). Ob x => x ~> Act (RepAction :: k -> (RepSub k, k) -> Type) (Unit :: RepSub k) x Source Github #

multiplicator :: forall (a :: RepSub k) (b :: RepSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (RepAction :: k -> (RepSub k, k) -> Type) (a ** b) x ~> Act (RepAction :: k -> (RepSub k, k) -> Type) a (Act (RepAction :: k -> (RepSub k, k) -> Type) b x) Source Github #

multiplicatorInv :: forall (a :: RepSub k) (b :: RepSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (RepAction :: k -> (RepSub k, k) -> Type) a (Act (RepAction :: k -> (RepSub k, k) -> Type) b x) ~> Act (RepAction :: k -> (RepSub k, k) -> Type) (a ** b) x Source Github #

CategoryOf k => MonoidalAction (TravAction :: k -> (TravSub k, k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

unitor :: forall (x :: k). Ob x => Act (TravAction :: k -> (TravSub k, k) -> Type) (Unit :: TravSub k) x ~> x Source Github #

unitorInv :: forall (x :: k). Ob x => x ~> Act (TravAction :: k -> (TravSub k, k) -> Type) (Unit :: TravSub k) x Source Github #

multiplicator :: forall (a :: TravSub k) (b :: TravSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (TravAction :: k -> (TravSub k, k) -> Type) (a ** b) x ~> Act (TravAction :: k -> (TravSub k, k) -> Type) a (Act (TravAction :: k -> (TravSub k, k) -> Type) b x) Source Github #

multiplicatorInv :: forall (a :: TravSub k) (b :: TravSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (TravAction :: k -> (TravSub k, k) -> Type) a (Act (TravAction :: k -> (TravSub k, k) -> Type) b x) ~> Act (TravAction :: k -> (TravSub k, k) -> Type) (a ** b) x Source Github #

CategoryOf k => Promonad (Endo :: ENDO k -> ENDO k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

id :: forall (a :: ENDO k). Ob a => Endo a a Source Github #

(.) :: forall (b :: ENDO k) (c :: ENDO k) (a :: ENDO k). Endo b c -> Endo a b -> Endo a c Source Github #

CategoryOf k => MonoidalProfunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

one :: Endo (Unit :: ENDO k) (Unit :: ENDO k) Source Github #

(**) :: forall (x1 :: ENDO k) (x2 :: ENDO k) (y1 :: ENDO k) (y2 :: ENDO k). Endo x1 x2 -> Endo y1 y2 -> Endo (x1 ** y1) (x2 ** y2) Source Github #

CategoryOf k => Profunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

dimap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k) (d :: ENDO k). (c ~> a) -> (b ~> d) -> Endo a b -> Endo c d Source Github #

lmap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k). (c ~> a) -> Endo a b -> Endo c b Source Github #

rmap :: forall (b :: ENDO k) (d :: ENDO k) (a :: ENDO k). (b ~> d) -> Endo a b -> Endo a d Source Github #

(\\) :: forall (a :: ENDO k) (b :: ENDO k) r. ((Ob a, Ob b) => r) -> Endo a b -> r Source Github #

(CategoryOf h, CategoryOf x) => MonoidalAction (Rep Precomp :: (x +-> h) -> (REV (ENDO x), x +-> h) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

unitor :: forall (x0 :: x +-> h). Ob x0 => Act (Rep Precomp) (Unit :: REV (ENDO x)) x0 ~> x0 Source Github #

unitorInv :: forall (x0 :: x +-> h). Ob x0 => x0 ~> Act (Rep Precomp) (Unit :: REV (ENDO x)) x0 Source Github #

multiplicator :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x0 :: x +-> h). (Ob a, Ob b, Ob x0) => Act (Rep Precomp) (a ** b) x0 ~> Act (Rep Precomp) a (Act (Rep Precomp) b x0) Source Github #

multiplicatorInv :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x0 :: x +-> h). (Ob a, Ob b, Ob x0) => Act (Rep Precomp) a (Act (Rep Precomp) b x0) ~> Act (Rep Precomp) (a ** b) x0 Source Github #

CategoryOf k => FunctorForRep (RepAction' :: (RepSub k, k) +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

fmap :: forall (a :: (RepSub k, k)) (b :: (RepSub k, k)). (a ~> b) -> ((RepAction' :: (RepSub k, k) +-> k) @ a) ~> ((RepAction' :: (RepSub k, k) +-> k) @ b) Source Github #

CategoryOf k => FunctorForRep (TravAction' :: (TravSub k, k) +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

fmap :: forall (a :: (TravSub k, k)) (b :: (TravSub k, k)). (a ~> b) -> ((TravAction' :: (TravSub k, k) +-> k) @ a) ~> ((TravAction' :: (TravSub k, k) +-> k) @ b) Source Github #

(CategoryOf h, CategoryOf x) => FunctorForRep (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

fmap :: forall (a :: (REV (ENDO x), x +-> h)) (b :: (REV (ENDO x), x +-> h)). (a ~> b) -> (Precomp @ a) ~> (Precomp @ b) Source Github #

type Unit Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type Unit = 'E (Id :: k -> k -> Type)
type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (~>) = Endo :: ENDO k -> ENDO k -> Type
type Ob (a :: ENDO k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type Ob (a :: ENDO k) = (Is ('E :: (k +-> k) -> ENDO k) a, Profunctor (UN ('E :: (k +-> k) -> ENDO k) a))
type ('E p :: ENDO k) ** ('E q :: ENDO k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type ('E p :: ENDO k) ** ('E q :: ENDO k) = 'E (p :.: q)
type (RepAction' :: (RepSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), x) :: (SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (RepAction' :: (RepSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), x) :: (SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), k)) = p % x
type (TravAction' :: (TravSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), x) :: (SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (TravAction' :: (TravSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), x) :: (SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), k)) = p % x
type (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) @ ('('R ('E g), q) :: (REV (ENDO x), x +-> h)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) @ ('('R ('E g), q) :: (REV (ENDO x), x +-> h)) = q :.: g

data Endo (p :: ENDO k) (q :: ENDO k) where Source Github #

Morphisms of ENDO k are natural transformations between the underlying profunctors.

Constructors

Endo :: forall {k} (p1 :: k +-> k) (q1 :: k +-> k). (Profunctor p1, Profunctor q1) => (p1 :~> q1) -> Endo ('E p1) ('E q1) 

Instances

Instances details
CategoryOf k => Promonad (Endo :: ENDO k -> ENDO k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

id :: forall (a :: ENDO k). Ob a => Endo a a Source Github #

(.) :: forall (b :: ENDO k) (c :: ENDO k) (a :: ENDO k). Endo b c -> Endo a b -> Endo a c Source Github #

CategoryOf k => MonoidalProfunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

one :: Endo (Unit :: ENDO k) (Unit :: ENDO k) Source Github #

(**) :: forall (x1 :: ENDO k) (x2 :: ENDO k) (y1 :: ENDO k) (y2 :: ENDO k). Endo x1 x2 -> Endo y1 y2 -> Endo (x1 ** y1) (x2 ** y2) Source Github #

CategoryOf k => Profunctor (Endo :: ENDO k -> ENDO k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

dimap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k) (d :: ENDO k). (c ~> a) -> (b ~> d) -> Endo a b -> Endo c d Source Github #

lmap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k). (c ~> a) -> Endo a b -> Endo c b Source Github #

rmap :: forall (b :: ENDO k) (d :: ENDO k) (a :: ENDO k). (b ~> d) -> Endo a b -> Endo a d Source Github #

(\\) :: forall (a :: ENDO k) (b :: ENDO k) r. ((Ob a, Ob b) => r) -> Endo a b -> r Source Github #

class (Is ('E :: (k +-> k) -> ENDO k) a, c (UN ('E :: (k +-> k) -> ENDO k) a)) => OnE (c :: (k +-> k) -> Constraint) (a :: ENDO k) Source Github #

Lift a constraint on profunctors k +-> k to the corresponding ENDO objects.

Instances

Instances details
(Is ('E :: (k +-> k) -> ENDO k) a, c (UN ('E :: (k +-> k) -> ENDO k) a)) => OnE (c :: (k +-> k) -> Constraint) (a :: ENDO k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type RepSub k = SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)) Source Github #

The subcategory of representable endo-profunctors -- i.e. ordinary functors k -> k under the profunctor encoding. The most permissive restriction of ENDO for which an Action even makes sense (% needs Representable), so every other MonoidalAction on k embeds into this one -- see TravSub for a further restriction.

type RepAction = Rep (RepAction' :: (RepSub k, k) +-> k) Source Github #

The action of RepSub on k by application: Act RepAction (SUB (E f)) x = f % x.

data family RepAction' :: (RepSub k, k) +-> k Source Github #

Instances

Instances details
CategoryOf k => MonoidalAction (RepAction :: k -> (RepSub k, k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

unitor :: forall (x :: k). Ob x => Act (RepAction :: k -> (RepSub k, k) -> Type) (Unit :: RepSub k) x ~> x Source Github #

unitorInv :: forall (x :: k). Ob x => x ~> Act (RepAction :: k -> (RepSub k, k) -> Type) (Unit :: RepSub k) x Source Github #

multiplicator :: forall (a :: RepSub k) (b :: RepSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (RepAction :: k -> (RepSub k, k) -> Type) (a ** b) x ~> Act (RepAction :: k -> (RepSub k, k) -> Type) a (Act (RepAction :: k -> (RepSub k, k) -> Type) b x) Source Github #

multiplicatorInv :: forall (a :: RepSub k) (b :: RepSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (RepAction :: k -> (RepSub k, k) -> Type) a (Act (RepAction :: k -> (RepSub k, k) -> Type) b x) ~> Act (RepAction :: k -> (RepSub k, k) -> Type) (a ** b) x Source Github #

CategoryOf k => FunctorForRep (RepAction' :: (RepSub k, k) +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

fmap :: forall (a :: (RepSub k, k)) (b :: (RepSub k, k)). (a ~> b) -> ((RepAction' :: (RepSub k, k) +-> k) @ a) ~> ((RepAction' :: (RepSub k, k) +-> k) @ b) Source Github #

type (RepAction' :: (RepSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), x) :: (SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (RepAction' :: (RepSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), x) :: (SUBCAT (OnE (Representable :: (k +-> k) -> Constraint)), k)) = p % x

type TravSub k = SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))) Source Github #

The subcategory of representable, traversable endo-profunctors -- exactly the functors repTraverse can traverse with. Monoidal for free via Proarrow.Category.Instance.Sub's generic Monoidal (SUBCAT ob), since both Representable and Traversable already have instances closing them under :.:/Id.

type TravAction = Rep (TravAction' :: (TravSub k, k) +-> k) Source Github #

The action of TravSub on k by application: Act TravAction (SUB (E f)) x = f % x.

data family TravAction' :: (TravSub k, k) +-> k Source Github #

Instances

Instances details
CategoryOf k => MonoidalAction (TravAction :: k -> (TravSub k, k) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

unitor :: forall (x :: k). Ob x => Act (TravAction :: k -> (TravSub k, k) -> Type) (Unit :: TravSub k) x ~> x Source Github #

unitorInv :: forall (x :: k). Ob x => x ~> Act (TravAction :: k -> (TravSub k, k) -> Type) (Unit :: TravSub k) x Source Github #

multiplicator :: forall (a :: TravSub k) (b :: TravSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (TravAction :: k -> (TravSub k, k) -> Type) (a ** b) x ~> Act (TravAction :: k -> (TravSub k, k) -> Type) a (Act (TravAction :: k -> (TravSub k, k) -> Type) b x) Source Github #

multiplicatorInv :: forall (a :: TravSub k) (b :: TravSub k) (x :: k). (Ob a, Ob b, Ob x) => Act (TravAction :: k -> (TravSub k, k) -> Type) a (Act (TravAction :: k -> (TravSub k, k) -> Type) b x) ~> Act (TravAction :: k -> (TravSub k, k) -> Type) (a ** b) x Source Github #

CategoryOf k => FunctorForRep (TravAction' :: (TravSub k, k) +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

fmap :: forall (a :: (TravSub k, k)) (b :: (TravSub k, k)). (a ~> b) -> ((TravAction' :: (TravSub k, k) +-> k) @ a) ~> ((TravAction' :: (TravSub k, k) +-> k) @ b) Source Github #

type (TravAction' :: (TravSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), x) :: (SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), k)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (TravAction' :: (TravSub k, k) +-> k) @ ('('SUB ('E p) :: SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), x) :: (SUBCAT (OnE ((Representable :: (k +-> k) -> Constraint) :&&: (Traversable :: (k +-> k) -> Constraint))), k)) = p % x

data family Precomp :: forall x h. (REV (ENDO x), x +-> h) +-> (x +-> h) Source Github #

Endo-profunctors on x (any, not just representable ones) act on profunctors x +-> h by precomposition: Act Precomp (E g) q = q :.: g. Unlike RepAction/ TravAction, the acted-upon kind here isn't x or h itself but the whole profunctor kind x +-> h, so the witness g never has to be Representable -- only the assembled action (Rep Precomp) does, which is automatic. This is what lets toPrecompOptic turn any OpticSq (not just ones already shaped like an Action) into a genuine Optic.

The index category is REV (ENDO x), not ENDO x, because precomposition reverses the order composition happens in: ** on ENDO x composes its two arguments left-to-right, but composing two precomposition actions in sequence applies them right-to-left.

Instances

Instances details
(CategoryOf h, CategoryOf x) => MonoidalAction (Rep Precomp :: (x +-> h) -> (REV (ENDO x), x +-> h) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

unitor :: forall (x0 :: x +-> h). Ob x0 => Act (Rep Precomp) (Unit :: REV (ENDO x)) x0 ~> x0 Source Github #

unitorInv :: forall (x0 :: x +-> h). Ob x0 => x0 ~> Act (Rep Precomp) (Unit :: REV (ENDO x)) x0 Source Github #

multiplicator :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x0 :: x +-> h). (Ob a, Ob b, Ob x0) => Act (Rep Precomp) (a ** b) x0 ~> Act (Rep Precomp) a (Act (Rep Precomp) b x0) Source Github #

multiplicatorInv :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x0 :: x +-> h). (Ob a, Ob b, Ob x0) => Act (Rep Precomp) a (Act (Rep Precomp) b x0) ~> Act (Rep Precomp) (a ** b) x0 Source Github #

(CategoryOf h, CategoryOf x) => FunctorForRep (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

Methods

fmap :: forall (a :: (REV (ENDO x), x +-> h)) (b :: (REV (ENDO x), x +-> h)). (a ~> b) -> (Precomp @ a) ~> (Precomp @ b) Source Github #

type (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) @ ('('R ('E g), q) :: (REV (ENDO x), x +-> h)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.EndoProf

type (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) @ ('('R ('E g), q) :: (REV (ENDO x), x +-> h)) = q :.: g