The Coq mailing list

[Michael Shulman <viritrilbia AT gmail.com>]

2010/3/27 Pierre-Marie Pédrot 
<pierremarie.pedrot AT ens-lyon.fr>:
>> More specifically, Thomas Steicher exhibited models of Type Theory where
>> there are non standard closed proofs of (A = A). In these models, pf
>> might be one of those non-standard proofs (i.e. semantically distinct
>> from (refl_equal A)). Since Type (the type of A) is not decidable,
>> you're out of luck without Streicher's K axiom (or its equivalent in Coq).
>
> Well, I still don't grasp the subtle difference between the two
> innocuous examples ; the existence of non-standard equality proofs
> should also forbid the reduction of the second equality...

My intuition for nonstandard proofs of (A=A) is that they can be
thought of as nontrivial *automorphisms* of A.  This is literally the
case in the Hoffman-Streicher groupoid model, and also in newer
homotopical models.

Thus in the second case, we are given an automorphism "pf" of X, and
we want to construct an isomorphism between X and the result of
reducing X along "pf."  But such an isomorphism is essentially given
by "pf" itself.

However, in the first case, we are given an automorphism "pf" of A,
while X is only an element of A, and we want to construct an
isomorphism between X and the result of reducing it along "pf," which
in this case is basically the *image* of X under the automorphism "pf"
of A.  But just because "pf" is an automorphism of A, doesn't mean
that it maps every element of A to something isomorphic to itself.

But I'm still pretty new to this myself, so possibly someone will tell
me that that's all wrong.

Anyway, as long as I'm commenting on this, let me say that I hope that
if Coq is eventually extended in some way which makes axiom K or its
equivalents provable, that it will at least be possible to turn off
such an extension.  Since my interest is largely in models such as
groupoids and homotopy theory, I would not want uniqueness of
reflexive identity proofs to be built into the system unavoidably.

Mike