[Agda] Re: strict unit type

[Vladimir Voevodsky]

On May 1, 2012, at 3:51 AM, Andreas Abel wrote:

> On 30.04.12 3:36 PM, Vladimir Voevodsky wrote:
>>>> PS There is another non-confluent situation with a ->   tt for a
>>>> : Pt which does not require dependent sums namely \lambda x:T, f
>>>> x where f : T ->   Pt reduces both to f and to \lambda x:T tt .
>>>> Both non-confluences can be taken care of by additional
>>>> reductions in particular the reduction \prod x:T, Pt ->   Pt for
>>>> the example with \lambda.
>>> 
>>> Such a reduction is unhealthy except in the situation where \prod
>>> is a "for all" that does not leave marks on the term level.
>> 
>> Well, that was my first thought as well but I am not so sure now. It
>> does make it necessary to do some type checking before beta-reduction
>> but anyhow the reduction such as a ->  tt for objects of the unit
>> type makes reduction context dependent. I have not checked all the
>> details yet but it is possible that one can preserve confluence and
>> normal form and still have reductions which change the
>> sum/prod-structure of type expressions.
> 
> I agree that this can likely be modeled, i.e., terms and types can be interpreted in a way that these reductions become identities. Partially, this is done in Werner et al.'s proof irrelevant model of the CIC.
> 
> However, I am not so convinced that reduction is the right method in this case.  For instance, subject reduction fails unless you work on equivalence classes of types.  A more "semantic" approach seems more fitting, from my experience.  Also, from the implementor's perspective such reductions complicate the picture.  For instance, the problem
> 
>  tt : \prod x:T. Y(x)    with Y a meta-variable
> 
> cannot be decided at the spot, but has to wait for the solution of Y. Also, then a term has many types, which makes type inference more complicated.


In the system which I am trying to write up there is a typing function on terms i.e. for any o-term X (object like term) and any function \Gamma assigning t-terms (type-like terms) to the free variables in  X there is a simply computed t-term \tau_{\Gamma}(X) which, if everything happened to be derivable gives a canonical representative to the type of X. 

The fact that there can be many t-terms which are definitionally equal to \tau_{\Gamma}(X) seems unavoidable in any system with universes.

Vladimir.