Hello. I came here to answer a question. I was referred here on Reddit. The question is:

Is there an attempt to incorporate Cubical Type Theory into Coq? In Agda, Cubical Agda already exists. I'm interested to see if a similar attempt will be made with Coq as well.

@nicolas tabareau student Loiuc Pujet has thought a bit about this. Loic does not seem to be on zulip.

Hi ! I indeed thought quite a bit about implementing some cubical models of univalence inside Coq. While the resulting computation rules do resemble the ones that are used in cubical type theories, I am not quite sure that approach is suitable for concrete use (computation is slowed down by a fair amount I think) and it is mostly about getting some canonicity/decidability/etc results.

Thank you. CuTT has the benefit of shortening the proof, but I still can't seem to get that benefit with Coq.

Even in Agda, significant questions seem to remain. Do they support indexed inductives properly? Not last I checked...

Has there been any progress toward incorporating cubical type theory in Coq?

I am aware that it is integrated into Agda but it is time intensive to learn a completely new proof assistant.

It would be nice to have function extensionality as a theorem that could be computationally justified.

@Loïc P and Nicolas (Tabareau) have been working on another kind of system, inspired by observational type theory, which gets you fun-ext, prop-ext, and so on, but without going cubical. You can go look the papers up on Loïc's webpage. Afaict, there is definitely interest in integrating this in the current sort of strict propositions, but we are not there yet…

I don't do much with fancy type theories, but isn't the whole point of cubical that you get univalence as a theorem instead of axiom, and thus all nice homotopy stuff including higher inductive types in computable way? From more practical standpoint, funext/propext might be viewed as a minor detail

Indeed, this is the idea, but I think fun-ext and prop-ext are still seen as valuable consequences of univalence.

Bumping this thread out of curiosity, has there been any advance towards integrating features of either cubical type theory or observational type theory into Coq in the past few months? Are there any plans for a plugin or a library that would allow an end user to reason in one of these theories?

I think there is definitely some interest to do this in Coq, but I am not aware of any plans by the team to do so. @Hugo Herbelin has probably thought to most about this.

I think @Loïc P is currently working on a very early prototype using rewrite rules

Last updated: Sep 30 2023 at 05:01 UTC