/quotient

quotient types in cubical Agda

Primary LanguageAgdaMIT LicenseMIT

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: