agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
Added initial work for the zero ring and zero abelian group, along with proofs of their uniqueness up to contractible type. Remaining work is refactoring for the rest of the...
Defines displayed precategories.
### Todo - [ ] Wait for #885 to merge. - [ ] Refactor postulates of universal properties to be phrased in terms of coherently invertible maps. - [ ]...
This is the replacement of #1005. Proves a series of basic properties of the flat modality. ## Summary ### General properties - [X] The universal property of flat discrete crisp...
Defines what it means for a type to be colocal at a map, and shows a few basic properties of these.
Defines the strict symmetrization of a binary relation, and proves some basic properties of these. Among these, - the construction has a unit `R -> S(R)` if `R` is reflexive...
## Summary - Introduce a general naming scheme for infix endooperations on propositions and the corresponding endooperations on types - Remove uses of `∀` - remove the redundant `implication-Prop` -...
- Renames `diagonal` to `diagonal-product`, and `diagonal-maps-of-types` to `diagonal-maps-cartesian-products-of-types` - Defines `diagonal-exponential A X : A -> X -> A` in a file `diagonal-maps-of-types`
In anticipation for #885. The proof of the universal property of coequalizers being preserved by equivalences of coforks got a bit unwieldy, but it should become more conceptual once morphisms...
In https://github.com/UniMath/agda-unimath/pull/1056#discussion_r1519953433 @EgbertRijke raised the question whether we should keep with the type theory convention of having "isomorphisms" be in general maps with structure, or if we should reappropriate it...