What kind of ‘category’ is Cubical type theory the internal language of?

Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher inductive types you get the internal language of locally cartesian closed $(\infty , 1)$-categories, a.k.a HoTT without Univalence. And as far as I know, it is suspected that plain HoTT is the internal language of whatever an $(\infty , 1)$-topos is.

Cubical type theory doesn’t quite fit into this sequence of type theories but it is surprisingly good at modelling HoTT. It is a strange kind of type theory in that it uses Heyting algebras to reason about cubes but non the less it begs the question: What kind of category does it generate?

I suspect the answer to this question isn’t known, however I would be more than happy to see peoples suspicions.

What kind of ‘category’ is Cubical type theory the internal language of?

Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher inductive types you get the internal language of locally cartesian closed $(\infty , 1)$-categories, a.k.a HoTT without Univalence. And as far as I know, it is suspected that plain HoTT is the internal language of whatever an $(\infty , 1)$-topos is.

Cubical type theory doesn’t quite fit into this sequence of type theories but it is surprisingly good at modelling HoTT. It is a strange kind of type theory in that it uses De Morgan algebras to reason about cubes but non the less it begs the question: What kind of category does it generate?

I suspect the answer to this question isn’t known, however I would be more than happy to see peoples suspicions.

What kind of ‘category’ is Cubical type theory the internal language of?

Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher inductive types you get the internal language of locally cartesian closed $(\infty , 1)$-categories, a.k.a HoTT eithout Univalence. And as far as I know, it is suspected that plain HoTT is the internal language of whatever an $(\infty , 1)$-topos is.

Cubical type theory doesn’t quite fit into this sequence of type theories but it is suprisingoy good at modelling HoTT. It is a strange kind of type theory in that it uses Heyting algebras to reason about cubes but non the less it begs the question: What kind of category does it generate?

I suspect the answer to this question isn’t known, however I would be more than happy to see peoples suspicions.

What kind of ‘category’ is Cubical type theory the internal language of?

Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher inductive types you get the internal language of locally cartesian closed $(\infty , 1)$-categories, a.k.a HoTT without Univalence. And as far as I know, it is suspected that plain HoTT is the internal language of whatever an $(\infty , 1)$-topos is.

Cubical type theory doesn’t quite fit into this sequence of type theories but it is surprisingly good at modelling HoTT. It is a strange kind of type theory in that it uses Heyting algebras to reason about cubes but non the less it begs the question: What kind of category does it generate?

I suspect the answer to this question isn’t known, however I would be more than happy to see peoples suspicions.