This was before Cubical Agda was invented

Oops, I meant to say that this was around the time Andrea Vezzosi was implementing Cubical Agda (which Guillaume mentions in the slides).

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/78088eab-9b8e-4dc3-a2cf-91ae4aa3b5cbn%40googlegroups.com.