Axiom for induction for church encoding

[atennapel]

I'm trying to extend the system with an construct for induction for (non-recursive) church encodings.
I added the construct induction {T} x, with the typing rule:

x : T
---
induction {T} x : [generated induction principle for T and x]

For example for the unit type:

x : {t : *} -> t -> t
---
induction {{t : *} -> t -> t} x : {P : ({t : *} -> t -> t)-> *} -> P (\{t : *} (x : t). x) -> P x

The problem is with the reduction/semantic domain.
What we could do is simply

induction {T} x ~> \{P : T -> *}. x {P x}

But now type preservation (aka subject reduction) does not hold:

\(x : UnitType). induction {UnitType} x : (x : UnitType) -> {P : (UnitType -> *} -> P Unit -> P x
but
\(x : UnitType). \{P : UnitType -> *}. x {P x} : (x : UnitType) -> {P : (UnitType -> *} -> P x -> P x

Do you see anyway to preserve type preservation or is this approach doomed?

[atennapel]

I found the solution, the church encoded value has to be fully applied.