4 problems

Let $G$ be a graph, let its associated cubical set be given, and let $|G|$ denote the geometric realization of that cubical set. Suppose that $G$ satisfies the cubical approximatio…

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…