The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

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.

What to do?  We've seen the discussion of John Major equality in  
CoqArt... is this our only hope, or is there a lighter way?

Thanks!

    - Benjamin Pierce and Martin Hofmann