[Agda] Should we create an issue to track the status of Cubical?

[Apostolis Xekoukoulotakis]

I have recently learned to program with CTT. I was trying to understand the
consequences
it will have in programming. For now, I will just go back to my usual
programming
but I would like to be notified when quotient types or Higher Inductive
types are ready
so as to start using them as soon as possible.

For this reason, I propose that we create an issue to track the development
of these features.

[Andrea Vezzosi]

Here it is, and thanks for checking cubical out!

https://github.com/agda/agda/issues/2761

Cheers,
Andrea

On Mon, Sep 18, 2017 at 7:49 AM, Apostolis Xekoukoulotakis

Post by Apostolis Xekoukoulotakis
I have recently learned to program with CTT. I was trying to understand the
consequences
it will have in programming. For now, I will just go back to my usual
programming
but I would like to be notified when quotient types or Higher Inductive
types are ready
so as to start using them as soon as possible.
For this reason, I propose that we create an issue to track the development
of these features.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda