How to evaluate primitive induction principles?

[atennapel]

Let's say we add a primitive unit type to the language:

UnitTy : *
Unit : UnitTy

Now we want an induction principle, so we add a primitive indUnit with the following typing rule:

P : UnitTy -> *
p : P Unit
x : UnitTy
-------------------
indUnit P p x : P x

But how should indUnit be evaluated? We could evaluate it as:

indUnit P p x ~> p

But now the type is not preserved, we go from P x to P Unit. So then the elaboration may not typecheck any longer.

How can a unit type (or any inductive type) with an induction priniciple be added such that evaluation will work out with type preservation? Any resources are appreciated.

EDIT: Just realized that indUnit P p x should only be reduced if x reduces to Unit, in which case everything works out fine.