[Agda] Impredicativity

[Simon Boulier]

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

[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

Hi all,
I need an impredicative Prop universe.
Would it be lot of work to add an experimental "--impredicative-prop" flag?
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
https://lists.chalmers.se/mailman/listinfo/agda

[Simon Boulier]

Post by Jesper Cockx
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)?

Ho I see. For me it would be enough for experimentation. But people
should be aware that it does not turn Agda into a proof assistant for an
impredicative type theory.

Maybe we could name such a flag "--unsafe-impredicative-prop" ?

[Martin Escardo]

There is also an alternative hack, using rewriting rather than
--type-in-type:

http://www.cs.bham.ac.uk/~mhe/impredicativity-via-rewriting/

Martin

Post by Simon Boulier
Hi all,
I need an impredicative Prop universe.
Would it be lot of work to add an experimental "--impredicative-prop" flag?
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
https://lists.chalmers.se/mailman/listinfo/agda