[Agda] A plea for Set:Set

[Thorsten Altenkirch]

Hi,

would it be difficult to make it possible to switch off the checking  
of universe levels. Especially until Agda adopts some way of universe  
polymorphism?

I just tried to define a family using [_,_]

   Plus : Cont -> Cont -> Cont
   Plus (S ◁ P) (T ◁ Q) = (S ⊎ T) ◁ [ P , Q ]

but I get

/Users/txa/Talks/fun 08/ucont.agda:31,38-39
Set1 != Set
when checking that the expression P has type
(_87 S P T Q -> _89 S P T Q)

Ok, here is a way out - I define a new operator

   [_,,_] :  {a b : Set}{c : Set1}
       -> (a -> c) -> (b -> c) -> (a ⊎ b -> c)
   [ f ,, g ] (inj₁ x) = f x
   [ f ,, g ] (inj₂ y) = g y

   Plus : Cont -> Cont -> Cont
   Plus (S ◁ P) (T ◁ Q) = (S ⊎ T) ◁ [ P ,, Q ]

Obviously this will lead to an explosion of definitions and hamper  
library developments. Hence, I'd suggest that there is an "Epigram- 
switch" to allows Set:Set.

Cheers,
Thrsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.