[TYPES] strict unit type
Vladimir Voevodsky
vladimir at ias.edu
Sun Apr 29 10:10:47 EDT 2012
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 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,
2. Prod x : T , Pt reduces to Pt,
3. Prod x : Pt , T reduces to T.
Thanks,
Vladimir.
More information about the Types-list
mailing list