# Homotopy Type Theory bilinear function > history (Rev #5)

## Definiton

Let $A$, $B$, and $C$ be abelian groups, and let $f:A \times B \to C$ be a function from the product type of $A$ and $B$ to $C$. Let us define the types

$isLeftDistributive(f) \coloneqq \prod_{a:A} \prod_{b:B} \prod_{c:B} f(a, b +_B c) = f(a, b) +_C f(a, c)$
$isRightDistributive(f) \coloneqq \prod_{a:A} \prod_{b:A} \prod_{c:B} f(a +_A b, c) = f(a, c) +_C f(b, c)$
$isBilinear(f) \coloneqq isLeftDistributive(f) \times isRightDistributive(f)$

$f$ is a bilinear function if the type $isBilinear(f)$ has a term.

We could define the type of all bilinear functions for abelian groups $A$, $B$, and $C$ as

$BilinearFunc(A, B, C) \prod_{f:A \times B \to C} isBilinear(f)$