Return to Answer

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categories with natural number objects.

Note that even at this level, one only have a $2$-equivalence of (strict) $2$-categories, this is not an equivalence of the $1$-categories.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

For example, when one says that Martin löf type theory with intentional identity type is the internal language of cartesian closed $(\infty,1)$-categories with natural number objects (not proved yet), it is a statement that compare a "homotopy category", (or a Dwyer-Kan localization) of contextual category with the structure corresponding to Martin löf type theory to some homotopy category (or $\infty$-category) of cartesian closed $(\infty,1)$-category.

In general those homotopy category (or $\infty$-category) are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additional structures corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' or $\infty$-category that we want to compare to some other homotopy/$\infty$-category of $\infty$-categories with certain structures/properties, or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubical fibrations category satisfying some additional axiom in the spirit of model toposes.

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categories with natural number objects.

Note that even at this level, one only have a $2$-equivalence of (strict) $2$-categories, this is not an equivalence of the $1$-categories.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

For example, when one says that Martin löf type theory with intentional identity type is the internal language of cartesian closed $(\infty,1)$-categories with natural number objects (not proved yet), it is a statement that compare a "homotopy category", (or a Dwyer-Kan localization) of contextual categories with the structure corresponding to Martin löf type theory, to some homotopy category (or $\infty$-category) of cartesian closed $(\infty,1)$-category.

In general those homotopy category (or $\infty$-category) are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additional structures corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' or $\infty$-category that we want to compare to some other homotopy/$\infty$-category of $\infty$-categories with certain structures/properties, or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubical fibrations category satisfying some additional axiom in the spirit of model toposes.

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categories with natural number objects.

Note that even at this level, one only have a $2$-equivalence of (strict) $2$-categories, this is not an equivalence of the $1$-categories.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

Like, when one says that Martin löf type theory with intentional identity type is the internal language of cartesian closed $(\infty,1)$-categories with natural number objects (not proved yet), it is a statement that compare a "homotopy category" of contextual category with the structure corresponding to Martin löf type theory to some homotopy category of cartesian closed $(\infty,1)$-category.

In general those homotopy category are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additinal structure corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' that we want to compare to some other homotopy category of $\infty$-categories with certain structures/properties. or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubically enriched fibrations category satisfying some additional axiom in the spirit of model toposes.

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categories with natural number objects.

Note that even at this level, one only have a $2$-equivalence of (strict) $2$-categories, this is not an equivalence of the $1$-categories.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

For example, when one says that Martin löf type theory with intentional identity type is the internal language of cartesian closed $(\infty,1)$-categories with natural number objects (not proved yet), it is a statement that compare a "homotopy category", (or a Dwyer-Kan localization) of contextual category with the structure corresponding to Martin löf type theory to some homotopy category (or $\infty$-category) of cartesian closed $(\infty,1)$-category.

In general those homotopy category (or $\infty$-category) are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additional structures corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' or $\infty$-category that we want to compare to some other homotopy/$\infty$-category of $\infty$-categories with certain structures/properties, or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubical fibrations category satisfying some additional axiom in the spirit of model toposes.

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categoris with natural number objects.

Note that even at this level, one only have an equivalence of strict $2$-category, this is not an equivalence of the underlying $1$-category.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

Like, when one says that Martin löf type theory with intentional identity rules is the internal language of cartesian closed $(\infty,1)$-category with natural number objects (not proved yet) is a statement that compare a "homotopy category" of contextual category with the structure corresponding to Martin löf type theory to some homotopy category of cartesian closed $(\infty,1)$-category.

In general those homotopy category are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additinal structure corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' that we want to compare to some other homotopy category of $\infty$-categories with certain structures/properties. or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubically enriched fibrations category satisfying some additional axiom in the spirit of model toposes.

I would say that the question is not even well defined.

Saying that Martin löf type theory with extensional identity types is the internal language of cartesian closed categories with natural number objects is a rather clear formal statement: you are saying that some $2$-category of contextual categories with additional structure corresponding to Martin löf type theory is equivalent to a $2$-category of cartesian closed categories with natural number objects.

Note that even at this level, one only have a $2$-equivalence of (strict) $2$-categories, this is not an equivalence of the $1$-categories.

When you move to $\infty$-categorical statement there is a new difficulty: you are comparing $\infty$-categories:

Like, when one says that Martin löf type theory with intentional identity type is the internal language of cartesian closed $(\infty,1)$-categories with natural number objects (not proved yet), it is a statement that compare a "homotopy category" of contextual category with the structure corresponding to Martin löf type theory to some homotopy category of cartesian closed $(\infty,1)$-category.

In general those homotopy category are defined as ordinary $1$-category, localized at some class of weak equivalences.

(I recomend this paper of Lumsdain and Kapulkin for a very nice and precise formulation of this)

To come back to your question, if one start with cubical type theory, it is rather clear what is the underlying $1$-category (although probably a pain to state or to prove): it is some kind of contextual category with additinal structure corresponding to the axioms of cubical type theory, but it is very unclear what should be the weak equivalences between them, and hence what should be the corresponding 'homotopy category' that we want to compare to some other homotopy category of $\infty$-categories with certain structures/properties. or even if you want to see it as $2$-category and so one.

Depending on the choice of weak equivalences, one could get very different answer to that question (so you might get precise answer to your question after all, just probably not a unique one)

For example, one could imagine a notion of weak equivalences that completely ignore the cubical aspect, and which would provide an equivalence with some notion of $(\infty,1)$-topos.

Or one could take a more restricted notion of weak equivalences that see the cubical aspect and say that cubical type theory is the internal language of some kind of cubically enriched fibrations category satisfying some additional axiom in the spirit of model toposes.