agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
A lot of results in logic and foundations. ### Summary - Types with decidable Σ-, Π-, and ∀-types - Logical properties of maps - Irrefutably surjective maps - Propositionally double...
It sounds like we don't necessarily want this, but I built this as a draft.
Here's a preview of what the library might look like with depostulated axioms. Depends on #1373 #1379
~~There are still two holes left to fill, but they seem to be conceptually easy enough that I'm confident publishing this *draft* PR now — in particular they don't have...
The first steps of real analysis -- certainly the first steps in the constructive real analysis developments I've seen -- involve getting basic power series up and running. What are...
I was discussing best practices with Egbert yesterday (in person!) and in particular what lessons from my background would be applicable and valuable to agda-unimath. (For context, in my professional...
Streams
Early work on streams, the coinductive version of lists. As lists are currently used for finite-dimensional linear algebra, streams seem the natural candidate for infinite-dimensional objects such as polynomial algebras...
Reasoning syntax doesn't produce the expected result for relations which aren't strictly left unital
Equational reasoning works as advertised: `equational-reasoning x ＝ y by p` computes to `p`, but it relies on `refl` being a strict left unit with respect to path composition, since...
Anodyne maps
Defines anodyne maps and weakly anodyne maps and establishes some basic closure properties.
Here's that PR I talked about a while back.