proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Instance.Sub

Description

Full subcategories: the kind SUBCAT ob restricts a category to the objects satisfying the predicate ob, with Sub wrapping the underlying arrows unchanged. This is how object constraints beyond a kind's own Ob are imposed (e.g. the category of representable profunctors in Proarrow.Category.Instance.Rep).

Synopsis

Documentation

data SUBCAT (ob :: OB k) Source Github #

Constructors

SUB k 

Instances

Instances details
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.

Instance details

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 #

(FiniteCat j, FiniteCat k) => Closed (PROD (FINITARY j k)) Source Github #

Finitary profunctors are cartesian closed. The PROD wrapper is what makes the tensor the product rather than Day convolution, exactly as it does for j +-> k itself.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

withObExp :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)) (c :: PROD (FINITARY j k)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)) (x :: PROD (FINITARY j k)) (y :: PROD (FINITARY j k)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

(FiniteCat j, FiniteCat k) => ElementaryTopos (PROD (FINITARY j k)) Source Github #

Finitary profunctors between finite categories form an elementary topos: finite limits and colimits, cartesian closed, a subobject classifier, and image factorization.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

(FiniteCat j, FiniteCat k) => HasSubobjectClassifier (PROD (FINITARY j k)) Source Github #

The subobject classifier is the profunctor of sieves, and an arrow classifies its graph: the sieve of all the ways an element of p and one of q can be carried to a matching pair.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Associated Types

type Omega 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type Omega = 'PR ('SUB (Sieve :: k -> j -> Type) :: SUBCAT (Finitary :: (j +-> k) -> Constraint))

Methods

true :: (TerminalObject :: PROD (FINITARY j k)) ~> (Omega :: PROD (FINITARY j k)) Source Github #

classifyGraph :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)). (a ~> b) -> (a && b) ~> (Omega :: PROD (FINITARY j k)) Source Github #

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 #

EnrichedProfunctor v p => EnrichedProfunctor (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched

Methods

withProObj :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. (Ob a, Ob b) => (Ob (ProObj (Clone v) (Op p) a b) => r) -> r Source Github #

underlying :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). Op p a b -> (Unit :: Clone v) ~> ProObj (Clone v) (Op p) a b Source Github #

enriched :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => ((Unit :: Clone v) ~> ProObj (Clone v) (Op p) a b) -> Op p a b Source Github #

rmap :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) (c :: OPPOSITE k). (Ob a, Ob b, Ob c) => (HomObj (Clone v) b c ** ProObj (Clone v) (Op p) a b) ~> ProObj (Clone v) (Op p) a c Source Github #

lmap :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) (c :: OPPOSITE j). (Ob a, Ob b, Ob c) => (HomObj (Clone v) c a ** ProObj (Clone v) (Op p) a b) ~> ProObj (Clone v) (Op p) c b Source Github #

