The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello,

On 3 juin 2013, at 23:10, Greg Morrisett 
<greg AT eecs.harvard.edu>
 wrote:

> The usual way around this is to define syntax for types e.g.,:
> 
> Inductive tipe : Set := 
>  | Nat : tipe
>  | Pair : tipe -> tipe -> tipe
>  | Arrow : tipe -> tipe -> tipe.
> […]
> This gets trickier when you have complicated types (e.g., 
> polymorphism or dependent types).  

I remember trying once for polymorphic types and ran quickly into troubles.
Without functional equality axiom (I think), for polymorphic types, I could 
not prove things like:
f : [[ Arrow t1 t2]] 
x : [[t1]] 
----------------------
(f x) : [[apply  (Arrow t1 t2) t1]]

Is there a known encoding that is axiom-free ?
What subset of Coq can be reflected this way ? Are there known limits ?

--
Frédéric

PS: We ran into this problem when considering a reflexive version of 
congruence.
We sidestepped the difficulty by ruling out  polymorphism and considering
e.g. (cons nat) and (cons Z) as different constructors.