The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 16 May 2012 10:54:13 +0200,
Andrej Bauer 
<andrej.bauer AT andrej.com>
 a écrit :

> > Fixpoint endpoints (n : nat) (X : Type) : Type :=
> >  match n return Type with
> >    | 0 => unit
> >    | S n => {e : endpoints n X & path n X e & path n X e}
> >  end
> > with path (n : nat) (X : Type) (e : endpoints n X) : Type :=
> >  match n return Type with
> >    | 0 => X
> >    | S n =>
> >      match e with
> >        | existT2 _ x y => x = y
> >      end
> >  end.
> >
> > but Coq doesn't like "endpoints" showing up in the type signature of
> > path. Hope this helps.
> 
> Thanks! This is precisely the sort of thing I need. How do I make Coq
> happy?
> 
> With kind regards,
> 
> Andrej

Inductive endpoints (T : Type) : nat -> Type :=
| End : T -> endpoints T O
| Step : forall n (a b : endpoints T n), a = b -> endpoints T (S n).

I don't know if it is what you wish.
Typically, if you have something of type "endpoints T 2", you can
decompose it into:
a : T
b : T
c : T
d : T
Hab : End a = End b (* thus a = b *)
Hcd : End c = End d (* thus c = d *)
Habcd : Step Hab = Step Hcd