Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.Prof

Documentation

data PROFK j k Source Comments #

Constructors

PK (j +-> k)

Instances

Instances details

Bicategory PROFK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Ob0 PROFK (k :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Ob0 PROFK (k :: Type) = CategoryOf k
type I
Instance details Defined in Proarrow.Category.Bicategory.Prof type I = 'PK (Id :: i -> i -> Type)
type O (p :: PROFK k1 k2) (q :: PROFK j k1)
Instance details Defined in Proarrow.Category.Bicategory.Prof type O (p :: PROFK k1 k2) (q :: PROFK j k1) = 'PK (UN ('PK :: (k1 +-> k2) -> PROFK k1 k2) p :.: UN ('PK :: (j +-> k1) -> PROFK j k1) q)

Methods

o :: forall {i} j k (a :: PROFK j k) (b :: PROFK j k) (c :: PROFK i j) (d :: PROFK i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

withOb2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) r. (Ob a, Ob b, Ob0 PROFK i, Ob0 PROFK j, Ob0 PROFK k) => (Ob (O a b) => r) -> r Source Comments #

withOb0s :: forall {j} {k} (a :: PROFK j k) r. Ob a => ((Ob0 PROFK j, Ob0 PROFK k) => r) -> r Source Comments #

(\\\) :: forall i j (ps :: PROFK i j) (qs :: PROFK i j) r. ((Ob0 PROFK i, Ob0 PROFK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall {i} {j} (a :: PROFK i j). (Ob0 PROFK i, Ob0 PROFK j, Ob a) => O (I :: PROFK j j) a ~> a Source Comments #

leftUnitorInv :: forall {i} {j} (a :: PROFK i j). (Ob0 PROFK i, Ob0 PROFK j, Ob a) => a ~> O (I :: PROFK j j) a Source Comments #

rightUnitor :: forall {i} {j} (a :: PROFK i j). (Ob0 PROFK i, Ob0 PROFK j, Ob a) => O a (I :: PROFK i i) ~> a Source Comments #

rightUnitorInv :: forall {i} {j} (a :: PROFK i j). (Ob0 PROFK i, Ob0 PROFK j, Ob a) => a ~> O a (I :: PROFK i i) Source Comments #

associator :: forall {h} {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) (c :: PROFK h i). (Ob0 PROFK h, Ob0 PROFK i, Ob0 PROFK j, Ob0 PROFK k, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {h} {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) (c :: PROFK h i). (Ob0 PROFK h, Ob0 PROFK i, Ob0 PROFK j, Ob0 PROFK k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

HasBinaryProducts FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Fst FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Fst FUNK (a :: Type) (b :: Type) = FUN (Rep (FstCat :: (a, b) +-> a))
type Snd FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Snd FUNK (a :: Type) (b :: Type) = FUN (Rep (SndCat :: (a, b) +-> b))
type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) = FUN (UNFUN f :&&&: UNFUN g)

Methods

fstObj :: (Ob0 FUNK a, Ob0 FUNK b) => Obj (Fst FUNK a b) Source Comments #

sndObj :: (Ob0 FUNK a, Ob0 FUNK b) => Obj (Snd FUNK a b) Source Comments #

prodObj :: forall j a b (f :: FUNK j a) (g :: FUNK j b). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob f, Ob g) => Obj (f &&& g) Source Comments #

prodUniv :: forall j a b (h :: FUNK j (Product FUNK a b)) (k :: FUNK j (Product FUNK a b)). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob h, Ob k) => (O (Fst FUNK a b) h ~> O (Fst FUNK a b) k) -> (O (Snd FUNK a b) h ~> O (Snd FUNK a b) k) -> h ~> k Source Comments #

HasTerminalObject FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Terminate FUNK (j :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Terminate FUNK (j :: Type) = FUN (Rep (Terminate :: j +-> ()))

Methods

terminate :: Ob0 FUNK j => Obj (Terminate FUNK j) Source Comments #

termUniv :: forall j (f :: FUNK j (TerminalObject FUNK)) (g :: FUNK j (TerminalObject FUNK)). (Ob0 FUNK j, Ob f, Ob g) => f ~> g Source Comments #

Equipment PROFK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withCotightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #

WithObO2 Cotight PROFK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withObO2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) r. (Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) => ((IsOb Cotight (O a b), Ob (O a b)) => r) -> r Source Comments #

WithObO2 Tight PROFK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withObO2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK i j) r. (Ob a, Ob b, IsOb Tight a, IsOb Tight b) => ((IsOb Tight (O a b), Ob (O a b)) => r) -> r Source Comments #

(Profunctor f, Profunctor j) => RightKanExtension ('PK j :: PROFK c d) ('PK f :: PROFK c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Ran ('PK j :: PROFK c d) ('PK f :: PROFK c e)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Ran ('PK j :: PROFK c d) ('PK f :: PROFK c e) = 'PK (Ran ('OP j) f)

