[Agda] Impredicative prop?

[amp12]

> On 23 Feb 2023, at 12:12, Martin Escardo <m.escardo at bham.ac.uk> wrote:
> 
> I am listening. :-)
> Yes, I did that for Andy who at some point needed a small type of propositions. I am not sure it still works in the current version of Agda. (I think also Andreas and/or Jesper improved rewriting for the purposes of the second file, at that time.)
> But I think Andy wrote an improved version?

I was intending to, but didn't get very far (for the particular project I had at the time, I decided to try to to remain predicative).

Jesper Cock's example...

> Here is the example that shows Agda's current termination checker is not compatible with impredicativity: https://github.com/agda/agda/issues/3883#issuecomment-508416591

...shows a inconsistency problem with trying to force Agda's Prop (with its very useful ability to use pattern matching when defining functions on datatypes in Prop)  to be closed under impredicative definitions. Whereas Martin's stuff makes hidden use of --type-in-type (or alternatively, use of rewriting) to fudge _some_ type of h-props closed under impredicative ∀. I hope the latter is logically consistent (hope based on the belief that  the internal logic of toposes is consistent) but of course I don't know that for a fact, since some other cool feature of Agda might mix badly with Martin's tricks to produce inconsistency.

Andy