agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
This PR formalizes the concept of constancy of a map of types.
## Summary - [X] Add dotted underlines under links that are adjacent making it possible to tell them apart, e.g.:   The styling does not apply to code, or...
Defines - Subfinite types - Subfinitely indexed types - Dedekind finite types - dual Dedekind finite types - Noninjective maps (maps for which there exists a repetition of values) Proves...
This aims at centralizing conversations regarding metric spaces and real / functional analysis. # Concepts - [x] distance functions - #1394 - #1400 - [x] rework limits - #1378 -...
This draft PR contains some very preliminary joint work with Emily, Tim, and Jonathan
Real addition will give us our first large group, but we have to define what that looks like. The biggest issue I see is the inverse laws: if `x :...
Some upcoming PRs (#1378, #1402, #1398, #1417, etc.) introduce new metric spaces so we should update `tables/metric-spaces.md` accordingly. However, since some of these PRs are already quite ready, I think...
Replace the current notation for similarity/indiscernibility `x ≈ y` with `x ≍ y` as proposed in #1418. Resolves #1418.
The library has adopted the symbol `≈` for "similarity" of elements, for instance, for elements in preorders. However, it seems to me that the symbol `≈` is used more commonly...