The Coq mailing list

[Conor McBride <c.t.mcbride AT durham.ac.uk>]

Hi Christine

Christine Paulin wrote:
> 
> Looking about properties of John Major Equality (related to
> extensional equality), we encountered the following problem.
> It seems that the following property is not provable
> 
>         forall A1 A2 B1 B2 : Type,
>         forall f : (A1 -> B1),
>         forall g : (A2 -> B2),
>         forall x1 : A1, x2:A2,
>         f == g -> x1 == x2 -> (f x1) == (g x2)
> 
> == being JM equality

You're right. It isn't provable. There's nothing you can
eliminate!

Some observations:

(1) If we also equipped JM with the usual induction principle,
      given its constructor, (ie. fixing x : X, the one whose
      motive is indexed over {Y : Type, y : Y, q : x == y}),
      we would be able to eliminate x1 == x2 above...

(2) ...but we would still have problems with f : A -> B1,
      g : A -> B2. We need even more strength to solve this
      one, e.g. making -> injective.

However

(3) The following is easily provable (unless there's a universe
      level problem):

         forall A1 A2 B1 B2 : Type,
         forall f : (A1 -> B1),
         forall g : (A2 -> B2),
         forall x1 : A1, x2:A2,
         A1 == A2 -> B1 == B2 ->
         f == g -> x1 == x2 -> (f x1) == (g x2)

      The key thing is that we now have hypotheses which form
      a telescopic equation between two vectors in
        {A,B : Type, f : A -> B, x : A}

JM equality was designed to support the expression and elimination
of these telescopic equations, as they naturally show up in dependent
eliminations. Things stop working when you have completely
heterogeneous equations, like those you suggest above. In fact
JM equality isn't even symmetric or transitive for heterogeneous
equations. Also, one cannot refute 3 == cons.

So I guess an interesting question is whether these totally
heterogeneous problems ever show up `in real life'. Or, is (3)
enough? I don't know, but I'd be interested to find out.

Other interesting questions include

(4) should type constructors be injective and disjoint?
      At the moment, I suspect we can only refute equations between
      types if they happen to be non-isomorphic. I suppose there
      are perfectly good models of type theory which identify
      some isomorphic types.

      With my pragmatic head on, I think it might be convenient to
      make type constructors behave like data constructors in this
      way. With my dogmatic head on, I think that if I want things
      to behave like data, then they should actually be represented
      as data, by constructing a universe of types over a datatype
      of names whose constructors are injective and disjoint.

(5) should we have

      forall A B : Type, forall a : A, forall b : B, a == b -> A == B

    ?

Actually, (5) follows from the inductive elim rule for JM. Of course,
the inductive elim rule for JM falls outside Daria's precondition for
preservation of normalization...

Hoping this is useful.

Cheers

Conor