Felix Cherubini

> What do you have in mind more concretely? An S with few files would probably just be the Base and Properties file, no? But if there is Base and...

Nice! Please go on ;-) I think the old modalities code should be replaced as soon as this one covers the same functionality (and no problems with the Typeω come...

Did you see the finite multisets: https://github.com/agda/cubical/blob/master/Cubical/HITs/FiniteMultiset/Base.agda ? ~~Unordered pairs are a special case and I think it would be better to define them as such, if you really have...

> Yes, I know the relation. I will try to put in the properties. For example, in Agda Stdlib (https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Recursive.agda), they defined Vec using Product. So maybe it is possible...

As I just learned in the hallway, there is also an untruncated unordered pair notion, defined as maps from a set merely equivalent to Fin 2 to A. I guess...

> I am trying to do your implementation, but I am in trouble. What am I doing wrong? What you are trying to prove is true. The first part of...

```∥_∥₁``` is propositional truncation.

You can, of course, also postpone the proof and wrap up the current PR...

Sorry for the long wait and thanks for the updates. I am a bit puzzled about the recursive FMSets - maybe it is better to save those for a PR...

Hm, I see. I never thought of the spectrification as indexed, because I only thought about spectrifying suspension spectra... So far, there is nothing specific to the Integer - I...