8
$\begingroup$

The extensional version of Intuitionistic Type Theory is usually formulated in a way that makes extensional concepts like functional extensionality derivable. In particular, equality reflection, together with $\xi$- and $\eta$-rules for $\Pi$ types are enough to get the standard formulation of $\textsf{funext}$

$\Pi_{x \in A}\textsf{Eq}(B(x), f x, g x) \implies \textsf{Eq}(\Pi_{x \in A}B(x), f, g)$

where $\textsf{Eq}$ is the identity type with rules of reflection and uniqueness of identity proofs (see page 61 of M. Hofmann, Extensional Constructs in Intensional Type Theory).

But what if $\eta$ is not assumed? In particular, consider a standard intensional Martin-Löf type theory with $\Pi$ formulated with $\xi$-rule and "elimination as application", and to which we only add an extensional identity type $\textsf{Eq}$ as described above. What is the power of the resulting theory, in terms of extensional constructs (like functional extensionality) that can be derived in it? It seems to me that neither $\eta$ nor $\textsf{funext}$ should be derivable, although we can surely get to a weaker version using equality reflection and $\xi$:

$\Pi_{x \in A}\textsf{Eq}(B(x), f x, g x) \implies \textsf{Eq}(\Pi_{x \in A}B(x), \lambda x . f x, \lambda x . g x)$

(so, from $\eta$ we could get to $\textsf{funext}$, and obviously vice versa). Here R. Garner shows that the $\eta$ rule is not derivable if $\Pi$ types are given with "elimination as application". He does that for an intensional theory, but the same argument should be applicable in the presence of $\textsf{Eq}$ too, I think.

Are my suspicions correct? Are there any proofs of this in the literature, and in general any investigations on the kind of extensional constructs that can be derived in such minimal versions of ETT? What do we gain by only adding $\textsf{Eq}$, in the presence of such a "limited" $\Pi$ type (no $\eta$ equality, and no induction principle)?

$\endgroup$
  • $\begingroup$ A day late and a dollar short, but you might want to e-mail Garner himself to get his thoughts. I agree that the "model construction" which is really translating to a similar type theory with "known" meta-theory seems plausible in the extensional setting as well. $\endgroup$ – cody Jul 17 '17 at 18:12

Your Answer

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

Browse other questions tagged or ask your own question.