The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Pierre Corbineau wrote:
> 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...

But thanks anyway, I should accept this axiom and live with that.

> On a more speculative side, I am working on adding the K axiom to Coq's
> Type system by relaxing some typing constraints, but I cannot give you
> any date for completion.

It may be really useful that for dependently-typed programming you don't
need to have a bunch of axioms in your context.

Thanks for this disillusion,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature