[Agda] Impredicative prop?

[Thorsten Altenkirch]

One way to add an impredicative universe on Set is

{-# NO_UNIVERSE_CHECK #-}
record Pi {ℓ} (A : Set ℓ)(B : A → Set)  : Set where
  constructor lam
  field
    _$_ : (a : A) → B a
  infixl 10 _$_

open Pi

syntax Pi A (λ x → P)  = Π[ x ∈ A ] P
syntax lam (λ x → p) = λ[ x ] p

but the syntax is a bit ugly. Also I am not sure whether this works for Prop.

From: Agda <agda-bounces at lists.chalmers.se> on behalf of Neel Krishnaswami <nk480 at cl.cam.ac.uk>
Date: Thursday, 23 February 2023 at 09:47
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] Impredicative prop?
Hi,

I'd like to teach a course next year which (among other things) proves a
simple termination result for System F in Agda.

Obviously, I can't do this without an impredicative Prop sort, and so I
was wondering what changes would need to be made to Agda to support it.

As far as I can tell, there are two things which would need to be done:

1. Turn off universe levels for Prop.
2. Enforce the strict positivity restriction on Prop-valued datatype
declarations.

Is there anything I'm missing?

Thanks,
Neel

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20230223/656c3032/attachment.html>