SubMonoidal ob => Monoidal (SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Associated Types

type Unit 
Instance details

Defined in Proarrow.Category.Instance.Sub

type Unit = 'SUB (Unit :: k) :: SUBCAT ob

Methods

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

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

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

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

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

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

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

(SymMonoidal k, SubMonoidal ob) => SymMonoidal (SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

swap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

(SubMonoidal ob, CopyDiscard k) => CopyDiscard (SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.CopyDiscard

Methods

copy :: forall (a :: SUBCAT ob). Ob a => a ~> (a ** a) Source Github #

discard :: forall (a :: SUBCAT ob). Ob a => a ~> (Unit :: SUBCAT ob) Source Github #

(Enumerable j, Enumerable k) => HasEpiMonoFactorization (FINITARY j k) Source Github #

The image of a natural transformation is the equalizer of its cokernel pair.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

factorize :: forall (a :: FINITARY j k) (b :: FINITARY j k). (a ~> b) -> (Hom (FINITARY j k) :.: Hom (FINITARY j k)) a b Source Github #

(CategoryOf j, CategoryOf k) => HasBinaryCoproducts (FINITARY j k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

withObCoprod :: forall (a :: FINITARY j k) (b :: FINITARY j k) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: FINITARY j k) (a :: FINITARY j k) (y :: FINITARY j k). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: FINITARY j k) (b :: FINITARY j k) (x :: FINITARY j k) (y :: FINITARY j k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

(Enumerable j, Enumerable k) => HasCoequalizers (FINITARY j k) Source Github #

Coequalizers: at each pair of objects, partition the indices by the equivalence relation the two natural transformations generate, and reify the table. Naturality makes the partition a congruence, so the quotient is again a profunctor.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

coequalize :: forall (a :: FINITARY j k) (b :: FINITARY j k) r. (a ~> b) -> (a ~> b) -> (forall (c :: FINITARY j k). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: FINITARY j k) (x :: FINITARY j k) (c' :: FINITARY j k). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

(CategoryOf j, CategoryOf k) => HasInitialObject (FINITARY j k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Associated Types

type InitialObject 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type InitialObject = FIN (InitialProfunctor :: k -> j -> Type)

Methods

initiate :: forall (a :: FINITARY j k). Ob a => (InitialObject :: FINITARY j k) ~> a Source Github #

(Enumerable j, Enumerable k) => HasPushouts (FINITARY j k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

pushout :: forall (o :: FINITARY j k) (a :: FINITARY j k) (b :: FINITARY j k) r. (o ~> a) -> (o ~> b) -> (forall (p :: FINITARY j k). (a ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a :: FINITARY j k) (b :: FINITARY j k) (p :: FINITARY j k) (q :: FINITARY j k). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

CategoryOf k => CategoryOf (SUBCAT ob) Source Github #

The subcategory with objects with instances of the given constraint ob.

Instance details

Defined in Proarrow.Category.Instance.Sub

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (~>) = Sub ((~>) :: CAT k) :: SUBCAT ob -> SUBCAT ob -> Type
(CategoryOf j, CategoryOf k) => HasBinaryProducts (FINITARY j k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

withObProd :: forall (a :: FINITARY j k) (b :: FINITARY j k) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: FINITARY j k) (x :: FINITARY j k) (y :: FINITARY j k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: FINITARY j k) (b :: FINITARY j k) (x :: FINITARY j k) (y :: FINITARY j k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

(Enumerable j, Enumerable k) => HasEqualizers (FINITARY j k) Source Github #

Equalizers of finitary profunctors between finite categories: at each pair of objects, keep the indices on which the two natural transformations agree, and reify the table.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

equalize :: forall (a :: FINITARY j k) (b :: FINITARY j k) r. (a ~> b) -> (a ~> b) -> (forall (e :: FINITARY j k). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (e :: FINITARY j k) (x :: FINITARY j k) (e' :: FINITARY j k). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

(Enumerable j, Enumerable k) => HasPullbacks (FINITARY j k) Source Github #

Pullbacks are equalizers of products, and pushouts coequalizers of coproducts, all of which finitary profunctors have.

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

pullback :: forall (o :: FINITARY j k) (a :: FINITARY j k) (b :: FINITARY j k) r. (a ~> o) -> (b ~> o) -> (forall (p :: FINITARY j k). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a :: FINITARY j k) (b :: FINITARY j k) (p :: FINITARY j k) (q :: FINITARY j k). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

(CategoryOf j, CategoryOf k) => HasTerminalObject (FINITARY j k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Associated Types

type TerminalObject 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type TerminalObject = FIN (TerminalProfunctor :: k -> j -> Type)

Methods

terminate :: forall (a :: FINITARY j k). Ob a => a ~> (TerminalObject :: FINITARY j k) Source Github #

(FiniteCat j, FiniteCat k) => HasPushoutComplements (FINITARY j k) Source Github #

Pushout complements of finitary profunctors, for any finite schema at all -- so double-pushout rewriting of graphs, typed graphs, or the rows of a database, in one instance.

The gluing condition splits into exactly its two classical halves, neither of which has to mention graphs:

  • an identification conflict is the match identifying two elements that the rule does not both keep -- either a kept element with a deleted one, or two distinct deleted ones -- and
  • the dangling condition is that the surviving elements are closed under the action of the schema's arrows -- which is precisely the statement that they form a subprofunctor, and hence that Reindex can carve them out at all. For the two-object schema E -> V it says that a surviving edge still has both its endpoints, which is where the classical name comes from.
Instance details

Defined in Proarrow.Tools.DPO

Methods

pushoutComplement :: forall (a :: FINITARY j k) (l :: FINITARY j k) (g :: FINITARY j k) ans. (a ~> l) -> (l ~> g) -> (forall (d :: FINITARY j k). (a ~> d) -> (d ~> g) -> ans) -> ans -> ans Source Github #

(SubMonoidal ob, CopyDiscard k, Ob a) => CocommutativeComonoid (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.CopyDiscard

(SubMonoidal ob, CopyDiscard k, Ob a) => Comonoid (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.CopyDiscard

Methods

counit :: a ~> (Unit :: SUBCAT ob) Source Github #

comult :: a ~> (a ** a) 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 k => FunctorForRep (Forget ob :: SUBCAT ob +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

fmap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (a ~> b) -> (Forget ob @ a) ~> (Forget ob @ 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 #

corepUniv :: forall (a :: k). Ob a => Rep (Forget ob) a (Rep (Forget ob) %% a) Source Github #

(Monoidal k2, Monoidal (SUBCAT ob), MonoidalAction t) => MonoidalAction (SubAction ob t :: k1 -> (SUBCAT ob, k1) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

Methods

unitor :: forall (x :: k1). Ob x => Act (SubAction ob t) (Unit :: SUBCAT ob) x ~> x Source Github #

unitorInv :: forall (x :: k1). Ob x => x ~> Act (SubAction ob t) (Unit :: SUBCAT ob) x Source Github #

multiplicator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: k1). (Ob a, Ob b, Ob x) => Act (SubAction ob t) (a ** b) x ~> Act (SubAction ob t) a (Act (SubAction ob t) b x) Source Github #

multiplicatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: k1). (Ob a, Ob b, Ob x) => Act (SubAction ob t) a (Act (SubAction ob t) b x) ~> Act (SubAction ob t) (a ** b) x Source Github #

(Monoidal k2, Monoidal (SUBCAT ob), Representable t) => FunctorForRep (SubAction' ob t :: (SUBCAT ob, k1) +-> k1) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

Methods

fmap :: forall (a :: (SUBCAT ob, k1)) (b :: (SUBCAT ob, k1)). (a ~> b) -> (SubAction' ob t @ a) ~> (SubAction' ob t @ b) Source Github #

Applicative f => Strong (SubAction Traversable ApplyAction) (Star (Prelude f) :: Type -> Type -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Star

Methods

act :: forall (a :: SUBCAT Traversable) x y. Ob a => Star (Prelude f) x y -> Star (Prelude f) (Act (SubAction Traversable ApplyAction) a x) (Act (SubAction Traversable ApplyAction) a y) Source Github #

Monoid m => EnrichedProfunctor (Clone k) (Mon :: MONOID m -> MONOID m -> Type) Source Github #

A monoid is a one object enriched category.

Instance details

Defined in Proarrow.Category.Enriched

Methods

withProObj :: forall (a :: MONOID m) (b :: MONOID m) r. (Ob a, Ob b) => (Ob (ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) => r) -> r Source Github #

underlying :: forall (a :: MONOID m) (b :: MONOID m). Mon a b -> (Unit :: Clone k) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b Source Github #

enriched :: forall (a :: MONOID m) (b :: MONOID m). (Ob a, Ob b) => ((Unit :: Clone k) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) -> Mon a b Source Github #

rmap :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m). (Ob a, Ob b, Ob c) => (HomObj (Clone k) b c ** ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a c Source Github #

lmap :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m). (Ob a, Ob b, Ob c) => (HomObj (Clone k) c a ** ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) a b) ~> ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) c b Source Github #

(FiniteCat j, FiniteCat k) => Finitary (Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) :: SUBCAT (Finitary :: (j +-> k) -> Constraint) -> SUBCAT (Finitary :: (j +-> k) -> Constraint) -> Type) Source Github #

FINITARY j k is locally finite: its own hom-profunctor is finitary, by natTransformations. So the numbering above is not just a testing device, it is the skeleton of each hom-set, and the Finitary laws apply to it like to any other. (It is not a FiniteCat -- there are unboundedly many finitary profunctors -- which is exactly the difference between finite and locally finite.)

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

size :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b -> Natural Source Github #

fromIndex :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => Natural -> Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b Source Github #

elements :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => [Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b] Source Github #

(MonoidalProfunctor p, SubMonoidal ob) => MonoidalProfunctor (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

one :: Sub p (Unit :: SUBCAT ob) (Unit :: SUBCAT ob) Source Github #

(**) :: forall (x1 :: SUBCAT ob) (x2 :: SUBCAT ob) (y1 :: SUBCAT ob) (y2 :: SUBCAT ob). Sub p x1 x2 -> Sub p y1 y2 -> Sub p (x1 ** y1) (x2 ** y2) Source Github #

Profunctor p => Profunctor (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob) (d :: SUBCAT ob). (c ~> a) -> (b ~> d) -> Sub p a b -> Sub p c d Source Github #

lmap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob). (c ~> a) -> Sub p a b -> Sub p c b Source Github #

rmap :: forall (b :: SUBCAT ob) (d :: SUBCAT ob) (a :: SUBCAT ob). (b ~> d) -> Sub p a b -> Sub p a d Source Github #

(\\) :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r. ((Ob a, Ob b) => r) -> Sub p a b -> r Source Github #

(Representable p, forall (a :: k). ob a => ob (p % a)) => Representable (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

index :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). Sub p a b -> a ~> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % b) Source Github #

tabulate :: forall (b :: SUBCAT ob) (a :: SUBCAT ob). Ob b => (a ~> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % b)) -> Sub p a b Source Github #

repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (a ~> b) -> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % a) ~> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % b) Source Github #

repUniv :: forall (a :: SUBCAT ob). Ob a => Sub p ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % a) a Source Github #

Profunctor j => Profunctor (LimitAdj j :: COREPK b k -> REPK a k -> Type) Source Github # 
Instance details

Defined in Proarrow.Adjunction

Methods

dimap :: forall (c :: COREPK b k) (a0 :: COREPK b k) (b0 :: REPK a k) (d :: REPK a k). (c ~> a0) -> (b0 ~> d) -> LimitAdj j a0 b0 -> LimitAdj j c d Source Github #

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

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

(\\) :: forall (a0 :: COREPK b k) (b0 :: REPK a k) r. ((Ob a0, Ob b0) => r) -> LimitAdj j a0 b0 -> r 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 #

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

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

Colimit j ⊣ Limit j

Instance details

Defined in Proarrow.Adjunction

Methods

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

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

repMap :: forall (a0 :: REPK a k) (b0 :: REPK a 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 #

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

Promonad p => Promonad (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

id :: forall (a :: SUBCAT ob). Ob a => Sub p a a Source Github #

(.) :: forall (b :: SUBCAT ob) (c :: SUBCAT ob) (a :: SUBCAT ob). Sub p b c -> Sub p a b -> Sub p a c Source Github #

HasFree (On Monoid Semigroup) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Free

Associated Types

type Free (On Monoid Semigroup) ('SUB a :: SUBCAT Semigroup) 
Instance details

Defined in Proarrow.Profunctor.Free

type Free (On Monoid Semigroup) ('SUB a :: SUBCAT Semigroup) = 'SUB (Maybe a) :: SUBCAT Semigroup

Methods

lift :: forall (a :: SUBCAT Semigroup). Ob a => a ~> Free (On Monoid Semigroup) a Source Github #

foldMap :: forall (b :: SUBCAT Semigroup) (a :: SUBCAT Semigroup). On Monoid Semigroup b => (a ~> b) -> Free (On Monoid Semigroup) a ~> b Source Github #

type (Rep (Forget ob) :: k -> SUBCAT ob -> Type) %% (a :: k) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Free

type (Rep (Forget ob) :: k -> SUBCAT ob -> Type) %% (a :: k) = 'SUB (Free ob a) :: SUBCAT ob
type (Corep (Forget ob) :: SUBCAT ob -> k -> Type) % (a :: k) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Cofree

type (Corep (Forget ob) :: SUBCAT ob -> k -> Type) % (a :: k) = 'SUB (Cofree ob a) :: SUBCAT ob
type Omega Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type Omega = 'PR ('SUB (Sieve :: k -> j -> Type) :: SUBCAT (Finitary :: (j +-> k) -> Constraint))
type (p :: PROD (SUBCAT (Finitary :: (j +-> k) -> Constraint))) ~~> (q :: PROD (SUBCAT (Finitary :: (j +-> k) -> Constraint))) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type (p :: PROD (SUBCAT (Finitary :: (j +-> k) -> Constraint))) ~~> (q :: PROD (SUBCAT (Finitary :: (j +-> k) -> Constraint))) = 'PR ('SUB (UN ('SUB :: (k -> j -> Type) -> SUBCAT (Finitary :: (j +-> k) -> Constraint)) (UN ('PR :: SUBCAT (Finitary :: (j +-> k) -> Constraint) -> PROD (SUBCAT (Finitary :: (j +-> k) -> Constraint))) p) :~>: UN ('SUB :: (k -> j -> Type) -> SUBCAT (Finitary :: (j +-> k) -> Constraint)) (UN ('PR :: SUBCAT (Finitary :: (j +-> k) -> Constraint) -> PROD (SUBCAT (Finitary :: (j +-> k) -> Constraint))) q)) :: SUBCAT (Finitary :: (j +-> k) -> Constraint))
type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched

type ProObj (Clone v) (Op p :: OPPOSITE j -> OPPOSITE k -> Type) ('OP a :: OPPOSITE j) ('OP b :: OPPOSITE k) = 'SUB (ProObj v p b a) :: SUBCAT (Any :: v -> Constraint)
type Unit Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type Unit = 'SUB (Unit :: k) :: SUBCAT ob
type InitialObject Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type InitialObject = FIN (InitialProfunctor :: k -> j -> Type)
type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (~>) = Sub ((~>) :: CAT k) :: SUBCAT ob -> SUBCAT ob -> Type
type TerminalObject Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type TerminalObject = FIN (TerminalProfunctor :: k -> j -> Type)
type Ob (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type Ob (a :: SUBCAT ob) = (WrappedOb ('SUB :: k -> SUBCAT ob) a, ob (UN ('SUB :: k -> SUBCAT ob) a))
type (a :: SUBCAT ob) ** (b :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (a :: SUBCAT ob) ** (b :: SUBCAT ob) = 'SUB (UN ('SUB :: k -> SUBCAT ob) a ** UN ('SUB :: k -> SUBCAT ob) b) :: SUBCAT ob
type (a :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) || (b :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type (a :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) || (b :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) = 'SUB (UN ('SUB :: (j +-> k) -> SUBCAT (Finitary :: (j +-> k) -> Constraint)) a :+: UN ('SUB :: (j +-> k) -> SUBCAT (Finitary :: (j +-> k) -> Constraint)) b) :: SUBCAT (Finitary :: (j +-> k) -> Constraint)
type (a :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) && (b :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

type (a :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) && (b :: SUBCAT (Finitary :: (j +-> k) -> Constraint)) = 'SUB (UN ('SUB :: (j +-> k) -> SUBCAT (Finitary :: (j +-> k) -> Constraint)) a :*: UN ('SUB :: (j +-> k) -> SUBCAT (Finitary :: (j +-> k) -> Constraint)) b) :: SUBCAT (Finitary :: (j +-> k) -> Constraint)
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 (Forget ob :: SUBCAT ob +-> k) @ (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (Forget ob :: SUBCAT ob +-> k) @ (a :: SUBCAT ob) = UN ('SUB :: k -> SUBCAT ob) a
type (SubAction' ob t :: (SUBCAT ob, k2) +-> k2) @ ('('SUB a :: SUBCAT ob, x) :: (SUBCAT ob, k2)) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Action

type (SubAction' ob t :: (SUBCAT ob, k2) +-> k2) @ ('('SUB a :: SUBCAT ob, x) :: (SUBCAT ob, k2)) = t % '(a, x)
type ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) ('M :: MONOID m) ('M :: MONOID m) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched

type ProObj (Clone k) (Mon :: MONOID m -> MONOID m -> Type) ('M :: MONOID m) ('M :: MONOID m) = 'SUB m :: SUBCAT (Any :: k -> Constraint)
type (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % (a :: SUBCAT ob) = 'SUB (p % UN ('SUB :: k -> SUBCAT ob) a) :: SUBCAT ob
type (LimitAdj j :: COREPK b k -> REPK a k -> Type) %% (c :: COREPK b k) Source Github # 
Instance details

Defined in Proarrow.Adjunction

type (LimitAdj j :: COREPK b k -> REPK a k -> Type) %% (c :: COREPK b k) = REP (CorepStar (Colimit j (UN ('OP :: (k +-> b) -> OPPOSITE (k +-> b)) (UN ('SUB :: OPPOSITE (k +-> b) -> SUBCAT (OpCorepresentable :: OPPOSITE (k +-> b) -> Constraint)) c))))
type (LimitAdj j :: COREPK b k -> REPK a k -> Type) % (r :: REPK a k) Source Github # 
Instance details

Defined in Proarrow.Adjunction

type (LimitAdj j :: COREPK b k -> REPK a k -> Type) % (r :: REPK a k) = COREP (RepCostar (Limit j (UN ('SUB :: (a +-> k) -> SUBCAT (Representable :: (a +-> k) -> Constraint)) r)))
type Free (On Monoid Semigroup) ('SUB a :: SUBCAT Semigroup) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Free

type Free (On Monoid Semigroup) ('SUB a :: SUBCAT Semigroup) = 'SUB (Maybe a) :: SUBCAT Semigroup

data Sub (p :: CAT k) (a :: SUBCAT ob) (b :: SUBCAT ob) where Source Github #

Wraps an arrow whose endpoints satisfy the predicate ob: the arrows of the full subcategory SUBCAT.

Constructors

Sub 

Fields

  • :: forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k). (ob a1, ob b1)
     
  • => { unSub :: p a1 b1
     
  •    } -> Sub p ('SUB a1 :: SUBCAT ob) ('SUB b1 :: SUBCAT ob)
     

Instances

Instances details
(FiniteCat j, FiniteCat k) => Finitary (Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) :: SUBCAT (Finitary :: (j +-> k) -> Constraint) -> SUBCAT (Finitary :: (j +-> k) -> Constraint) -> Type) Source Github #

FINITARY j k is locally finite: its own hom-profunctor is finitary, by natTransformations. So the numbering above is not just a testing device, it is the skeleton of each hom-set, and the Finitary laws apply to it like to any other. (It is not a FiniteCat -- there are unboundedly many finitary profunctors -- which is exactly the difference between finite and locally finite.)

Instance details

Defined in Proarrow.Category.Enriched.Finitary.Topos

Methods

size :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b -> Natural Source Github #

fromIndex :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => Natural -> Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b Source Github #

elements :: forall (a :: FINITARY j k) (b :: FINITARY j k). (Ob a, Ob b) => [Sub (Prof :: (j +-> k) -> (j +-> k) -> Type) a b] Source Github #

(MonoidalProfunctor p, SubMonoidal ob) => MonoidalProfunctor (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

one :: Sub p (Unit :: SUBCAT ob) (Unit :: SUBCAT ob) Source Github #

(**) :: forall (x1 :: SUBCAT ob) (x2 :: SUBCAT ob) (y1 :: SUBCAT ob) (y2 :: SUBCAT ob). Sub p x1 x2 -> Sub p y1 y2 -> Sub p (x1 ** y1) (x2 ** y2) Source Github #

Profunctor p => Profunctor (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob) (d :: SUBCAT ob). (c ~> a) -> (b ~> d) -> Sub p a b -> Sub p c d Source Github #

lmap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob). (c ~> a) -> Sub p a b -> Sub p c b Source Github #

rmap :: forall (b :: SUBCAT ob) (d :: SUBCAT ob) (a :: SUBCAT ob). (b ~> d) -> Sub p a b -> Sub p a d Source Github #

(\\) :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r. ((Ob a, Ob b) => r) -> Sub p a b -> r Source Github #

(Representable p, forall (a :: k). ob a => ob (p % a)) => Representable (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

index :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). Sub p a b -> a ~> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % b) Source Github #

tabulate :: forall (b :: SUBCAT ob) (a :: SUBCAT ob). Ob b => (a ~> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % b)) -> Sub p a b Source Github #

repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (a ~> b) -> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % a) ~> ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % b) Source Github #

repUniv :: forall (a :: SUBCAT ob). Ob a => Sub p ((Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % a) a Source Github #

Promonad p => Promonad (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

id :: forall (a :: SUBCAT ob). Ob a => Sub p a a Source Github #

(.) :: forall (b :: SUBCAT ob) (c :: SUBCAT ob) (a :: SUBCAT ob). Sub p b c -> Sub p a b -> Sub p a c Source Github #

type (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (Sub p :: SUBCAT ob -> SUBCAT ob -> Type) % (a :: SUBCAT ob) = 'SUB (p % UN ('SUB :: k -> SUBCAT ob) a) :: SUBCAT ob

class c (UN ('SUB :: k -> SUBCAT ob) a) => On (c :: k -> Constraint) (ob :: OB k) (a :: SUBCAT ob) Source Github #

Instances

Instances details
c (UN ('SUB :: k -> SUBCAT ob) a) => On (c :: k -> Constraint) (ob :: OB k) (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

class ob (a ** b) => IsObMult (ob :: OB k) (a :: k) (b :: k) Source Github #

Instances

Instances details
ob (a ** b) => IsObMult (ob :: k -> Constraint) (a :: k) (b :: k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

class (Monoidal k, ob (Unit :: k), forall (a :: k) (b :: k). (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k) Source Github #

Instances

Instances details
(Monoidal k, ob (Unit :: k), forall (a :: k) (b :: k). (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: k -> Constraint) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

data family Forget :: forall (ob :: OB k) -> SUBCAT ob +-> k Source Github #

Instances

Instances details
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.

Instance details

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 #

CategoryOf k => FunctorForRep (Forget ob :: SUBCAT ob +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

Methods

fmap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (a ~> b) -> (Forget ob @ a) ~> (Forget ob @ 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 #

corepUniv :: forall (a :: k). Ob a => Rep (Forget ob) a (Rep (Forget ob) %% a) Source Github #

type (Rep (Forget ob) :: k -> SUBCAT ob -> Type) %% (a :: k) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Free

type (Rep (Forget ob) :: k -> SUBCAT ob -> Type) %% (a :: k) = 'SUB (Free ob a) :: SUBCAT ob
type (Corep (Forget ob) :: SUBCAT ob -> k -> Type) % (a :: k) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Cofree

type (Corep (Forget ob) :: SUBCAT ob -> k -> Type) % (a :: k) = 'SUB (Cofree ob a) :: SUBCAT ob
type (Forget ob :: SUBCAT ob +-> k) @ (a :: SUBCAT ob) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Sub

type (Forget ob :: SUBCAT ob +-> k) @ (a :: SUBCAT ob) = UN ('SUB :: k -> SUBCAT ob) a

type FUN j k = SUBCAT (Representable :: (j +-> k) -> Constraint) Source Github #

(!) :: forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j). (f ~> g) -> (a ~> b) -> (UN ('SUB :: (j +-> k) -> SUBCAT (Representable :: (j +-> k) -> Constraint)) f % a) ~> (UN ('SUB :: (j +-> k) -> SUBCAT (Representable :: (j +-> k) -> Constraint)) g % b) Source Github #

type ARROW k = FUN BOOL k Source Github #

The arrow category of k as functor category from 2 to k.

commSquare :: forall {k} (f :: BOOL +-> k) (g :: BOOL +-> k) (a :: k) (b :: k) (c :: k) (d :: k). (a ~ (f % 'FLS), b ~ (f % 'TRU), c ~ (g % 'FLS), d ~ (g % 'TRU)) => (('SUB f :: SUBCAT (Representable :: (BOOL +-> k) -> Constraint)) ~> ('SUB g :: SUBCAT (Representable :: (BOOL +-> k) -> Constraint))) -> (a ~> b, b ~> d, a ~> c, c ~> d) Source Github #