Just attended a talk by Jon Sterling on cubical type theory implementations: redtt and cooltt. Throughout the talk the speaker kept saying how all this stuff is already supported by Cubical Agda. I guess it was a good choice to choose Agda as language of preference for working with constructive type theories.

#cubical #typetheory #Agda #redtt #cooltt