[Agda] type:type locally?

[Jesper Cockx]

Hi Thorsten,

Currently we do not have such an option. I think it would make sense to add
a pragma for disabling the universe check for a data/record type without
disabling universe checking entirely. This would actually be easier to
implement than NO_POSITIVITY_CHECK, as the universe check is done for a
single data/record type rather than the whole mutual block. If there are no
takers I could take a look at it (probably only after the POPL deadline
though).

-- Jesper

On Tue, Jun 26, 2018 at 11:52 AM, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> I can switch off positivity checking locally by saying
>
>
>
> {-# NO_POSITIVITY_CHECK #-}
>
>
>
> But I can’t say
>
>
>
> {-# TYPE-IN-TYPE #-}
>
> data Prop : Set
>
> T : Prop → Set
>
>
>
> data Prop where
>
>   pi : (A : Set)(b : A → Prop) → Prop
>
>
>
> T (pi A b) = (x : A) → T (b x)
>
>
>
> Or is there a difference syntax? This would be useful for a simple-minded
> encoding of the calculus of constructions.
>
>
>
> Thorsten
>
>
>
> P.S. I know I can avoid this by adding another level:
>
>
>
> data Prop : Set
>
> T : Prop → Set
>
> data U : Set
>
> El : U → Set
>
>
>
> {-# NO_POSITIVITY_CHECK #-}
>
> data U where
>
>   prop : U
>
>   pi : (a : U)(b : El a → U) → U
>
>   emb : Prop → U
>
>
>
> El prop = Prop
>
> El (pi a b) = (x : El a) → El (b x)
>
> El (emb p) = T p
>
>
>
> data Prop where
>
>   pi : (a : U)(b : El a → Prop) → Prop
>
>
>
> T (pi a b) = (x : El a) → T (b x)
>
>
> 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.
>
>
>
>
>
> _______________________________________________
> 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/20180627/9e28edca/attachment.html>