Feature request: Cubical Type Theory

[Hexirp]

I have not been able to find any attempts or proposals to incorporate CuTT into Coq. It's hard, but the idea should be here.

[Alizter]

I don't know what exactly you have in mind, but something along this line would essentially copy Agda: https://agda.readthedocs.io/en/v2.6.1/language/cubical.html

There some things are mentioned as added:

1. An interval type and path types
2. Generalized transport (transp)
3. Partial elements
4. Homogeneous composition (hcomp)
5. Glue types
6. Higher inductive types
7. Cubical identity types

Since the main experts on implementing the tricky details here are all working on Agda, I don't see this happening in Coq any time soon. Perhaps adding 1-4 is feasible, but I know for a fact that 5 is very difficult to get right. I don't think any of the core developers have the time or effort to make these changes to the kernel.

[ejgallego]

Related #6938

[Zimmi48]

Actually @herbelin is working on Cubical TT and I think he would like that it eventually makes it into Coq. But I'm not sure keeping an open issue in GitHub is going to be of any use in the meantime.

[herbelin]

There are quite a lot to say about the subject and I could actually share the current state of my reflection. The idea is not to follow Cubical Agda but:

• to have a generic notion of "interval" and associated (heterogeneous) equality-over whose rules are specified at user level; it would provide at will either a univalent equality or a bridge equality (see Cavallo-Harper)
• in the univalent case, to have A =_Type B characterized as A ≃ B (no partial elements, Altenkirch-Kaposi's symmetric definition of equivalence - or a variant of it); in the bridge case, to similarly have the characterization of A =_Type B as A -> B -> Type (added note: being exactly definitionally equivalent is a priori delicate, would require the interval to be affine, see Bernardy-Moulin, Cavallo-Harper)
• Kan composition (completion of open cubes) derives from the definition of equivalence
• Higher Inductive Types a priori as in CCHM
• if my intuitions are right, J and its reduction rule would be admissible for univalent equality over without needing identity types (suspectingly thanks to not having partial elements)

[Edited]

[patrick-nicodemus]

Has there been any further discussion of this feature request/wish?

Having a computational interpretation of function extensionality so that one can identify two extensionally-equal functions without assuming additional axioms would be useful. Setoid rewriting with automated typeclass resolution can take a long time when term sizes are large.