Abstract: I'll discuss ongoing work on formulating proof-theoretically weak dependent type theories (of strength polytime and primitive recursive) that permit some higher type and large eliminations. Motivations include constructive reverse mathematics and eventually also a weak homotopy type theory.