Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Prof

Synopsis

data PROFK j k = PK (j +-> k)
data Prof (p :: PROFK j k) (q :: PROFK j k) where
- Prof :: forall {j} {k} (p1 :: j +-> k) (q1 :: j +-> k). (Ob p1, Ob q1) => (p1 :~> q1) -> Prof ('PK p1) ('PK q1)
data ProfRep
type FUNK = SUBCAT ProfRep PROFK
type FUN (p :: i +-> j) = 'SUB ('PK p) :: SUBCAT ProfRep PROFK i j
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)
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)
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
- 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
- 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)
- 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)
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'
type ProfSq (p :: j +-> h) (q :: k +-> i) (f :: j +-> k) (g :: h +-> i) = Sq '('PK p, FUN g) '('PK q, FUN f)
isCotabulator :: forall {j} {k} (p :: PRO j k). Profunctor p => ProfSq p (Collage :: COLLAGE p -> COLLAGE p -> Type) (InjR p) (InjL p)
data CotabulatorFactorizer s (p :: j +-> k) (f :: j +-> h) (g :: k +-> h) (a :: h) (b :: COLLAGE p) where
- CF :: forall {j} {k} {h} (p :: j +-> k) (b :: COLLAGE p) (a :: h) s (f :: j +-> h) (g :: k +-> h). Ob b => (a ~> (CotabulatorFactorizer s p f g % b)) -> CotabulatorFactorizer s p f g a b
cotabulatorFactorize :: forall {h} {j} {k} (p :: PRO h j) (f :: j +-> k) (g :: h +-> k) r. (Profunctor p, Representable f, Representable g) => ProfSq p (Id :: k -> k -> Type) f g -> (forall s. Reifies s (ProfSq p (Id :: k -> k -> Type) f g) => ProfSq (Id :: COLLAGE p -> COLLAGE p -> Type) (Id :: k -> k -> Type) (CotabulatorFactorizer s p f g) (CotabulatorFactorizer s p f g) -> r) -> r

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

iObj :: Ob0 PROFK i => Obj (I :: PROFK i i) Source Comments #

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 #

(\\\) :: 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 #

Equipment PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

Methods

mapConjoint :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Conjoint PROFK g ~> Conjoint PROFK f Source Comments #

conjToId :: Ob0 FUNK k => Conjoint PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

conjFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Conjoint PROFK (I :: FUNK k k) Source Comments #

conjToCompose :: forall {k1} {j} {k2} (f :: FUNK j k2) (g :: FUNK k1 j). Obj f -> Obj g -> Conjoint PROFK (O f g) ~> O (Conjoint PROFK g) (Conjoint PROFK f) Source Comments #

conjFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Conjoint PROFK g) (Conjoint PROFK f) ~> Conjoint PROFK (O f g) Source Comments #

comConUnit :: forall {j} {k} (f :: FUNK j k). Obj f -> (I :: PROFK j j) ~> O (Conjoint PROFK f) (Companion PROFK f) Source Comments #

comConCounit :: forall {j} {k} (f :: FUNK j k). Obj f -> O (Companion PROFK f) (Conjoint PROFK f) ~> (I :: PROFK k k) Source Comments #

HasCompanions PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

Methods

mapCompanion :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Companion PROFK f ~> Companion PROFK g Source Comments #

compToId :: Ob0 FUNK k => Companion PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

compFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Companion PROFK (I :: FUNK k k) Source Comments #

compToCompose :: forall {i} {j} {k} (f :: FUNK j k) (g :: FUNK i j). Obj f -> Obj g -> Companion PROFK (O f g) ~> O (Companion PROFK f) (Companion PROFK g) Source Comments #

compFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Companion PROFK f) (Companion PROFK g) ~> Companion PROFK (O f g) Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

limitObj :: forall (d :: FUNK i k). Ob d => Obj (Limit ('PK j) d) Source Comments #

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

limitUniv :: forall (d :: FUNK i k) (p :: FUNK a k). (Ob d, Ob p) => (O (Companion PROFK p) ('PK j) ~> Companion PROFK d) -> p ~> Limit ('PK j) d 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 #

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

unit :: (I :: PROFK c c) ~> O ('PK r) ('PK l) Source Comments #

counit :: O ('PK l) ('PK r) ~> (I :: PROFK d d) 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, LaxProfunctor sk tk kk, Ob c, Ob m) => Monad ('PK (P sk tk kk ('CO c) m) :: PROFK (kk i j) (kk i j)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

eta :: (I :: PROFK (kk i j) (kk i j)) ~> '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 #

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

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

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 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) (d :: SUBCAT ProfRep PROFK i k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Colimit ('PK j :: PROFK a i) (d :: SUBCAT ProfRep PROFK i k) = FUN (Colimit j (UNFUN d))

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Limit ('PK j :: PROFK i a) (d :: SUBCAT ProfRep PROFK i k) = FUN (Limit j (UNFUN d))

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

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 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 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

Equipment PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

Methods

mapConjoint :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Conjoint PROFK g ~> Conjoint PROFK f Source Comments #

conjToId :: Ob0 FUNK k => Conjoint PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

conjFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Conjoint PROFK (I :: FUNK k k) Source Comments #

conjToCompose :: forall {k1} {j} {k2} (f :: FUNK j k2) (g :: FUNK k1 j). Obj f -> Obj g -> Conjoint PROFK (O f g) ~> O (Conjoint PROFK g) (Conjoint PROFK f) Source Comments #

conjFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Conjoint PROFK g) (Conjoint PROFK f) ~> Conjoint PROFK (O f g) Source Comments #

comConUnit :: forall {j} {k} (f :: FUNK j k). Obj f -> (I :: PROFK j j) ~> O (Conjoint PROFK f) (Companion PROFK f) Source Comments #

comConCounit :: forall {j} {k} (f :: FUNK j k). Obj f -> O (Companion PROFK f) (Conjoint PROFK f) ~> (I :: PROFK k k) Source Comments #

HasCompanions PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

Methods

mapCompanion :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Companion PROFK f ~> Companion PROFK g Source Comments #

compToId :: Ob0 FUNK k => Companion PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

compFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Companion PROFK (I :: FUNK k k) Source Comments #

compToCompose :: forall {i} {j} {k} (f :: FUNK j k) (g :: FUNK i j). Obj f -> Obj g -> Companion PROFK (O f g) ~> O (Companion PROFK f) (Companion PROFK g) Source Comments #

compFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Companion PROFK f) (Companion PROFK g) ~> Companion PROFK (O f g) Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

limitObj :: forall (d :: FUNK i k). Ob d => Obj (Limit ('PK j) d) Source Comments #

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Colimit ('PK j :: PROFK a i) (d :: SUBCAT ProfRep PROFK i k) = FUN (Colimit j (UNFUN d))

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Limit ('PK j :: PROFK i a) (d :: SUBCAT ProfRep PROFK i k) = FUN (Limit j (UNFUN d))

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

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 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 #

type ProfSq (p :: j +-> h) (q :: k +-> i) (f :: j +-> k) (g :: h +-> i) = Sq '('PK p, FUN g) '('PK q, FUN f) Source Comments #

isCotabulator :: forall {j} {k} (p :: PRO j k). Profunctor p => ProfSq p (Collage :: COLLAGE p -> COLLAGE p -> Type) (InjR p) (InjL p) Source Comments #

The collage is a cotabulator with this 2-cell.

J-InjR-Col
|   v   |
p---@   |
|   v   |
K-InjL-Col

data CotabulatorFactorizer s (p :: j +-> k) (f :: j +-> h) (g :: k +-> h) (a :: h) (b :: COLLAGE p) where Source Comments #

Any 2-cell of shape p(a, b) -> e(f a, g b) factors through the cotabulator 2-cell.

J--f--H    J-Inj1-CG--X--H
|  v  |    |   v   |  v  |
p--@  | == p---@   |  |  |
|  v  |    |   v   |  v  |
K--g--H    K-Inj2-CG--X--H

Constructors

CF :: forall {j} {k} {h} (p :: j +-> k) (b :: COLLAGE p) (a :: h) s (f :: j +-> h) (g :: k +-> h). Ob b => (a ~> (CotabulatorFactorizer s p f g % b)) -> CotabulatorFactorizer s p f g a b

Instances

Instances details

(Profunctor p, Representable f, Representable g, Reifies s (ProfSq p (Id :: j2 -> j2 -> Type) f g)) => Profunctor (CotabulatorFactorizer s p f g :: j2 -> COLLAGE p -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods dimap :: forall (c :: j2) (a :: j2) (b :: COLLAGE p) (d :: COLLAGE p). (c ~> a) -> (b ~> d) -> CotabulatorFactorizer s p f g a b -> CotabulatorFactorizer s p f g c d Source Comments # (\\) :: forall (a :: j2) (b :: COLLAGE p) r. ((Ob a, Ob b) => r) -> CotabulatorFactorizer s p f g a b -> r Source Comments #
(Profunctor p, Representable f, Representable g, Reifies s (ProfSq p (Id :: k2 -> k2 -> Type) f g)) => Representable (CotabulatorFactorizer s p f g :: k2 -> COLLAGE p -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods index :: forall (a :: k2) (b :: COLLAGE p). CotabulatorFactorizer s p f g a b -> a ~> (CotabulatorFactorizer s p f g % b) Source Comments # tabulate :: forall (b :: COLLAGE p) (a :: k2). Ob b => (a ~> (CotabulatorFactorizer s p f g % b)) -> CotabulatorFactorizer s p f g a b Source Comments # repMap :: forall (a :: COLLAGE p) (b :: COLLAGE p). (a ~> b) -> (CotabulatorFactorizer s p f g % a) ~> (CotabulatorFactorizer s p f g % b) Source Comments #
type (CotabulatorFactorizer s p f g :: k2 -> COLLAGE p -> Type) % ('L a :: COLLAGE p) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type (CotabulatorFactorizer s p f g :: k2 -> COLLAGE p -> Type) % ('L a :: COLLAGE p) = g % a
type (CotabulatorFactorizer s p f g :: k2 -> COLLAGE p -> Type) % ('R a :: COLLAGE p) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type (CotabulatorFactorizer s p f g :: k2 -> COLLAGE p -> Type) % ('R a :: COLLAGE p) = f % a

cotabulatorFactorize :: forall {h} {j} {k} (p :: PRO h j) (f :: j +-> k) (g :: h +-> k) r. (Profunctor p, Representable f, Representable g) => ProfSq p (Id :: k -> k -> Type) f g -> (forall s. Reifies s (ProfSq p (Id :: k -> k -> Type) f g) => ProfSq (Id :: COLLAGE p -> COLLAGE p -> Type) (Id :: k -> k -> Type) (CotabulatorFactorizer s p f g) (CotabulatorFactorizer s p f g) -> r) -> r Source Comments #