[Agda] [ANNOUNCE] Agda 2.6.2

[Andrew Pitts]

> On 19 Jun 2021, at 07:38, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> 
> The Agda Team is very pleased to announce the release of Agda 2.6.2.
> 
> # Highlights
…

I took a look at Agda.Primitive and saw

{-# BUILTIN TYPE Set #-}
{-# BUILTIN PROP Prop #-}
{-# BUILTIN SETOMEGA Setω #-}

which I guess has to do with

> * The Primitive Sorts (https://agda.readthedocs.io/en/v2.6.2/language/built-ins.html#sorts) of Agda (`Set` and `Prop`) are no longer keywords and can be renamed when importing `Agda.Primitive`.

but then there is

{-# BUILTIN STRICTSET      SSet  #-}
{-# BUILTIN STRICTSETOMEGA SSetω #-}

SSet and SSetω are undocumented (although the former appears in <https://agda.readthedocs.io/en/latest/language/cubical.html>)

What are they for?

Just curious,

Andy