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.
-
Notifications
You must be signed in to change notification settings - Fork 0
quotient types in cubical Agda
License
kcsmnt0/quotient
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
quotient types in cubical Agda
Topics
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published