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
(Bicategory jj, Bicategory kk) => Bicategory (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Comments # | |
Defined in Proarrow.Category.Bicategory.Product Methods o :: forall {k1 :: (j, k)} (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0) (b :: PRODK jj kk i j0) (c :: PRODK jj kk j0 k1) (d :: PRODK jj kk j0 k1). (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). Obj a -> O (I :: PRODK jj kk i i) a ~> a Source Comments # leftUnitorInv :: forall (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0). Obj a -> a ~> O (I :: PRODK jj kk i i) a Source Comments # rightUnitor :: forall (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0). Obj a -> O a (I :: PRODK jj kk j j) ~> a Source Comments # rightUnitorInv :: forall (i :: (j, k)) (j0 :: (j, k)) (a :: PRODK jj kk i j0). Obj a -> a ~> O a (I :: PRODK jj kk j j) Source Comments # associator :: forall {j1 :: (j, k)} {k1 :: (j, k)} (i :: (j, k)) (j2 :: (j, k)) (a :: PRODK jj kk i j2) (b :: PRODK jj kk j2 j1) (c :: PRODK jj kk j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments # associatorInv :: forall {j1 :: (j, k)} {k1 :: (j, k)} (i :: (j, k)) (j2 :: (j, k)) (a :: PRODK jj kk i j2) (b :: PRODK jj kk j2 j1) (c :: PRODK jj kk j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments # | |
(CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => CategoryOf (PRODK jj kk ik jl) Source Comments # | |
Defined in Proarrow.Category.Bicategory.Product | |
(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 # | |
(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 # | |
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, k) -> (j2, k) -> Type) (jk :: (j1, k1)) Source Comments # | |
type I Source Comments # | |
type O ('PROD a b :: PRODK jj kk i j2) ('PROD c d :: PRODK jj kk j2 k1) Source Comments # | |
type (~>) Source Comments # | |
type Ob (p :: PRODK jj kk ik jl) Source Comments # | |
data Prod (a :: PRODK jj kk j1 k1) (b :: PRODK jj kk j1 k1) where Source Comments #
Constructors
Prod :: 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)). (a1 ~> b1) -> (c ~> d) -> Prod ('PROD a1 c :: PRODK jj kk j1 k1) ('PROD b1 d :: PRODK jj kk j1 k1) |
Instances
(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 # | |
(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 # | |
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 # |