The Coq mailing list

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

On Sun, Aug 10, 2014 at 10:25 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
 wrote:
> The terms (v1:A1 -> B1)  and (v2:A2 -> B2) denote equal PI types in Nuprl
> iff
> A1 and A2 are equal types
> and
> forall terms a1 and a2 such that a1 and a2 are equal members of A1,
> B1[v1\a1] and B2[v2\a2] are equal types.

Unless you intend to introduce crazy recursive types this is not a
problem: equality on PI_{x:A} B(x) is defined in terms of equality on
A and equality on B, where these two equalities have been previously
defined. So this is still a fixpoint which uses structural recursion
on the structure of a type. Why would you be unhappy with that?

Funnily, I was going to provide this example:

(* 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} :=
  match t with
    | Nat => (fun (n m : tm Nat) => n = m)
    | Arrow s t =>
        (fun f g : Arrow s t =>
           forall (x y : tm s), ty_eq x y -> ty_eq (app f x) (app g y))
  end.

(* Oops, Coq 8.4pl2 gets stack overflow?! *)

But I get a stack overflow...