Methods

ran :: O (Ran ('PK j) ('PK f)) ('PK j) ~> 'PK f Source Comments #

ranUniv :: forall (g :: PROFK d e). Ob g => (O g ('PK j) ~> 'PK f) -> g ~> Ran ('PK j) ('PK f) Source Comments #

(Profunctor f, Profunctor j) => RightKanLift ('PK j :: PROFK d c) ('PK f :: PROFK e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Rift ('PK j :: PROFK d c) ('PK f :: PROFK e c)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Rift ('PK j :: PROFK d c) ('PK f :: PROFK e c) = 'PK (Rift ('OP j) f)

Methods

rift :: O ('PK j) (Rift ('PK j) ('PK f)) ~> 'PK f Source Comments #

riftUniv :: forall (g :: PROFK e d). Ob g => (O ('PK j) g ~> 'PK f) -> g ~> Rift ('PK j) ('PK f) Source Comments #

(HasColimits j k, Ob j) => HasColimits ('PK j :: PROFK a i) (k :: Kind) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withObColimit :: forall (d :: PROFK k i) r. IsCotight d => (IsCotight (Colimit ('PK j) d) => r) -> r Source Comments #

colimit :: forall (d :: PROFK k i). IsCotight d => O ('PK j) (Colimit ('PK j) d) ~> d Source Comments #

colimitUniv :: forall (d :: PROFK k i) (p :: PROFK k a). (IsCotight d, Ob p) => (O ('PK j) p ~> d) -> p ~> Colimit ('PK j) d Source Comments #

(HasLimits j k, Ob j) => HasLimits ('PK j :: PROFK i a) (k :: Kind) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withObLimit :: forall (d :: PROFK i k) r. IsTight d => (IsTight (Limit ('PK j) d) => r) -> r Source Comments #

limit :: forall (d :: PROFK i k). IsTight d => O (Limit ('PK j) d) ('PK j) ~> d Source Comments #

limitUniv :: forall (d :: PROFK i k) (p :: PROFK a k). (IsTight d, Ob p) => (O p ('PK j) ~> d) -> p ~> Limit ('PK j) d Source Comments #

Proadjunction l r => Adjunction_ ('PK l :: PROFK c d) ('PK r :: PROFK d c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

adj :: Adj ('PK l) ('PK r) Source Comments #

(Category cj, Category ck, Profunctor p) => Bimodule ('PK ck :: PROFK k k) ('PK cj :: PROFK j j) ('PK p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

leftAction :: O ('PK ck) ('PK p) ~> 'PK p Source Comments #

rightAction :: O ('PK p) ('PK cj) ~> 'PK p Source Comments #

Procomonad p => Comonad ('PK p :: PROFK k k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

epsilon :: 'PK p ~> (I :: PROFK k k) Source Comments #

delta :: 'PK p ~> O ('PK p) ('PK p) Source Comments #

Promonad p => Monad ('PK p :: PROFK k k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

eta :: (I :: PROFK k k) ~> 'PK p Source Comments #

mu :: O ('PK p) ('PK p) ~> 'PK p Source Comments #

(Monad m, Comonad c, Ob0 sk i, Ob0 tk k2, LaxProfunctor sk tk kk, Ob c, Ob m) => Monad ('PK (P sk tk kk ('CO c) m) :: PROFK (kk i k2) (kk i k2)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

eta :: (I :: PROFK (kk i k2) (kk i k2)) ~> 'PK (P sk tk kk ('CO c) m) Source Comments #

mu :: O ('PK (P sk tk kk ('CO c) m)) ('PK (P sk tk kk ('CO c) m)) ~> 'PK (P sk tk kk ('CO c) m) Source Comments #

