The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, May 18, 2012 at 4:33 AM, Andrej Bauer 
<andrej.bauer AT andrej.com>
 wrote:
> 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.

Here's something I just thought of which might allow for a definition
where the inductive constructor goes on the right...

Inductive ibubble (A:Type) : nat -> forall B:Type, B -> B -> Type :=
| ibubble_base : forall x0 y0:A, ibubble A 0 A x0 y0
| build_ibubble : forall (n:nat) (B:Type) (xn yn:B),
  ibubble A n B xn yn -> forall (xn1 yn1:xn=yn),
                         ibubble A (S n) (xn=yn) xn1 yn1.

Inductive bubble (A:Type) (n:nat) : Type :=
| bubble_existT : forall (B:Type) (x y:B),
  ibubble A n B x y -> bubble A n.

So "ibubble" is essentially bubble indexed by the final elements xn,
yn and their type.  I'm not sure how much easier or harder this might
be to work with in practice than the original bubble type you defined.
-- 
Daniel Schepler