Safe Haskell	None
Language	Haskell2010

Category.Product

Documentation

data (c1 :><: c2) a b where Source

Constructors

(:><:) :: (a ~ `(L a, R a)`, b ~ `(L b, R b)`) => c1 (L a) (L b) -> c2 (R a) (R b) -> (c1 :><: c2) a b

Instances

(Category k1 c1, Category k c2) => Category ((,) k k) ((:><:) k k k k c1 c2)
type Object ((,) k1 k) ((:><:) k k k1 k1 c1 c2) a = (Object k1 c1 (L k1 k a), Object k c2 (R k1 k a), (~) ((,) k1 k) a ((,) k1 k (L k1 k a) (R k1 k a)))

type family L t Source

Equations

L `(a, b)` = a

type family R t Source

Equations

R `(a, b)` = b

data Diag c where Source

Constructors

Instances

Category k c => Functor k ((,) k k) (Diag k c) (KProxy (k -> (,) k k))
TerminalMorphism * ((,) * ) (Diag (->)) (a, b) ((,) * * a b)
TerminalMorphism Constraint ((,) Constraint Constraint) (Diag Constraint (:-)) (a, b) ((,) Constraint Constraint a b)
type Domain k (Diag k c) = c
type FMap k ((,) k k) (Diag k c) a = (,) k k a a
type Codomain ((,) k k) (Diag k c) = (:><:) k k k k c c