An invertible mapping between a and b in category cat.

Laws

fwd . bwd ≡ id
bwd . fwd ≡ id

A Bifunctor t is a Functor whose domain is the product of two categories. GBifunctor is equivalent to the ordinary Bifunctor class but we replace the implicit (->) Category with three distinct higher kinded variables cat1, cat2, and cat3 allowing the user to pickout a functor from \(cat_1 \times cat_2\) to \(cat_3\).

Laws

gbimap id id ≡ id
grmap id ≡ id
glmap id ≡ id

gbimap (f . g) (h . i) ≡ gbimap f h . gbimap g i
grmap (f . g) ≡ grmap f . grmap g
glmap (f . g) ≡ glmap f . glmap g

Infix operator for gbimap.

Covariantally map over the right variable.

Covariantally map over the left variable.

A bifunctor \(\_\otimes\_: \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) is Associative if it is equipped with a natural isomorphism of the form \(\alpha_{x,y,z} : (x \otimes (y \otimes z)) \to ((x \otimes y) \otimes z)\), which we call assoc.

Laws

fwd assoc . bwd assoc ≡ id
bwd assoc . fwd assoc ≡ id

A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) that maps out of the product category \(\mathcal{C} \times \mathcal{C}\) is a Tensor if it has:

1. a corresponding identity type \(I\)
2. Left and right unitor operations \(\lambda_{x} : 1 \otimes x \to x\) and \(\rho_{x} : x \otimes 1 \to x\), which we call unitr and unitl.

Laws

fwd unitr (a ⊗ i) ≡ a
bwd unitr a ≡ (a ⊗ i)

fwd unitl (i ⊗ a) ≡ a
bwd unitl a ≡ (i ⊗ a)

A bifunctor \(\_ \otimes\_ \ : \mathcal{C} \times \mathcal{C} \to \mathcal{C}\) is Symmetric if it has a product operation \(B_{x,y} : x \otimes y \to y \otimes x\) such that \(B_{x,y} \circ B_{x,y} \equiv 1_{x \otimes y}\), which we call swap.

Laws

swap . swap ≡ id