The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Hi Freek,

> It is "just" a notion of binding a variable, to be able to do HOAS.

I think that is slightly misleading.  For adequacy of HOAS
representation you need termination of the meta language, which seems
to require types.

You also need to identify meta language terms up to
beta-eta-conversion.  What is the deal with Automath and eta?

Best,
Randy
--


On Mon, Nov 16, 2015 at 11:50 AM, Freek Wiedijk 
<freek AT cs.ru.nl>
 wrote:
> Hi Thorsten,
>
>>What is nice about this conceptual confusion?
>
> That you can get away with it?  That you can simplify your
> syntax and typing rules that way and still have a viable
> logical framework?
>
> The "[x:A]" binder of automath should not be thought of
> as creating a function or function type.  It is "just"
> a notion of binding a variable, to be able to do HOAS.
>
> I'm not saying that the Automath approach to type theory
> is more powerful than the "modern" one (it's basically an
> alternative to LF), but it _is_ simpler and more regular
> and it _does_ work.
>
> Freek
>