First of all let's extend this calculus by several type formers:

# The usual ones:

(A, B) # pair, (multiplicative) product of A and B

Either(A, B) # disjoint sum, (additive) sum of A and B

# The unusual ones:

Choose(A, B) # the user may choose to take A or B from the box.

Superposition(A, B) # the user must uniformly transform both A and B

(The last one is very much like Either(A, B) except the user cannot get to know which one of the cases really occurs: in some models Superposition(A, B) encodes quantum superpositions of objects. The Schrödinger cat is Superposition(LivingCat, DeadCat) as long as the box is closed and becomes Either(LivingCat, DeadCat) in the context of observer who opened the box. In game/resource semantics it's simply the pair with delayed choice.)

**Intuitionistic types**

First of all, let's give a way how to restore usual intuitionistic types. Intuitionistic type or ValueType is a type T equipped with structure of symmetric comonoid (with comultiplication clone : T -o (T, T) and counit discard : T -o Unit). On such types we can define usual lambda terms (x : X) -> Y that use the variable x any finite number of times: these lambda-terms can be rewritten into linear ones using clone and discard operations on X, the symmetry of comonoid X is precisely the property that all such interpretations (i.e. all possible combinations and permutations of clonings and discardings yielding the same number of copies) produce

^{(up to coherent equivalence)}equal results. By A -> B (where A is a symmetric comonoid and B any type) we'll denote the type of usual lambda terms taking values of A and producing Bs.

We can also see that pairs (A, B) and disjoint sums Either(A, B) of value types are naturally value types as well. We also want all types without destructors (in particular, universes) to be value types as well, then we can define dependent sums and products (x : X, Y(x)), (x : X) -> Y(x), as long as X is a value type and Y : X -> Type.

In order to proceed do Id-types and type families we'll need to add the value type former Ghost(T) with constructor ⧘_⧙ : T -> Ghost(T) and no destructors guaranteing that all functions depending on Ghost types use their value only as indices and are parametric in these. Now it would probably be not contradictory to require existence of inductive type families indexed by ghost types and universes, perhaps even with any value types. And for any type T there should be a natural Id type _=_ : (x : Ghost(T), t : Ghost(T)) -> Type

This type should be automatically equipped with a structure of a "weak Groupoid", i.e. weak partial Hopf algebra, so its elements are allowed to be cloned, but cloning is not necessary symmetric, only coassociative up to coherent equivalence.