Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Equipment.Limit

Synopsis

class (HasCompanions hk vk, Ob j) => HasLimits (vk :: CAT s) (j :: hk i a) (k :: s) where
- type Limit (j :: hk i a) (d :: vk i k) :: vk a k
- limitObj :: forall (d :: vk i k). Ob d => Obj (Limit j d)
- limit :: forall (d :: vk i k). Ob d => O (Companion hk (Limit j d)) j ~> Companion hk d
- limitUniv :: forall (d :: vk i k) (p :: vk a k). (Ob d, Ob p) => (O (Companion hk p) j ~> Companion hk d) -> p ~> Limit j d
class (HasCompanions hk vk, Ob j) => HasColimits (vk :: CAT s) (j :: hk a i) (k :: s) where
- type Colimit (j :: hk a i) (d :: vk i k) :: vk a k
- colimitObj :: forall (d :: vk i k). Ob d => Obj (Colimit j d)
- colimit :: forall (d :: vk i k). Ob d => O (Companion hk d) j ~> Companion hk (Colimit j d)
- colimitUniv :: forall (d :: vk i k) (p :: vk a k). (Ob d, Ob p) => (O (Companion hk d) j ~> Companion hk p) -> Colimit j d ~> p
type family TerminalObject (hk :: CAT s) (vk :: CAT s) :: s
class HasCompanions hk vk => HasTerminalObject (hk :: CAT s) (vk :: CAT s) where
- type Terminate (hk :: CAT s) (vk :: CAT s) (j :: s) :: vk j (TerminalObject hk vk)
- terminate :: forall (j :: s). Ob0 vk j => Obj (Terminate hk vk j)
- termUniv :: forall (i :: s) (j :: s) (p :: hk i j). (Ob0 vk i, Ob0 vk j, Ob p) => Sq '(p, Terminate hk vk j) '(I :: hk (TerminalObject hk vk) (TerminalObject hk vk), Terminate hk vk i)
type family InitialObject (hk :: CAT s) (vk :: CAT s) :: s
class HasCompanions hk vk => HasInitialObject (hk :: CAT s) (vk :: CAT s) where
- type Initiate (hk :: CAT s) (vk :: CAT s) (j :: s) :: vk (InitialObject hk vk) j
- initiate :: forall (j :: s). Ob0 vk j => Obj (Initiate hk vk j)
- initUniv :: forall (i :: s) (j :: s) (p :: hk i j). (Ob0 vk i, Ob0 vk j, Ob p) => Sq '(I :: hk (InitialObject hk vk) (InitialObject hk vk), Initiate hk vk j) '(p, Initiate hk vk i)
type family Product (hk :: CAT s) (vk :: CAT s) (a :: s) (b :: s) :: s
class HasBinaryProducts (hk :: CAT s) (vk :: CAT s) where
- type Fst (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk (Product hk vk i j) i
- type Snd (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk (Product hk vk i j) j
- type ProdV (hk :: CAT s) (vk :: CAT s) (f :: vk k i) (g :: vk k j) :: vk k (Product hk vk i j)
- type ProdH (hk :: CAT s) (vk :: CAT s) (p :: hk j k) (q :: hk j' k') :: hk (Product hk vk j j') (Product hk vk k k')
- fstObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Fst hk vk i j)
- sndObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Snd hk vk i j)
- prodObj :: forall (j :: s) (a :: s) (b :: s) (f :: vk j a) (g :: vk j b). (Ob0 vk j, Ob0 vk a, Ob0 vk b, Ob f, Ob g) => Obj (ProdV hk vk f g)
- prodUniv :: forall {i :: s} {j :: s} (k :: s) (k' :: s) (p :: hk k k') (i' :: s) (f' :: vk k' i') (a :: hk i i') (f :: vk k i) (j' :: s) (g' :: vk k' j') (b :: hk j j') (g :: vk k j). Sq '(p, f') '(a, f) -> Sq '(p, g') '(b, g) -> Sq '(p, ProdV hk vk f' g') '(ProdH hk vk a b, ProdV hk vk f g)
type family Coproduct (hk :: CAT s) (vk :: CAT s) (a :: s) (b :: s) :: s
class HasBinaryCoproducts (hk :: CAT s) (vk :: CAT s) where
- type Lft (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk i (Coproduct hk vk i j)
- type Rgt (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk j (Coproduct hk vk i j)
- type CoprodV (hk :: CAT s) (vk :: CAT s) (f :: vk i k) (g :: vk j k) :: vk (Coproduct hk vk i j) k
- type CoprodH (hk :: CAT s) (vk :: CAT s) (p :: hk j k) (q :: hk j' k') :: hk (Coproduct hk vk j j') (Coproduct hk vk k k')
- lftObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Lft hk vk i j)
- rgtObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Rgt hk vk i j)
- coprodObj :: forall (j :: s) (a :: s) (b :: s) (f :: vk a j) (g :: vk b j). (Ob0 vk j, Ob0 vk a, Ob0 vk b, Ob f, Ob g) => Obj (CoprodV hk vk f g)
- coprodUniv :: forall (i :: s) (i' :: s) (a :: hk i i') (k' :: s) (f' :: vk i' k') (k :: s) (p :: hk k k') (f :: vk i k) (j :: s) (j' :: s) (b :: hk j j') (g' :: vk j' k') (g :: vk j k). Sq '(a, f') '(p, f) -> Sq '(b, g') '(p, g) -> Sq '(CoprodH hk vk a b, CoprodV hk vk f' g') '(p, CoprodV hk vk f g)

Documentation

class (HasCompanions hk vk, Ob j) => HasLimits (vk :: CAT s) (j :: hk i a) (k :: s) where Source Comments #

weighted limits

Associated Types

type Limit (j :: hk i a) (d :: vk i k) :: vk a k Source Comments #

Methods

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

limit :: forall (d :: vk i k). Ob d => O (Companion hk (Limit j d)) j ~> Companion hk d Source Comments #

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

Instances

Instances details

(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 #
(Closed k, Ob j) => HasLimits (MonK k :: () -> () -> Type) ('MK j :: MonK k i a) '() Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods limitObj :: forall (d :: MonK k i '()). Ob d => Obj (Limit ('MK j :: MonK k i a) d) Source Comments # limit :: forall (d :: MonK k i '()). Ob d => O (Companion (MonK k) (Limit ('MK j :: MonK k i a) d)) ('MK j :: MonK k i a) ~> Companion (MonK k) d Source Comments # limitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()). (Ob d, Ob p) => (O (Companion (MonK k) p) ('MK j :: MonK k i a) ~> Companion (MonK k) d) -> p ~> Limit ('MK j :: MonK k i a) d Source Comments #

class (HasCompanions hk vk, Ob j) => HasColimits (vk :: CAT s) (j :: hk a i) (k :: s) where Source Comments #

weighted colimits

Associated Types

type Colimit (j :: hk a i) (d :: vk i k) :: vk a k Source Comments #

Methods

colimitObj :: forall (d :: vk i k). Ob d => Obj (Colimit j d) Source Comments #

colimit :: forall (d :: vk i k). Ob d => O (Companion hk d) j ~> Companion hk (Colimit j d) Source Comments #

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

Instances

Instances details

(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 colimitObj :: forall (d :: FUNK i k). Ob d => Obj (Colimit ('PK j) d) Source Comments # 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 #
(Monoidal k, Ob j) => HasColimits (MonK k :: () -> () -> Type) ('MK j :: MonK k a i) '() Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods colimitObj :: forall (d :: MonK k i '()). Ob d => Obj (Colimit ('MK j :: MonK k a i) d) Source Comments # colimit :: forall (d :: MonK k i '()). Ob d => O (Companion (MonK k) d) ('MK j :: MonK k a i) ~> Companion (MonK k) (Colimit ('MK j :: MonK k a i) d) Source Comments # colimitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()). (Ob d, Ob p) => (O (Companion (MonK k) d) ('MK j :: MonK k a i) ~> Companion (MonK k) p) -> Colimit ('MK j :: MonK k a i) d ~> p Source Comments #

type family TerminalObject (hk :: CAT s) (vk :: CAT s) :: s Source Comments #

Instances

Instances details

type TerminalObject PROFK FUNK Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type TerminalObject PROFK FUNK = ()

class HasCompanions hk vk => HasTerminalObject (hk :: CAT s) (vk :: CAT s) where Source Comments #

Associated Types

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

Methods

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

termUniv :: forall (i :: s) (j :: s) (p :: hk i j). (Ob0 vk i, Ob0 vk j, Ob p) => Sq '(p, Terminate hk vk j) '(I :: hk (TerminalObject hk vk) (TerminalObject hk vk), Terminate hk vk i) Source Comments #

Instances

Instances details

HasTerminalObject PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

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

Methods

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

termUniv :: forall i j (p :: PROFK i j). (Ob0 FUNK i, Ob0 FUNK j, Ob p) => Sq '(p, Terminate PROFK FUNK j) '(I :: PROFK (TerminalObject PROFK FUNK) (TerminalObject PROFK FUNK), Terminate PROFK FUNK i) Source Comments #

type family InitialObject (hk :: CAT s) (vk :: CAT s) :: s Source Comments #

Instances

Instances details

type InitialObject PROFK FUNK Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type InitialObject PROFK FUNK = VOID

class HasCompanions hk vk => HasInitialObject (hk :: CAT s) (vk :: CAT s) where Source Comments #

Associated Types

type Initiate (hk :: CAT s) (vk :: CAT s) (j :: s) :: vk (InitialObject hk vk) j Source Comments #

Methods

initiate :: forall (j :: s). Ob0 vk j => Obj (Initiate hk vk j) Source Comments #

initUniv :: forall (i :: s) (j :: s) (p :: hk i j). (Ob0 vk i, Ob0 vk j, Ob p) => Sq '(I :: hk (InitialObject hk vk) (InitialObject hk vk), Initiate hk vk j) '(p, Initiate hk vk i) Source Comments #

Instances

Instances details

HasInitialObject PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Initiate PROFK FUNK (j :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Initiate PROFK FUNK (j :: Type) = FUN (Initiate :: j -> VOID -> Type)

Methods

initiate :: Ob0 FUNK j => Obj (Initiate PROFK FUNK j) Source Comments #

initUniv :: forall i j (p :: PROFK i j). (Ob0 FUNK i, Ob0 FUNK j, Ob p) => Sq '(I :: PROFK (InitialObject PROFK FUNK) (InitialObject PROFK FUNK), Initiate PROFK FUNK j) '(p, Initiate PROFK FUNK i) Source Comments #

type family Product (hk :: CAT s) (vk :: CAT s) (a :: s) (b :: s) :: s Source Comments #

Instances

Instances details

type Product PROFK FUNK (a :: Type) (b :: Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type Product PROFK FUNK (a :: Type) (b :: Type) = (a, b)

class HasBinaryProducts (hk :: CAT s) (vk :: CAT s) where Source Comments #

Associated Types

type Fst (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk (Product hk vk i j) i Source Comments #

type Snd (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk (Product hk vk i j) j Source Comments #

type ProdV (hk :: CAT s) (vk :: CAT s) (f :: vk k i) (g :: vk k j) :: vk k (Product hk vk i j) Source Comments #

type ProdH (hk :: CAT s) (vk :: CAT s) (p :: hk j k) (q :: hk j' k') :: hk (Product hk vk j j') (Product hk vk k k') Source Comments #

Methods

fstObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Fst hk vk i j) Source Comments #

sndObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Snd hk vk i j) Source Comments #

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

prodUniv :: forall {i :: s} {j :: s} (k :: s) (k' :: s) (p :: hk k k') (i' :: s) (f' :: vk k' i') (a :: hk i i') (f :: vk k i) (j' :: s) (g' :: vk k' j') (b :: hk j j') (g :: vk k j). Sq '(p, f') '(a, f) -> Sq '(p, g') '(b, g) -> Sq '(p, ProdV hk vk f' g') '(ProdH hk vk a b, ProdV hk vk f g) Source Comments #

Instances

Instances details

HasBinaryProducts PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Fst PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Fst PROFK FUNK (a :: Type) (b :: Type) = FUN (FstCat :: a -> (a, b) -> Type)
type Snd PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Snd PROFK FUNK (a :: Type) (b :: Type) = FUN (SndCat :: b -> (a, b) -> Type)
type ProdV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i1 i2) ('SUB ('PK g) :: SUBCAT ProfRep PROFK i1 j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProdV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i1 i2) ('SUB ('PK g) :: SUBCAT ProfRep PROFK i1 j) = 'SUB ('PK (f :&&&: g)) :: SUBCAT ProfRep PROFK i1 (i2, j)
type ProdH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2)
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProdH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) = 'PK (p :**: q)

Methods

fstObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Fst PROFK FUNK i j) Source Comments #

sndObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Snd PROFK FUNK i j) 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 (ProdV PROFK FUNK f g) Source Comments #

prodUniv :: forall {i} {j} k k' (p :: PROFK k k') i' (f' :: FUNK k' i') (a :: PROFK i i') (f :: FUNK k i) j' (g' :: FUNK k' j') (b :: PROFK j j') (g :: FUNK k j). Sq '(p, f') '(a, f) -> Sq '(p, g') '(b, g) -> Sq '(p, ProdV PROFK FUNK f' g') '(ProdH PROFK FUNK a b, ProdV PROFK FUNK f g) Source Comments #

type family Coproduct (hk :: CAT s) (vk :: CAT s) (a :: s) (b :: s) :: s Source Comments #

Instances

Instances details

type Coproduct PROFK FUNK (a :: Type) (b :: Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type Coproduct PROFK FUNK (a :: Type) (b :: Type) = COPRODUCT a b

class HasBinaryCoproducts (hk :: CAT s) (vk :: CAT s) where Source Comments #

Associated Types

type Lft (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk i (Coproduct hk vk i j) Source Comments #

type Rgt (hk :: CAT s) (vk :: CAT s) (i :: s) (j :: s) :: vk j (Coproduct hk vk i j) Source Comments #

type CoprodV (hk :: CAT s) (vk :: CAT s) (f :: vk i k) (g :: vk j k) :: vk (Coproduct hk vk i j) k Source Comments #

type CoprodH (hk :: CAT s) (vk :: CAT s) (p :: hk j k) (q :: hk j' k') :: hk (Coproduct hk vk j j') (Coproduct hk vk k k') Source Comments #

Methods

lftObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Lft hk vk i j) Source Comments #

rgtObj :: forall (i :: s) (j :: s). (Ob0 vk i, Ob0 vk j) => Obj (Rgt hk vk i j) Source Comments #

coprodObj :: forall (j :: s) (a :: s) (b :: s) (f :: vk a j) (g :: vk b j). (Ob0 vk j, Ob0 vk a, Ob0 vk b, Ob f, Ob g) => Obj (CoprodV hk vk f g) Source Comments #

coprodUniv :: forall (i :: s) (i' :: s) (a :: hk i i') (k' :: s) (f' :: vk i' k') (k :: s) (p :: hk k k') (f :: vk i k) (j :: s) (j' :: s) (b :: hk j j') (g' :: vk j' k') (g :: vk j k). Sq '(a, f') '(p, f) -> Sq '(b, g') '(p, g) -> Sq '(CoprodH hk vk a b, CoprodV hk vk f' g') '(p, CoprodV hk vk f g) Source Comments #

Instances

Instances details

HasBinaryCoproducts PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Lft PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Lft PROFK FUNK (a :: Type) (b :: Type) = FUN (LftCat :: COPRODUCT a b -> a -> Type)
type Rgt PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Rgt PROFK FUNK (a :: Type) (b :: Type) = FUN (RgtCat :: COPRODUCT a b -> b -> Type)
type CoprodV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i j1) ('SUB ('PK g) :: SUBCAT ProfRep PROFK j2 j1)
Instance details Defined in Proarrow.Category.Bicategory.Prof type CoprodV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i j1) ('SUB ('PK g) :: SUBCAT ProfRep PROFK j2 j1) = 'SUB ('PK (f :\|\|\|: g)) :: SUBCAT ProfRep PROFK (COPRODUCT i j2) j1
type CoprodH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2)
Instance details Defined in Proarrow.Category.Bicategory.Prof type CoprodH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) = 'PK (p :++: q)

Methods

lftObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Lft PROFK FUNK i j) Source Comments #

rgtObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Rgt PROFK FUNK i j) Source Comments #

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

coprodUniv :: forall i i' (a :: PROFK i i') k' (f' :: FUNK i' k') k (p :: PROFK k k') (f :: FUNK i k) j j' (b :: PROFK j j') (g' :: FUNK j' k') (g :: FUNK j k). Sq '(a, f') '(p, f) -> Sq '(b, g') '(p, g) -> Sq '(CoprodH PROFK FUNK a b, CoprodV PROFK FUNK f' g') '(p, CoprodV PROFK FUNK f g) Source Comments #