Subject Reduction in Multi-Universe Type Theories

The Subject Reduction property states that if t is a term of type T in the context Γ, so is any term s to which t reduces. In this contribution the property is shown to be false in dependent-type theories with multiple universes and η-reduction by providing a judgement Γ ⊢ t : T and a one-step η-reduction t▷s such that Γ ⊢ s:T is impossible to derive. While the counterexample is immediate to check, the impossibility result requires setting up some machinery having interest of its own. The chapter also proposes an enhancement to the type system in which the claim that the Subject Reduction property holds has a strong justification.