Empty hcomps and empty systems are often mentioned in the context of cubical type theory, in particular related to the efficiency of evaluation, for example here and here. What exactly are they, and why are they an issue? I think it is good to collect some answers and references under this question, and I'll try to answer what I know in a few days.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.