extended-categories-0.1.0: Extended Categories

Safe HaskellNone
LanguageHaskell2010

Product

Documentation

class Category c => ProductCategory c where Source

Associated Types

type a >< b :: k Source

Methods

productObjectMap :: Tagged `(c, a, b)` ((Object c a, Object c b) :- Object c (a >< b)) Source

univProduct :: forall a b. Tagged `(c, a, b)` ((Object c a, Object c b) :- TerminalMorphism (Diag c) (a >< b) `(a, b)`) Source

proj1 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged b (c (a >< b) a) Source

proj2 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged a (c (a >< b) b) Source

(&&&) :: forall c a b1 b2. ProductCategory c => c a b1 -> c a b2 -> c a (b1 >< b2) Source

(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (a1 >< a2) (b1 >< b2) Source

data ProductF c where Source

Constructors

ProductF :: ProductCategory c => ProductF c 

Instances

ProductCategory k c => Functor ((,) k k) k (ProductF k c) (KProxy ((,) k k -> k)) 
type Codomain k (ProductF k c) = c 
type FMap ((,) k k) k (ProductF k c) a = (><) k (L k k a) (R k k a) 
type Domain ((,) k k) (ProductF k c) = (:><:) k k k k c c