[Agda] Re: [TYPES] strict unit type

[Vladimir Voevodsky]

On May 10, 2012, at 2:08 PM, Robert Harper wrote:

> hello everyone,
> 
> there is no problem to decide equivalence in the presence of extensionality axioms such as eta and xi, nor for unicity conditions such as the one stating that all maps to 1 are equal.  my work with chris stone on singleton types shows how to handle sigma's and pi's and unit (actually much more than just unit, but including it as a special case), which specializes to arrow and cross as well.  generally the method works well for negative types, but cannot be made to scale to positive types, which require some form of induction.  so, for example, there is no problem with the "iota" (i.e., beta) rules for inductive types, since these are purely computational, and we can handle extensionality conditions for negative types, but one cannot expect something as strong as the coproduct universal condition for sums, merely the beta-like rule of reduction.
> 
> the algorithm that stone and i give has a two-phase flavor.  first, a type-directed phase that reduces things to atomic types by elimination forms, then a structural phase that compares the weak head normal forms of the results of the type-directed phase.  (weak head normalization takes care of all beta-like rules.)  the structural phase calls back to the typed phase.  the correctness argument is fascinating (imo) because of the complications introduced by the asymmetries hinted at in thorsten's post having to do with the interaction between sigma's and pi's.
> 
> as an aside, would someone please explain to me as concisely as possible what is the problem with universes in coq?  this came up in discussion here yesterday, and i drew the impression, perhaps mistaken, that the problem is that coq does not implement the solution that pollack and i worked out in 1988.  if i am right, the problem is already solved, but was apparently not used in the coq implementation for some reason.  i can explain separately what pollack and i did and how it works.  it sounded as though it would address many of the problems that have arisen, but i'm not completely certain until i learn more about them.
> 
> best,
> bob
> 

Hi Bob,

I would sum things with universes as follows:

1. there is no universe polymorphism

2. because of strict sub-typing for universes eta-reduction of \lambda-terms is problematic 


From the HOTT point of view another problem is that it is unclear how to proceed with the modifications which are needed for adding the resizing rules. 


Vladimir.

PS Could you send a link to the your paper with Stone which you are referring to?