UniMath/agda-unimath issues and pull requests

#913 - Clean up characerization of homotopies in suspenison file

Pull Request - State: closed - Opened by morphismz about 1 year ago

#912 - Isomorphisms induce equivalences by pre- and postcomposition

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: category-theory

#911 - Typeset `nlab` as `$n$Lab`

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: documentation, fix

#910 - Additions during work on material set theory in HoTT

Pull Request - State: closed - Opened by elisabethstenholm about 1 year ago - 14 comments
Labels: category-theory, foundation, order-theory

#909 - Composition and left factor for epis/acyclic maps

Pull Request - State: closed - Opened by tomdjong about 1 year ago
Labels: foundation, synthetic-homotopy-theory

#908 - Acyclic types are closed under retracts

Pull Request - State: closed - Opened by tomdjong about 1 year ago
Labels: synthetic-homotopy-theory

#907 - A map is a dependent epi iff it is an epi iff it is acyclic

Pull Request - State: closed - Opened by tomdjong about 1 year ago

#906 - Fix Elisabeth's GitHub link

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 1 comment
Labels: documentation, fix

#905 - A type is acyclic if and only if its terminal map is an acyclic map

Pull Request - State: closed - Opened by tomdjong about 1 year ago

#904 - Name change for Elisabeth

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 1 comment

#903 - Refactoring of retractions, sections, and equivalences, and adding the 6-for-2 property of equivalences

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 12 comments
Labels: foundation, refactoring

#902 - Refactor extensionality of `Torsor-Abstract-Group`

Issue - State: open - Opened by fredrik-bakke about 1 year ago
Labels: group-theory

#901 - Acyclic types are closed under equivalences

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 7 comments
Labels: synthetic-homotopy-theory

#900 - Retracts of maps

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 3 comments
Labels: foundation, orthogonal-factorization-systems

#899 - Equality in iterated Sigma types

Pull Request - State: closed - Opened by maybemabeline about 1 year ago - 3 comments
Labels: foundation

#898 - Functoriality of suspensions

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 4 comments
Labels: synthetic-homotopy-theory

#897 - Small formatting fixes concrete groups

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: group-theory, refactoring

#896 - Indiscrete precategories

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 6 comments
Labels: category-theory

#895 - Adding myself as a maintainer

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 2 comments

#894 - The acyclic maps are exactly the epimorphisms

Pull Request - State: closed - Opened by tomdjong about 1 year ago
Labels: synthetic-homotopy-theory

#893 - The acyclic maps are precisely the epimorphisms

Pull Request - State: closed - Opened by tomdjong about 1 year ago

#892 - Codiagonal is fiberwise suspension

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 2 comments
Labels: synthetic-homotopy-theory

#891 - Implicit function extensionality

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 4 comments
Labels: foundation

#890 - Global function classes

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 11 comments
Labels: orthogonal-factorization-systems

#889 - Equivalence between spans and relations

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 3 comments
Labels: foundation

#888 - `apply-universal-property` vs. `recursion`

Issue - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: refactoring

#887 - Characterizing the fibers of cogap as a pushout of fibers

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 3 comments
Labels: synthetic-homotopy-theory

#886 - Fun with functors

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 10 comments
Labels: category-theory, foundation, cat-sitting

#885 - Rebase infrastructure for pushouts to span diagrams

Pull Request - State: open - Opened by EgbertRijke about 1 year ago - 21 comments
Labels: foundation, synthetic-homotopy-theory, refactoring

#884 - Add a mdbook `#concept` macro

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 17 comments
Labels: enhancement, website, tooling, mathswitch

#883 - Extending pushouts by equivalences

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 2 comments
Labels: synthetic-homotopy-theory

#882 - Transparent favicons, copy them properly

Pull Request - State: closed - Opened by VojtechStep about 1 year ago

#881 - Add favicons

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 9 comments
Labels: enhancement, website

#880 - Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 4 comments
Labels: category-theory, foundation

#879 - Refactor graphs with updates from Beyond finite sets

Pull Request - State: open - Opened by EgbertRijke about 1 year ago - 2 comments
Labels: graph-theory, refactoring

#878 - Refactor funext

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 3 comments
Labels: foundation, refactoring

#877 - Abelianization

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 13 comments
Labels: group-theory, foundation, order-theory, 🏆 milestone 🏆

#876 - Peano arithmetic

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 3 comments
Labels: elementary-number-theory, refactoring

#875 - Implement `is-torsorial` throughout the library

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 5 comments
Labels: refactoring

#874 - Preunivalence holds in univalent foundations

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: foundation

#873 - Improve computational behaviour of `iso-eq`

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: category-theory, refactoring

#872 - Add a favicon

Issue - State: closed - Opened by VojtechStep about 1 year ago - 7 comments
Labels: enhancement, website

#871 - Rename `is-contr-total` to `is-torsorial`

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 6 comments
Labels: refactoring

#870 - Formatting of postulates

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 3 comments
Labels: formatting

#869 - Flattening lemma for sequential colimits

Issue - State: closed - Opened by VojtechStep about 1 year ago
Labels: synthetic-homotopy-theory

#868 - Standard sequential colimit and its functoriality

Issue - State: closed - Opened by VojtechStep about 1 year ago - 2 comments
Labels: synthetic-homotopy-theory

#867 - Strict categories

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: set-theory, category-theory

#866 - Rename Axiom L to Preunivalence

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 5 comments
Labels: foundation

#865 - Universal property of smash products

Pull Request - State: closed - Opened by maybemabeline about 1 year ago - 9 comments
Labels: fix, synthetic-homotopy-theory

#864 - Nonunital precategories

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 29 comments
Labels: category-theory

#863 - Characteristic subgroups

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: group-theory

#862 - Level-universe compatibility patch

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 1 comment
Labels: repo-maintenance

#861 - Small subcategories

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: fix, category-theory

#860 - A map is an epimorphism if its codiagonal is an equivalence

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 7 comments
Labels: foundation

#859 - Fix broken links in `MIXFIX-OPERATORS.md`

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 4 comments
Labels: website, fix

#858 - A map is an embedding if and only if it has contractible fibers at values

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 1 comment
Labels: foundation

#857 - If a map is an epimorphism, then its codagional is an equivalence.

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 7 comments
Labels: foundation, synthetic-homotopy-theory

#856 - reversing naturality

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago

#855 - Inconsistent direction of natural transformations between small and large categories

Issue - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: category-theory

#854 - Adjunctions of large categories and some minor refactoring

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 4 comments
Labels: group-theory, category-theory

#853 - Tangent spheres

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 2 comments
Labels: synthetic-homotopy-theory

#852 - Classifying invertible maps

Pull Request - State: closed - Opened by maybemabeline about 1 year ago - 4 comments
Labels: foundation

#851 - Make pre-commit hooks talk to git

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 4 comments
Labels: fix, pre-commit

#850 - The perfect core of a group

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 5 comments
Labels: group-theory

#849 - add myself as contributor

Pull Request - State: closed - Opened by UlrikBuchholtz about 1 year ago
Labels: website

#848 - Generate index files based only on tracked files

Issue - State: closed - Opened by fredrik-bakke about 1 year ago - 1 comment
Labels: bug, pre-commit

#847 - Perfect subgroups

Pull Request - State: closed - Opened by UlrikBuchholtz about 1 year ago
Labels: group-theory

#846 - Compatibility patch for Agda 2.6.4

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 4 comments
Labels: repo-maintenance, fix

#845 - The simplex precategory

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 8 comments
Labels: category-theory, order-theory, univalent-combinatorics

#844 - The decidable total order on a standard finite type

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 3 comments
Labels: elementary-number-theory, order-theory, univalent-combinatorics

#843 - Perfect groups

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 1 comment
Labels: group-theory

#842 - Stable homotopy groups

Issue - State: open - Opened by fredrik-bakke about 1 year ago
Labels: synthetic-homotopy-theory

#841 - Sequential colimits

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 27 comments
Labels: synthetic-homotopy-theory

#840 - Patch file generation scripts to ignore `MAlonzo`

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: fix, pre-commit

#839 - Sequential limits

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 36 comments
Labels: foundation

#838 - Functoriality of the quotient operation on groups

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 7 comments
Labels: group-theory, category-theory, refactoring

#837 - Fix links to wikidata to the recommended links; add concept tags at end of file for testing purposes

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: website, mage

#836 - Cleaning up for homotopy groups

Pull Request - State: open - Opened by EgbertRijke about 1 year ago
Labels: group-theory, synthetic-homotopy-theory, higher-group-theory

#835 - The commutator subgroup

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 2 comments
Labels: group-theory

#834 - The long exact sequence of homotopy groups

Issue - State: open - Opened by fredrik-bakke about 1 year ago
Labels: good first issue, synthetic-homotopy-theory

#833 - Define suspension prespectra and maps of prespectra

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: synthetic-homotopy-theory

#832 - Creating internal and external links in Graph Theory

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 4 comments
Labels: website, graph-theory

#831 - Derive the flattening lemma for coequalizers from the flattening lemma for pushouts

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 1 comment
Labels: synthetic-homotopy-theory

#830 - Participating in the MaGE project

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 25 comments
Labels: website, mage

#829 - Clean up the commutators of elements file

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 2 comments
Labels: group-theory

#828 - Introduce the subuniverse P

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: fix, foundation

#827 - Dependent epimorphisms

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: foundation, synthetic-homotopy-theory

#826 - The codiagonal of a map

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: synthetic-homotopy-theory

#825 - Navigation buttons on bottom of webpage do not go anywhere

Issue - State: open - Opened by fredrik-bakke about 1 year ago - 1 comment
Labels: bug, website

#824 - Monomorphisms in the category of groups

Issue - State: open - Opened by EgbertRijke about 1 year ago
Labels: group-theory

#823 - Navigation tables for all files related to cyclic types, groups, and rings

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 3 comments
Labels: website, group-theory, ring-theory, elementary-number-theory, synthetic-homotopy-theory, structured-types

#822 - Negated equality

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 1 comment
Labels: foundation

#821 - Refactor ethane to comply with guidelines

Issue - State: open - Opened by EgbertRijke about 1 year ago
Labels: organic-chemistry

#820 - Cleanup Makefile Agda options, cleanup old targets

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 1 comment

#819 - Pin mdbook versions in the CI

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 3 comments

#818 - Update mdbook-catppuccin, lock mdbook dependencies

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 3 comments
Labels: repo-maintenance, website

#817 - Adding explanation to contractibility of the types of sections and retractions of an equivalence

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: foundation

#816 - Flattening lemma for pushouts 2: descent data boogaloo

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 5 comments
Labels: foundation, synthetic-homotopy-theory

#815 - Nontrivial groups, and a correction of a statement in torsion-free groups

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: group-theory

#814 - Update to Agda 2.6.4

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 25 comments
Labels: CI, repo-maintenance

GitHub / UniMath/agda-unimath issues and pull requests