The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Benjamin Pierce wrote:
> Suppose one wanted to define isomorphisms in the following slightly 
> unusual fashion:
>
> Inductive Dir : Set := R | L.
> Definition swap (d:Dir) := match d with R => L | L => R end.
>
> Module Type Iso.
> Parameter S : Dir -> Set.
> Parameter f : forall d, S d -> S (swap d).
> Axiom isoAx : forall d x, f (swap d) (f d x) = x.
> End Iso.
>
> Instead of two separate functions, two axioms, and two sets, we index 
> everything by a direction. This means we can write definitions of 
> composition of isomorphisms, juxtaposition, etc. and prove their 
> properties very compactly (saving 50% of the typing each time).
>
> Unfortunately, this definition doesn't typecheck: the term
>
> f (swap d) (f d x)
>
> has type S (swap (swap d)), not S d, which is the type of x. Of 
> course, swap (swap d) is provably equal to d for every d, but not 
> convertible.

You can restate the type of [isoAx] like this:

Axiom isoAx : forall d x, f (swap d) (f d x)
= match d return S d -> S (swap (swap d)) with
| R => fun x => x
| L => fun x => x
end x.

It's hard to say whether the details of your development will go more 
smoothly with this, with [JMeq], or with something else.