Is there any presentable work that makes essential use of
SSet in Agda? I kind of get the theory, but I'm not sure about the practical value of this. The documentation is currently not very helpful.
Since SSet provides another universe for not-necessarily fibrant types, it is useful when one is working on 2LTT. You can see one of the experimental library about 2LTT here : https://github.com/ElifUskuplu/2LTT-Agda .