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
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.
- Is this consistent?
- 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.