Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?

Question

If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit:

UnitType = (t : *) -> t -> t
Unit = \(t : *) (x : t). x

And the add the following construct indUnit:

G |- P : UnitType -> *
G |- pu : P Unit
G |- u : UnitType
--------------
G |- indUnit P pu u : P u

With reduction rule:

indUnit P pu Unit ~> pu

Basically this adds induction over the Church-encoded unit type.

1. Is this consistent?
2. If we change the reduction rule to:

indUnit P pu x ~> x (P x) pu (if x is a closed term)

Is it still consistent?

It seems to me that this is consistent.

Answer 1

Yes, it's consistent. Probably the easiest account is in my 2013 CSL paper with Derek Dreyer, Internalizing Parametricity in the Extensional Calculus of Construction, which is all about adding this style of parametricity axiom to the CoC.