Skip to content

Instantly share code, notes, and snippets.

View qcfu-bu's full-sized avatar

Qiancheng Fu qcfu-bu

View GitHub Profile
@gabriel-barrett
gabriel-barrett / qtt2.md
Last active April 11, 2022 20:40
On QTT part 2

Bidirectional form of QTT rules

Nondeterminism of the non-directional rules

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: