proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Bicategory.Limit

Documentation

type family TerminalObject (kk :: CAT s) :: s Source Comments #

Instances

Instances details
type TerminalObject FUNK Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TerminalObject FUNK = ()

class HasTerminalObject (kk :: CAT s) where Source Comments #

Associated Types

type Terminate (kk :: CAT s) (j :: s) :: kk j (TerminalObject kk) Source Comments #

Methods

terminate :: forall (j :: s). Ob0 kk j => Obj (Terminate kk j) Source Comments #

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

Instances

Instances details
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 (Terminate :: () -> j -> Type)

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 family Product (kk :: CAT s) (a :: s) (b :: s) :: s Source Comments #

Instances

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

class HasBinaryProducts (kk :: CAT s) where Source Comments #

Associated Types

type Fst (kk :: CAT s) (a :: s) (b :: s) :: kk (Product kk a b) a Source Comments #

type Snd (kk :: CAT s) (a :: s) (b :: s) :: kk (Product kk a b) b Source Comments #

type (f :: kk j a) &&& (g :: kk j b) :: kk j (Product kk a b) Source Comments #

Methods

fstObj :: forall (a :: s) (b :: s). (Ob0 kk a, Ob0 kk b) => Obj (Fst kk a b) Source Comments #

sndObj :: forall (a :: s) (b :: s). (Ob0 kk a, Ob0 kk b) => Obj (Snd kk a b) Source Comments #

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

prodUniv :: forall (j :: s) (a :: s) (b :: s) (h :: kk j (Product kk a b)) (k :: kk j (Product kk a b)). (Ob0 kk j, Ob0 kk a, Ob0 kk b, Ob h, Ob k) => (O (Fst kk a b) h ~> O (Fst kk a b) k) -> (O (Snd kk a b) h ~> O (Snd kk a b) k) -> h ~> k 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 (FstCat :: a -> (a, b) -> Type)
type Snd FUNK (a :: Type) (b :: Type) 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Snd FUNK (a :: Type) (b :: Type) = FUN (SndCat :: b -> (a, b) -> Type)
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 #