agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
The following probably doesn't type-check, but it will ge closer to what it should be (instead of an explicit pair of a function and a proof that it is an...
We should probably think about some conventions for consistent capitalization in entry names.
It would be very nice to have this sequence formalized in the library. Some intermediate goals are - [x] Define the homotopy pointed sets `πₙ` for `n ≥ 0` -...
Building on #834, a next goal is to define stable homotopy groups. Some intermediate steps include - [ ] Define colimits of sequential diagrams of pointed types - [ ]...
In anticipation of #834 I thought I'd clean up some stuff around homotopy groups and define them in a way that is well-connected with the existing formalization of groups, concrete...
Here is a constructive argument that monomorphisms in the category of groups are equalizers: https://ncatlab.org/toddtrimble/published/monomorphisms+in+the+category+of+groups It would be nice to add this to the library. A corollary is a constructive...
The definition of ethane should be refactored so that each of its components is defined separately, rather than all in one big definition.
That's an almost 3MB over the wire (17MB on disk) file that should only be downloaded when the users opens the search bar for the first time
It would be nice if `link-check` is ran before type-checking, or at least before the second type-checking stage, so that we don't have to wait 15 minutes to know if...