In Coq, are there types A,B and functions f, g : A -> B such that f = g propositionally but f is not equal to g definitionally?

If the axiom of functional extensionality is assumed, this is obviously true. It's not clear to me whether there is an example here that doesn't use axioms.

  • 5
    $\begingroup$ If a = b non-definitionally, and f is a binary function, then f a = f b is a (likely non-definitional) equality of unary functions. $\endgroup$
    – Jason Rute
    Commented Apr 7 at 0:31
  • 1
    $\begingroup$ That's a great answer, thank you very much! As a follow up, can you think of any examples of a,b which are closed and propositionally equal but not equal? It would be interesting to strengthen the question to require A,B, f,g to be closed, but this could be a separate question. $\endgroup$ Commented Apr 7 at 0:52
  • 6
    $\begingroup$ If all the terms involved are closed, by canonicity any proof of f = g is convertible to refl, so necessarily f is convertible to g. This also assumes the proof of f = g to be closed, but obviously if you work under a context you can get garbage equalities like 0 = 1. $\endgroup$ Commented Apr 7 at 12:00
  • 1
    $\begingroup$ In Pierre-Marie Pédrot's answer, the relevant canonicity theorem only needs to apply to the identity type not to an arbitrary type. I don't think that there is any formal proof that Coq (or rather its idealized theory PCUIC following metacoq to put aside implementation bugs) satisfy canonicity, but at least identity types do satisfy canonicity in MLTT+Pi+Sigma+Id+1 universe (as shown in this Coq dev). $\endgroup$ Commented Apr 7 at 12:57
  • 2
    $\begingroup$ Stressing out the leading in Coq from the original question, here is an actual instance. $\endgroup$ Commented Apr 8 at 13:51


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.