agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
This will necessarily have to be different for large strict posets, too, which I'm not even sure exist yet?
With #1373 I began work towards removing axioms as postulates in the library, this has multiple benefits as well as drawbacks. The current proposal does not make any changes to...
As demonstrated by Evan Cavallo, strong preunivalence follows from preunivalence + function extensionality. By an analogous proof, preunivalent categories are strongly preunivalent.
This PR is preparation for #1379. The `BUILTIN` pragma cannot be invoked inside of a parametrized module, which in practice means that we cannot have a dependency on an axiom...
We can discuss how much of https://github.com/UniMath/agda-unimath/pull/1388/ we want in large posets. I guess one of the main example would be sequences of real numbers so I'll try to keep...
Attempting to keep things general, I think we go: 1. Continuity of a function between metric spaces at a point (the function being defined in a neighborhood of the point)...
Still a draft with a long way to go. This is now my procrastination fuel. Typos/potential oversights found during transcription: - Page 114, Exercise 9.7 (e), typo in condition (ii)...
Given a concept macro invocation like `{{#concept "standard inequality relation" Disambiguation="on booleans" Agda=}}` the preprocessor should report an error that the `Agda` field is present but empty.
Work-in-progress, not ready for review, but at least putting this here to show how the parts fit together. Will complete #1353 .