[Agda] Impredicativity

[Jesper Cockx]

Hi Simon,

It would be easy to add such a flag, but unfortunately it would also be
unsound since Agda's termination checker currently assumes predicativity:

data ⊥ : Prop where
>
> data Weird : Prop where
>   weird : (∀ {A : Prop} → A → A) → Weird
>
> yes : Weird
> yes = weird (λ x → x)
>
> no : Weird → ⊥
> no (weird f) = no (f (weird f))
>
> boom : ⊥
> boom = no yes
>

Changing the termination checker to remove this assumption would take some
more work. Would you be happy with a version of --impredicative-prop which
is essentially a limited version of --type-in-type (and is thus unsound)?

-- Jesper

On Wed, Oct 10, 2018 at 10:20 AM Simon Boulier <simon.boulier at ens-rennes.fr>
wrote:

> Hi all,
>
> I need an impredicative Prop universe.
>
> Would it be lot of work to add an experimental "--impredicative-prop" flag?
>
> I am also aware of this hack of Martin Escardo:
> http://www.cs.bham.ac.uk/~mhe/impredicativity/
> But I am not sure to which extent I can adapt it to my needs...
>
> Cheers,
>
>
> Simon
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181010/1d3f0973/attachment.html>