5
$\begingroup$

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.

$\endgroup$
7

1 Answer 1

2
$\begingroup$

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 .

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.