[Agda] Is it possible to switch off universes checking?

[Martin Escardo]

On 28/12/15 19:09, Nils Anders Danielsson wrote:
> I don't know why universe polymorphism and --type-in-type cannot be used
> together.

I would be lovely if they could be used together.

Using --type-in-type, I managed to simulate hprop-resizing a la
Voevodsky here: http://www.cs.bham.ac.uk/~mhe/impredicativity/

However, there is a limitation, as discussed in the above link, in
connection with universe levels.

There is also the other thread, after this one, "Why no impredicattive
prop?", to which we have:

On 29/12/15 22:11, Thorsten Altenkirch wrote:
> Actually why do you need an impredicative universe?
>
> From a purely pragmatic point it is a bit strange if one universe
> behaves different from the other one. But having two impredicative
> universes is already unsound.
>
> More on the philosphical side: impredicativity is basically a classical
> idea which arises from the identification of Prop and Bool. I don’t know
> an intuitionistic justification of impredicativity.


Thorsten has a point, because there is a predicative version of the
above: http://www.cs.bham.ac.uk/~mhe/predicativity/

However, the main point is not this: Prop in Coq doesn't satisfy the
axiom of description (allowing us to get witnesses from unique existence).

The above predicative version in Agda does give you that. However, it is
not clear that the impredicative version "computes" (as opposed to
"diverges"). This is an open problem, as Thierry Coquand explained to me
a while ago.

Martin