In "Graded Modal Dependent Type Theory" why does the sigma not account for value-level usages (like QTT and "A graded dependent type system with usage-aware semantics" do)? A use for this is sigma modules like `(0 Nat : Type) ** (Z : Nat) ** ...`, with erasure of `Nat`.
