The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Robin

On 22 Jun 2009, at 10:08, Robin Green wrote:

> Is there a known implication between the axiom of dependent functional
> extensionality (by which I mean, Axiom functional_extensionality_dep  
> in
> Coq 8.2) and Streicher's axiom K, or vice-versa? If so, is it provable
> in Coq?

I think I have some sort of evidence that there is no
implication in either direction. In particular, it's
possible to come up with variations in which either
holds but not the other.

For one thing, remember why extensionality cannot hold
for the inductively defined equality: extensionality
implies that the closed terms (fn x => x + O) and
(fn x => O + x) are equal in the empty context, but in
the empty context, all proofs are canonical -- there is
no canonical proof that those two functions are equal.
If we add K *and its computation rule*, we preserve that
canonicity property, and we preserve the fact that in
the empty context, propositional equality and definitional
equality coincide, so our two functions are still not
provably equal. Here K holds but extensionality fails.
(Adding K without its computation rule cannot make more
things hold than adding K with its computation rule.)

The other way is trickier. In our PLPV 2007 paper,
"Observational Equality, Now", Thorsten, Wouter, and I
built a universe of sets with a subuniverse of
propositions: we defined equality by computing the
appropriate proposition to express the possibility
to transport between equal sets, and the observational
equivalence of values. This equality is extensional for
functions. Moreover, computation on proofs is strict
only when refuting absurdity, so transportation between
equal sets just relies on compatibility of the sets
themselves, and the system has the canonicity property.
The details aren't important, just the laziness. Our
propositions are built from the grammar

  PROP ::= 1
         | 0
         | PROP /\ PROP
         | forall x:SET. PROP

but we could just as well use 2 (bool) as the type of
trivially true propositions. As we are lazy, we
never inspect proofs of trivial propositions, so it
does no harm if there are two of them (apart from
breaking proof irrelvance, but that's an optional
extra). If we made that change, we would be in a
situation where extensionality holds, but uniqueness
of identity proofs does not.

Both function extensionality and uniqueness of identity
proofs hold in "extensional type theory", blessed and
cursed with the equality reflection rule:

   G |- q : s ==_S t
 ---------------------
   G |- s = t : S

which means that (excuse sloppy syntax)

  forall x y (q : x == y), q = refl_eq x

is (a) a well-formed proposition and (b) provable by
the usual induction principle for equality. I won't
do the derivation for extensionality, but they named
the type theory after it... The equality reflection
rule is a sledgehammer which makes lots of things
derivable, including (under hypotheses) a bunch of
stuff you'd prefer didn't happen. However, take away
the equality reflection rule and many of its famous
benefits become separable, and achievable
independently.

Hope this helps

Conor