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.


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.

| cite | improve this answer | |
  • 2
    $\begingroup$ Thanks! That's good to know. I had a small question about that paper: at the end of 5.3 it says "Details are given in the appendix.", but I am unable to find these details in the appendix. $\endgroup$ – Labbekak Mar 19 at 14:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.