The Coq mailing list

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

After many experiments, I have sort of settled for the following
definition. The nesting goes the wrong way, but at least we get the
types we want. Many thanks to everyone, and especially to Daniel
Schepler whose code inspired the definition below.

Fixpoint bubble (A:Type) (n:nat) : Type :=
  match n with
    | 0 => (A * A)%type
    | S m => { x : A & { y : A & bubble (x=y) m } }
  end.

Parameter A : Type.
Parameter a b c : A.
Parameter p q : a = b.
Parameter r : b = c.
Parameter h g : p = q.

Notation "( a ; b ; p )" := (existT _ a (existT _ b p)).

Eval compute in bubble A 1.

Let bub : bubble A 1 := (a ; b ; (p, q)).
Let bab : bubble A 2 := (a ; b ; (p ; q; (h, g))).

With kind regards,

Andrej