In Part 1 we have developed a basic set of rules for
a simple quantitative dependently typed theory. The rules were, however, non-directional (or nondeterministic). By this,
I mean that there could be multiple instances of rules that would lead to the same conclusion. For example, consider the
sequent 0 A : *, 0 B : *, ω f : A → B, ω a : A ⊢ ω (f a) : B. We could derive this sequent at least in two ways: