Questions tagged [cubical-agda]
The Cubical mode extends Agda with a variety of features from the CHM version of Cubical Type Theory. In particular, computational univalence and higher inductive types which hence gives computational meaning to Homotopy Type Theory and Univalent Foundations.
1
question with no upvoted or accepted answers
5
votes
1
answer
364
views
Paths Between Quotient Types in Cubical Agda
I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types.
In particular, my quotient type is the integers, quotiented by the absolute value function (<...
- 51