Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Product

Documentation

data PRODK (jj :: CAT j) (kk :: CAT k) (j1 :: (j, k)) (k1 :: (j, k)) where Source Comments #

Constructors

PROD :: forall {j} {k} (jj :: CAT j) (j1 :: (j, k)) (k1 :: (j, k)) (kk :: CAT k). jj (Fst j1) (Fst k1) -> kk (Snd j1) (Snd k1) -> PRODK jj kk j1 k1

Instances

Instances details

(Bicategory jj, Bicategory kk) => Bicategory (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

iObj :: forall (i :: (j, k)). Ob0 (PRODK jj kk) i => Obj (I :: PRODK jj kk i i) Source Comments #

o :: forall {i :: (j, k)} (j0 :: (j, k)) (k0 :: (j, k)) (a :: PRODK jj kk j0 k0) (b :: PRODK jj kk j0 k0) (c :: PRODK jj kk i j0) (d :: PRODK jj kk i j0). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: (j, k)) (j0 :: (j, k)) (ps :: PRODK jj kk i j0) (qs :: PRODK jj kk i j0) r. ((Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => O (I :: PRODK jj kk j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => a ~> O (I :: PRODK jj kk j j) a Source Comments #

rightUnitor :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => O a (I :: PRODK jj kk i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: (j, k)} {j0 :: (j, k)} (a :: PRODK jj kk i j0). (Ob0 (PRODK jj kk) i, Ob0 (PRODK jj kk) j0, Ob a) => a ~> O a (I :: PRODK jj kk i i) Source Comments #

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

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

(Comonad (PRODFST m), Comonad (PRODSND m), Ob m) => Comonad (m :: PRODK jj kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

epsilon :: m ~> (I :: PRODK jj kk a a) Source Comments #

delta :: m ~> O m m Source Comments #

(Monad (PRODFST m), Monad (PRODSND m), Ob m) => Monad (m :: PRODK jj kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

eta :: (I :: PRODK jj kk a a) ~> m Source Comments #

mu :: O m m ~> m Source Comments #

(Adjunction (PRODFST l) (PRODFST r), Adjunction (PRODSND l) (PRODSND r), Ob l, Ob r) => Adjunction (l :: PRODK jj kk c d) (r :: PRODK jj kk d c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

unit :: (I :: PRODK jj kk c c) ~> O r l Source Comments #

counit :: O l r ~> (I :: PRODK jj kk d d) Source Comments #

(Equipment hj vj, Equipment hk vk) => Equipment (PRODK hj hk :: (j, k) -> (j, k) -> Type) (PRODK vj vk :: (j, k) -> (j, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

mapConjoint :: forall {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0) (g :: PRODK vj vk j0 k0). (f ~> g) -> Conjoint (PRODK hj hk) g ~> Conjoint (PRODK hj hk) f Source Comments #

conjToId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => Conjoint (PRODK hj hk) (I :: PRODK vj vk k k) ~> (I :: PRODK hj hk k k) Source Comments #

conjFromId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => (I :: PRODK hj hk k k) ~> Conjoint (PRODK hj hk) (I :: PRODK vj vk k k) Source Comments #

conjToCompose :: forall {k1 :: (j, k)} {j0 :: (j, k)} {k2 :: (j, k)} (f :: PRODK vj vk j0 k2) (g :: PRODK vj vk k1 j0). Obj f -> Obj g -> Conjoint (PRODK hj hk) (O f g) ~> O (Conjoint (PRODK hj hk) g) (Conjoint (PRODK hj hk) f) Source Comments #

conjFromCompose :: forall {j1 :: (j, k)} {j2 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j2 k0) (g :: PRODK vj vk j1 j2). Obj f -> Obj g -> O (Conjoint (PRODK hj hk) g) (Conjoint (PRODK hj hk) f) ~> Conjoint (PRODK hj hk) (O f g) Source Comments #

comConUnit :: forall {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0). Obj f -> (I :: PRODK hj hk j j) ~> O (Conjoint (PRODK hj hk) f) (Companion (PRODK hj hk) f) Source Comments #

comConCounit :: forall {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0). Obj f -> O (Companion (PRODK hj hk) f) (Conjoint (PRODK hj hk) f) ~> (I :: PRODK hj hk k k) Source Comments #

(HasCompanions hj vj, HasCompanions hk vk) => HasCompanions (PRODK hj hk :: (j, k) -> (j, k) -> Type) (PRODK vj vk :: (j, k) -> (j, k) -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

mapCompanion :: forall {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0) (g :: PRODK vj vk j0 k0). (f ~> g) -> Companion (PRODK hj hk) f ~> Companion (PRODK hj hk) g Source Comments #

compToId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => Companion (PRODK hj hk) (I :: PRODK vj vk k k) ~> (I :: PRODK hj hk k k) Source Comments #

compFromId :: forall (k0 :: (j, k)). Ob0 (PRODK vj vk) k0 => (I :: PRODK hj hk k k) ~> Companion (PRODK hj hk) (I :: PRODK vj vk k k) Source Comments #

compToCompose :: forall {i :: (j, k)} {j0 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j0 k0) (g :: PRODK vj vk i j0). Obj f -> Obj g -> Companion (PRODK hj hk) (O f g) ~> O (Companion (PRODK hj hk) f) (Companion (PRODK hj hk) g) Source Comments #

compFromCompose :: forall {j1 :: (j, k)} {j2 :: (j, k)} {k0 :: (j, k)} (f :: PRODK vj vk j2 k0) (g :: PRODK vj vk j1 j2). Obj f -> Obj g -> O (Companion (PRODK hj hk) f) (Companion (PRODK hj hk) g) ~> Companion (PRODK hj hk) (O f g) Source Comments #

(CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => CategoryOf (PRODK jj kk ik jl) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Product type (~>) = Prod :: PRODK jj kk ik jl -> PRODK jj kk ik jl -> Type

(CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => Promonad (Prod :: PRODK jj kk ik jl -> PRODK jj kk ik jl -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

id :: forall (a :: PRODK jj kk ik jl). Ob a => Prod a a Source Comments #

(.) :: forall (b :: PRODK jj kk ik jl) (c :: PRODK jj kk ik jl) (a :: PRODK jj kk ik jl). Prod b c -> Prod a b -> Prod a c Source Comments #

(CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => Profunctor (Prod :: PRODK jj kk ik jl -> PRODK jj kk ik jl -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

dimap :: forall (c :: PRODK jj kk ik jl) (a :: PRODK jj kk ik jl) (b :: PRODK jj kk ik jl) (d :: PRODK jj kk ik jl). (c ~> a) -> (b ~> d) -> Prod a b -> Prod c d Source Comments #

(\\) :: forall (a :: PRODK jj kk ik jl) (b :: PRODK jj kk ik jl) r. ((Ob a, Ob b) => r) -> Prod a b -> r Source Comments #

type Ob0 (PRODK jj kk :: (j2, k2) -> (j2, k2) -> Type) (jk :: (j1, k1)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type Ob0 (PRODK jj kk :: (j2, k2) -> (j2, k2) -> Type) (jk :: (j1, k1)) = (Ob0 jj (Fst jk), Ob0 kk (Snd jk))

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type I = 'PROD (I :: jj (Fst i) (Fst i)) (I :: kk (Snd i) (Snd i)) :: PRODK jj kk i i

type O ('PROD a b :: PRODK jj kk j2 k2) ('PROD c d :: PRODK jj kk i j2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type O ('PROD a b :: PRODK jj kk j2 k2) ('PROD c d :: PRODK jj kk i j2) = 'PROD (O a c) (O b d) :: PRODK jj kk i k2

type Companion (PRODK hj hk :: (j1, k1) -> (j1, k1) -> Type) (fg :: PRODK vj vk j2 k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type Companion (PRODK hj hk :: (j1, k1) -> (j1, k1) -> Type) (fg :: PRODK vj vk j2 k2) = 'PROD (Companion hj (PRODFST fg)) (Companion hk (PRODSND fg)) :: PRODK hj hk j2 k2

type Conjoint (PRODK hj hk :: (j1, k1) -> (j1, k1) -> Type) (fg :: PRODK vj vk j2 k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type Conjoint (PRODK hj hk :: (j1, k1) -> (j1, k1) -> Type) (fg :: PRODK vj vk j2 k2) = 'PROD (Conjoint hj (PRODFST fg)) (Conjoint hk (PRODSND fg)) :: PRODK hj hk k2 j2

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type (~>) = Prod :: PRODK jj kk ik jl -> PRODK jj kk ik jl -> Type

type Ob (p :: PRODK jj kk ik jl) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type Ob (p :: PRODK jj kk ik jl) = (Ob (PRODFST p), Ob (PRODSND p), p ~ ('PROD (PRODFST p) (PRODSND p) :: PRODK jj kk ik jl))

type family PRODFST (p :: PRODK jj kk j1 k1) :: jj (Fst j1) (Fst k1) where ... Source Comments #

Equations

PRODFST ('PROD p q :: PRODK jj kk j2 k2) = p

type family PRODSND (p :: PRODK jj kk j1 k1) :: kk (Snd j1) (Snd k1) where ... Source Comments #

Equations

PRODSND ('PROD p q :: PRODK jj kk j2 k2) = q

type family Fst (p :: (j, k)) :: j where ... Source Comments #

Equations

Fst ('(a, b) :: (j, k)) = a

type family Snd (p :: (j, k)) :: k where ... Source Comments #

Equations

Snd ('(a, b) :: (j, k)) = b

data Prod (a :: PRODK jj kk j1 k1) (b :: PRODK jj kk j1 k1) where Source Comments #

Constructors

Prod
Fields :: forall {j} {jj :: CAT j} {k} {j1 :: (j, k)} {k1 :: (j, k)} {kk :: CAT k} (a1 :: jj (Fst j1) (Fst k1)) (b1 :: jj (Fst j1) (Fst k1)) (c :: kk (Snd j1) (Snd k1)) (d :: kk (Snd j1) (Snd k1)). { fst :: a1 ~> b1 , snd :: c ~> d } -> Prod ('PROD a1 c :: PRODK jj kk j1 k1) ('PROD b1 d :: PRODK jj kk j1 k1)

Instances

Instances details

(CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => Promonad (Prod :: PRODK jj kk ik jl -> PRODK jj kk ik jl -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product Methods id :: forall (a :: PRODK jj kk ik jl). Ob a => Prod a a Source Comments # (.) :: forall (b :: PRODK jj kk ik jl) (c :: PRODK jj kk ik jl) (a :: PRODK jj kk ik jl). Prod b c -> Prod a b -> Prod a c Source Comments #
(CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => Profunctor (Prod :: PRODK jj kk ik jl -> PRODK jj kk ik jl -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product Methods dimap :: forall (c :: PRODK jj kk ik jl) (a :: PRODK jj kk ik jl) (b :: PRODK jj kk ik jl) (d :: PRODK jj kk ik jl). (c ~> a) -> (b ~> d) -> Prod a b -> Prod c d Source Comments # (\\) :: forall (a :: PRODK jj kk ik jl) (b :: PRODK jj kk ik jl) r. ((Ob a, Ob b) => r) -> Prod a b -> r Source Comments #