Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.Limit

Documentation

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

Instances details

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

Associated Types

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

Methods

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

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

Instances details

Instance details

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

type family Product (kk :: CAT s) (a :: s) (b :: s) :: s Source Github #

Instances details

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

Associated Types

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

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

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

Methods

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

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

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

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

Instances details

Instance details

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

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

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