The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

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).

> 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.