agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
The following remains to be defined in `species.unlabeled-structures-species`: - [ ] Equivalences of unlabeled structures of a species
The following is waiting to be defined in `ring-theory.algebras-rings`: - [ ] Unital algebras over a ring
The following claims are waiting to be formalized: - [ ] "In the case that `l1 ⊔ l2 = l1` we recover the identity modality" in `orthogonal-factorization-systems.raise-modalities` - [ ]...
The following claims are waiting to be formalized in `orthogonal-factorization-systems.orthogonal-factorization-systems`: - [ ] An orthogonal factorization system is uniquely determined by its right class - [ ] The right class...
This claim is waiting to be formalized in the library in `group-theory.symmetric-concrete-groups`: - [ ] Equivalent sets have isomorphic symmetric concrete groups
This is not yet formalized in the library: - [ ] Equivalences of concrete groups are isomorphisms of concrete groups
The following claims are waiting to be formalized in `foundation.surjective-maps`: - [ ] The type `Surjection-Into-Truncated-Type l2 (succ-𝕋 k) A` is `k`-truncated - [ ] The type of surjections `A...
The following claim is waiting to be formalized in `foundation.partial-elements`: - [ ] The type of partial elements is a directed complete poset
The following notions are not yet defined in the library: - [ ] proper ideals of rings - [ ] proper ideals of commutative rings - [ ] maximal ideals...
LaTeX is not rendered in the left-hand view, i.e. the numbered overview of namespaces and modules. This issue was detected a while back, and all instances were fixed in #639...