3 problems

Let $\mathsf{cSet}^+$ denote the category of marked cubical sets and let $\mathsf{PreComp}$ denote the category of marked simplicial sets (pre-complicial sets). Let…

Pathhood-irrelevance conjecture. The interpretation of any type that can be constructed in ParamDTT has irrelevant pathhood. This property is introduced to ensure injectivity of th…

Substitution-interpretation conjecture. The interpretation of the substitution rule is given by the substitution above. The source assumes this claim without proof as part of the s…