replace WithK with a file in Axiom containing statement and consequences of UIP/K

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

454 stars 139 forks source link

replace WithK with a file in Axiom containing statement and consequences of UIP/K #896

Closed ecavallo closed 2 years ago

ecavallo commented 2 years ago

Resolves #830. This way we don't have a file that relies on an extra flag and isn't usable in the rest of the library (and needs its own special case in the Makefile).

mortberg commented 2 years ago

Nice!