FibredOriented structures equipped with an Additive and Multiplicative structure satisfying the laws of distributivity.

Properties Let d be a Distributive structure, then holds:

1. For all g in d and r in Root d with end g == start r holds: zero r * g == zero r' where r' == start g :> end r.
2. For all g, a and b in d with root a == root b and start a == end g holds: (a + b) * g == a*g + b*g.
3. For all f in d and r in Root d with start f == end r holds: f * zero r == zero r' where r' = start r :> end f.
4. For all f, a and b in d with root a == root b and start f == end a holds: f*(a + b) == f*a + f*b.

Note If d is interpreted as a small category C then it is usually called preadditive. If d is also Abelian then C is also usually called abelian.

type representing the class of Distributive structures.

helper class to avoid undecidable instances.

tau for Dst.

transposable distributive structures.

Property Let d be a TransposableDistributive structure, then holds:

1. For all r in Root d holds: transpose (zero r) == zero (transpose r)
2. For all a, b in d with root a == root b holds: transpose (a + b) == transpose a + transpose b.