The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

By the way, this works (fixed "f g : Arrow s t" to "f g : tm (Arrow s
t)" and explicitly told it the type of ty_eq:


(* Oops, Coq 8.4pl2 gets stack overflow?! *)
(* The types, here we just use a base type Nat and function types. *)
Inductive ty : Set :=
  | Nat
  | Arrow : ty -> ty -> ty.

(* The terms of a given type. *)
Parameter tm : ty -> Set.

(* Application. *)
Parameter app : forall {s t : ty}, tm (Arrow s t) -> tm s -> tm t.

(* Extensional equality of types. *)
Fixpoint ty_eq {t : ty} {struct t} : tm t -> tm t -> Prop :=
  match t with
    | Nat => (fun (n m : tm Nat) => n = m)
    | Arrow s t =>
        (fun f g : tm (Arrow s t) =>
           forall (x y : tm s), ty_eq x y -> ty_eq (app f x) (app g y))
  end.

So now I can continue with my argument: the equality on types is "ok",
it's just a fixed point, rather than an inductive definition. In your
definition you're trying to do too much at once by sticking in all
those "reducesTo", if you ask me.

With kind regards,

Andrej