CategoryOf (PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Prof type (~>) = Prof :: PROFK j k -> PROFK j k -> Type

Promonad (Prof :: PROFK j k -> PROFK j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

id :: forall (a :: PROFK j k). Ob a => Prof a a Source Comments #

(.) :: forall (b :: PROFK j k) (c :: PROFK j k) (a :: PROFK j k). Prof b c -> Prof a b -> Prof a c Source Comments #

Profunctor (Prof :: PROFK j k -> PROFK j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

dimap :: forall (c :: PROFK j k) (a :: PROFK j k) (b :: PROFK j k) (d :: PROFK j k). (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d Source Comments #

(\\) :: forall (a :: PROFK j k) (b :: PROFK j k) r. ((Ob a, Ob b) => r) -> Prof a b -> r Source Comments #

Functor ('PK :: (j +-> k) -> PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

map :: forall (a :: j +-> k) (b :: j +-> k). (a ~> b) -> 'PK a ~> 'PK b Source Comments #

type TerminalObject FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TerminalObject FUNK = ()

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type I = 'PK (Id :: i -> i -> Type)

type Terminate FUNK (j :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Terminate FUNK (j :: Type) = FUN (Rep (Terminate :: j +-> ()))

type Ob0 PROFK (k :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Ob0 PROFK (k :: Type) = CategoryOf k

type Fst FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Fst FUNK (a :: Type) (b :: Type) = FUN (Rep (FstCat :: (a, b) +-> a))

type Product FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Product FUNK (a :: Type) (b :: Type) = (a, b)

type Snd FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Snd FUNK (a :: Type) (b :: Type) = FUN (Rep (SndCat :: (a, b) +-> b))

type CotightAdjoint (p :: PROFK k j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type CotightAdjoint (p :: PROFK k j) = 'PK (RepCostar (UN ('PK :: (k +-> j) -> PROFK k j) p))

type TightAdjoint (p :: PROFK k j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TightAdjoint (p :: PROFK k j) = 'PK (CorepStar (UN ('PK :: (k +-> j) -> PROFK k j) p))

type O (p :: PROFK k1 k2) (q :: PROFK j k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type O (p :: PROFK k1 k2) (q :: PROFK j k1) = 'PK (UN ('PK :: (k1 +-> k2) -> PROFK k1 k2) p :.: UN ('PK :: (j +-> k1) -> PROFK j k1) q)

type IsOb ProfRep (p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb ProfRep (p :: PROFK j k) = Representable (UN ('PK :: (j +-> k) -> PROFK j k) p)

type IsOb Cotight (p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb Cotight (p :: PROFK j k) = Corepresentable (UN ('PK :: (j +-> k) -> PROFK j k) p)

type IsOb Tight (p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb Tight (p :: PROFK j k) = Representable (UN ('PK :: (j +-> k) -> PROFK j k) p)

type Ran ('PK j :: PROFK c d) ('PK f :: PROFK c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Ran ('PK j :: PROFK c d) ('PK f :: PROFK c e) = 'PK (Ran ('OP j) f)

type Rift ('PK j :: PROFK d c) ('PK f :: PROFK e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Rift ('PK j :: PROFK d c) ('PK f :: PROFK e c) = 'PK (Rift ('OP j) f)

type Colimit ('PK j :: PROFK a i) ('PK d :: PROFK k i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Colimit ('PK j :: PROFK a i) ('PK d :: PROFK k i) = 'PK (Colimit j d)

type Limit ('PK j :: PROFK i a) ('PK d :: PROFK i k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Limit ('PK j :: PROFK i a) ('PK d :: PROFK i k) = 'PK (Limit j d)

type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) = FUN (UNFUN f :&&&: UNFUN g)

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type (~>) = Prof :: PROFK j k -> PROFK j k -> Type

type Ob (p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Ob (p :: PROFK j k) = (Is ('PK :: (j +-> k) -> PROFK j k) p, Profunctor (UN ('PK :: (j +-> k) -> PROFK j k) p))

type UN ('PK :: (j +-> k) -> PROFK j k) ('PK p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type UN ('PK :: (j +-> k) -> PROFK j k) ('PK p :: PROFK j k) = p

data Prof (p :: PROFK j k) (q :: PROFK j k) where Source Comments #

Constructors

Prof :: forall {j} {k} (p1 :: j +-> k) (q1 :: j +-> k). (Ob p1, Ob q1) => (p1 :~> q1) -> Prof ('PK p1) ('PK q1)

Instances

Instances details

Promonad (Prof :: PROFK j k -> PROFK j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods id :: forall (a :: PROFK j k). Ob a => Prof a a Source Comments # (.) :: forall (b :: PROFK j k) (c :: PROFK j k) (a :: PROFK j k). Prof b c -> Prof a b -> Prof a c Source Comments #
Profunctor (Prof :: PROFK j k -> PROFK j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods dimap :: forall (c :: PROFK j k) (a :: PROFK j k) (b :: PROFK j k) (d :: PROFK j k). (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d Source Comments # (\\) :: forall (a :: PROFK j k) (b :: PROFK j k) r. ((Ob a, Ob b) => r) -> Prof a b -> r Source Comments #

data ProfRep Source Comments #

Instances

Instances details

HasBinaryProducts FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Fst FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Fst FUNK (a :: Type) (b :: Type) = FUN (Rep (FstCat :: (a, b) +-> a))
type Snd FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Snd FUNK (a :: Type) (b :: Type) = FUN (Rep (SndCat :: (a, b) +-> b))
type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) = FUN (UNFUN f :&&&: UNFUN g)

Methods

fstObj :: (Ob0 FUNK a, Ob0 FUNK b) => Obj (Fst FUNK a b) Source Comments #

sndObj :: (Ob0 FUNK a, Ob0 FUNK b) => Obj (Snd FUNK a b) Source Comments #

prodObj :: forall j a b (f :: FUNK j a) (g :: FUNK j b). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob f, Ob g) => Obj (f &&& g) Source Comments #

prodUniv :: forall j a b (h :: FUNK j (Product FUNK a b)) (k :: FUNK j (Product FUNK a b)). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob h, Ob k) => (O (Fst FUNK a b) h ~> O (Fst FUNK a b) k) -> (O (Snd FUNK a b) h ~> O (Snd FUNK a b) k) -> h ~> k Source Comments #

HasTerminalObject FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Terminate FUNK (j :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Terminate FUNK (j :: Type) = FUN (Rep (Terminate :: j +-> ()))

Methods

terminate :: Ob0 FUNK j => Obj (Terminate FUNK j) Source Comments #

termUniv :: forall j (f :: FUNK j (TerminalObject FUNK)) (g :: FUNK j (TerminalObject FUNK)). (Ob0 FUNK j, Ob f, Ob g) => f ~> g Source Comments #

type TerminalObject FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TerminalObject FUNK = ()

type Terminate FUNK (j :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Terminate FUNK (j :: Type) = FUN (Rep (Terminate :: j +-> ()))

type IsOb0 ProfRep (k :: s) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb0 ProfRep (k :: s) = ()

type Fst FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Fst FUNK (a :: Type) (b :: Type) = FUN (Rep (FstCat :: (a, b) +-> a))

type Product FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Product FUNK (a :: Type) (b :: Type) = (a, b)

type Snd FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Snd FUNK (a :: Type) (b :: Type) = FUN (Rep (SndCat :: (a, b) +-> b))

type IsOb ProfRep (p :: PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb ProfRep (p :: PROFK j k) = Representable (UN ('PK :: (j +-> k) -> PROFK j k) p)

type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) = FUN (UNFUN f :&&&: UNFUN g)

type FUNK = SUBCAT ProfRep PROFK Source Comments #

type FUN (p :: i +-> j) = 'SUB ('PK p) :: SUBCAT ProfRep PROFK i j Source Comments #

type UNFUN (p :: SUBCAT tag PROFK j k) = UN ('PK :: (j +-> k) -> PROFK j k) (UN ('SUB :: PROFK j k -> SUBCAT tag PROFK j k) p) Source Comments #

class (forall (s :: COK sk h i) (t :: tk j k2). (Ob s, Ob t) => Profunctor (p s t), forall (s :: COK sk h i). Ob s => Functor (p s), Functor p) => IsFunctorial (h :: k) (i :: k) (j :: k1) (k2 :: k1) (p :: COK sk h i -> tk j k2 -> kk h j +-> kk i k2) Source Comments #

Instances

Instances details

(forall (s :: COK sk h i) (t :: tk j k3). (Ob s, Ob t) => Profunctor (p s t), forall (s :: COK sk h i). Ob s => Functor (p s), Functor p) => IsFunctorial (h :: k1) (i :: k1) (j :: k2) (k3 :: k2) (p :: COK sk h i -> tk j k3 -> kk h j +-> kk i k3) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof

class (Bicategory sk, Bicategory tk, forall (h :: s) (i :: s) (j :: t) (k :: t). (Ob0 sk h, Ob0 sk i, Ob0 tk j, Ob0 tk k) => IsFunctorial h i j k (P sk tk kk), forall (j :: s) (k :: t). (Ob0 sk j, Ob0 tk k) => CategoryOf (kk j k)) => LaxProfunctor (sk :: CAT s) (tk :: CAT t) (kk :: t +-> s) where Source Comments #

Associated Types

data P (sk :: CAT s) (tk :: CAT t) (kk :: t +-> s) :: forall {h :: s} {i :: s} {j :: t} {k :: t}. COK sk h i -> tk j k -> kk h j +-> kk i k Source Comments #

Methods

laxId :: forall (k :: s) (j :: t). (Ob0 sk k, Ob0 tk j) => (Id :: kk k j -> kk k j -> Type) :~> P sk tk kk ('CO (I :: sk k k)) (I :: tk j j) Source Comments #

laxComp :: forall {j1 :: s} {i :: s} {j2 :: t} {k :: t} {h :: s} {j3 :: t} (s0 :: COK sk j1 i) (t0 :: tk j2 k) (s1 :: COK sk h j1) (t1 :: tk j3 j2). (P sk tk kk s0 t0 :.: P sk tk kk s1 t1) :~> P sk tk kk (O s0 s1) (O t0 t1) Source Comments #

Instances

Instances details

Bicategory kk => LaxProfunctor (kk :: CAT k) (kk :: CAT k) (HK kk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Hom

Associated Types

data P (kk :: CAT k) (kk :: CAT k) (HK kk :: k -> k -> Type) (s :: COK kk h i) (t :: kk j k1) (a :: HK kk i k1) (b :: HK kk h j)

Instance details

Defined in Proarrow.Category.Bicategory.Hom

data P (kk :: CAT k) (kk :: CAT k) (HK kk :: k -> k -> Type) (s :: COK kk h i) (t :: kk j k1) (a :: HK kk i k1) (b :: HK kk h j) where

Hom :: forall {k} {h :: k} {i :: k} {j :: k} {k1 :: k} {kk :: CAT k} (a1 :: kk i k1) (b1 :: kk h j) (s1 :: kk h i) (t :: kk j k1). (Ob a1, Ob b1, Ob s1, Ob t, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k1) => (O a1 s1 ~> O t b1) -> P kk kk (HK kk) ('CO s1) t ('HomK a1) ('HomK b1)

Methods

laxId :: forall (k0 :: k) (j :: k). (Ob0 kk k0, Ob0 kk j) => (Id :: HK kk k j -> HK kk k j -> Type) :~> P kk kk (HK kk) ('CO (I :: kk k k)) (I :: kk j j) Source Comments #

laxComp :: forall {j1 :: k} {i :: k} {j2 :: k} {k0 :: k} {h :: k} {j3 :: k} (s0 :: COK kk j1 i) (t0 :: kk j2 k0) (s1 :: COK kk h j1) (t1 :: kk j3 j2). (P kk kk (HK kk) s0 t0 :.: P kk kk (HK kk) s1 t1) :~> P kk kk (HK kk) (O s0 s1) (O t0 t1) Source Comments #

dimapLax :: forall {s1} {t1} {h :: s1} {i :: s1} {j :: t1} {k :: t1} (sk :: CAT s1) (tk :: CAT t1) (kk :: t1 +-> s1) (s' :: sk h i) (s2 :: sk h i) (t2 :: tk j k) (t' :: tk j k). LaxProfunctor sk tk kk => (s' ~> s2) -> (t2 ~> t') -> P sk tk kk ('CO s2) t2 :~> P sk tk kk ('CO s') t' Source Comments #