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)$