The Coq mailing list

[Nils Anders Danielsson <nad AT chalmers.se>]

On 2012-02-27 09:44, Arnaud Spiwack wrote:
> My feverish brain does not manage to see under which precise
> assumption this holds. However, I doubt it'll work for Coq (I'm
> guessing the fact that the type argument is taken in a predicative
> sort rather than an impredicative one would be the issue).

It is easy to prove that the two types are isomorphic:

  Set Implicit Arguments.

  Inductive Eq1 (A : Type) (x : A) : A -> Prop :=
    refl1 : Eq1 x x.

  Inductive Eq2 (A : Type) : A -> A -> Prop :=
    refl2 (x : A) : Eq2 x x.

  Record Iso (A B : Prop) : Prop :=
    { to      : A -> B
    ; from    : B -> A
    ; to_from : forall x, to (from x) = x
    ; from_to : forall x, from (to x) = x
    }.

  Lemma Eq1_to_Eq2 (A : Type) (x y : A) (eq : Eq1 x y) : Eq2 x y.
  Proof.
    intros.
    destruct eq.
    exact (refl2 _).
  Defined.

  Lemma Eq2_to_Eq1 (A : Type) (x y : A) (eq : Eq2 x y) : Eq1 x y.
  Proof.
    intros.
    destruct eq.
    exact (refl1 _).
  Defined.

  Lemma isomorphic (A : Type) (x y : A) : Iso (Eq1 x y) (Eq2 x y).
  Proof.
    intros.
    refine (Build_Iso (fun eq => Eq1_to_Eq2 eq)
                      (fun eq => Eq2_to_Eq1 eq) _ _).
      intros eq.
      destruct eq.
      exact (eq_refl _).
    intros eq.
    destruct eq.
    exact (eq_refl _).
  Defined.

Given the isomorphism it is straightforward to define Paulin-Mohring's
variant of J (eliminating into Type) for both types:

  Lemma J1 (A : Type) (x : A)
           (P : forall y, Eq1 x y -> Type)
           (p : P x (refl1 x))
           (y : A) (eq : Eq1 x y) : P y eq.
  Proof.
    intros.
    destruct eq.
    exact p.
  Defined.

  Lemma J2 (A : Type) (x : A)
           (P : forall y, Eq2 x y -> Type)
           (p : P x (refl2 x))
           (y : A) (eq : Eq2 x y) : P y eq.
  Proof.
    intros.
    set (P' := fun y => fun eq => P y (Eq1_to_Eq2 eq)).
    set (p' := J1 P' p (Eq2_to_Eq1 eq)).
    unfold P' in p'.
    set (lemma := to_from (isomorphic x y) eq).
    unfold isomorphic, to, from in lemma.
    rewrite lemma in p'.
    exact p'.
  Defined.

--
/NAD