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.
$\begingroup$
$\endgroup$
7
-
$\begingroup$ Do their usages in cubical suffice? $\endgroup$– ice1000Jun 5, 2022 at 15:50
-
$\begingroup$ Have you seen github.com/agda/agda/blob/master/test/Succeed/SST.agda? $\endgroup$– ice1000Jun 5, 2022 at 15:52
-
$\begingroup$ Also github.com/agda/agda/issues/5944 $\endgroup$– ice1000Jun 5, 2022 at 15:52
-
$\begingroup$ @ice1000 Which usage? Is there a medium or large sized repo using them? $\endgroup$– Trebor ♦Jun 5, 2022 at 16:24
-
2$\begingroup$ In this experimantal library about 2LTT, SSet plays an essential role. See github.com/ElifUskuplu/2LTT-Agda $\endgroup$– phdstudentJun 5, 2022 at 17:39
|
Show 2 more comments
1 Answer
$\begingroup$
$\endgroup$
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 .
