Stream: Coq users

Topic: Cubical Type Theory


view this post on Zulip Hexirp Prixeh (Oct 21 2020 at 13:03):

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.

view this post on Zulip Bas Spitters (Oct 21 2020 at 14:26):

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

view this post on Zulip Loïc P (Oct 21 2020 at 16:10):

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.

view this post on Zulip Hexirp Prixeh (Oct 28 2020 at 02:55):

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

view this post on Zulip Paolo Giarrusso (Oct 28 2020 at 21:10):

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

view this post on Zulip Patrick Nicodemus (Nov 20 2022 at 23:43):

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.

view this post on Zulip Patrick Nicodemus (Nov 20 2022 at 23:43):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 21 2022 at 10:51):

@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…

view this post on Zulip Karl Palmskog (Nov 21 2022 at 11:01):

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

view this post on Zulip Meven Lennon-Bertrand (Nov 21 2022 at 11:07):

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


Last updated: Feb 06 2023 at 11:03 UTC