quotient

This is a library for working with quotient types in cubical Agda, attempting to abstract away some of the cubical boilerplate involved in defining functions and proofs over quotient types. See numbers for examples.

Dependencies:

• cubical
• agda-stdlib