[Agda] Re: strict unit type

[Guillaume Brunerie]

2012/4/29 Vladimir Voevodsky <vladimir at ias.edu>:
>
> On Apr 29, 2012, at 11:38 AM, Guillaume Brunerie wrote:
>
>> Hello,
>>
>> 2012/4/29 Vladimir Voevodsky <vladimir at ias.edu>:
>>> Hello,
>>>
>>> let Pt be the unit type ("one point"). In Coq-like systems it is introduced through an eliminator and the associated iota-reduction rule. This is in practice sufficient for proving all its expected properties modulo propositional equality (or identity types) but does not create a terminal object in the category of contexts.
>>
>> I’m not sure if it is your question, but you do not need a unit type
>> to have a terminal object in the category of contexts, the empty
>> context is already a terminal object (there is exactly one context
>> morphism from any context to the empty context : the empty morphism).
>>
>>> I wonder if any one has considered type theories where Pt is introduced as having a distinguished object tt together with reduction rules of the following form (in the absence of dependent sums, otherwise one needs more):
>>>
>>> 1. any object of Pt other than tt reduces to tt,
>>
>> This is just the eta-expansion rule for Pt. For example Agda has it if
>> you implement Pt as a record.
>> You only need this (and beta/iota reduction) for (Pt) to be terminal
>> in the category of contexts (it will be isomorphic to the empty
>> context).
>
> I wonder how it works in Agda. This reduction for the unit type creates non-confluet situation when combined with iota/eta reduction for dependent sums. Additional reductions are needed to recover confluence. Are they implemented in Agda?

Do you have an example of a problematic situation?
By the way, I am far from a specialist in Agda, but perhaps that
normalization is implemented with something like normalization by
evaluation, which does not require confluence (I think).

>>> 2. Prod x : T , Pt reduces to Pt,
>>>
>>> 3. Prod x : Pt , T reduces to T.
>>
>> Sorry, I don’t know about these two, I have never seen those reduction
>> rules but you should wait for the answer of an actual type theorist.
>>
>> Guillaume
>>
>>> Thanks,
>>> Vladimir.
>