UniMath/agda-unimath

Issues

• List of notable theorems

  #1214 opened a month ago by EgbertRijke
  14

• Attributions for "100 theorems"

  #1203 opened 25 days ago by fredrik-bakke
  6

• Mdbook doesn't render links in headers in the right-hand bar

  #1204 opened a month ago by fredrik-bakke
  2

• Undetected ill-formed macro invocations

  #1200 opened a month ago by fredrik-bakke
  0

• Search engine support

  #1194 opened a month ago by fredrik-bakke
  2

• CI should error when `{{#bibliography}}` is invoked and there are no references

  #1175 opened 2 months ago by fredrik-bakke
  1

• Formalized results from the literature

  #1055 opened 9 months ago by fredrik-bakke
  3

• References for citations vs. further reading

  #1164 opened 3 months ago by fredrik-bakke
  0

• Idempotents in Intensional Type Theory

  #1103 opened 8 months ago by fredrik-bakke
  0

• Use box-drawing characters for character diagrams

  #1141 opened 5 months ago by fredrik-bakke
  0

• Inconsistent font sizes in code blocks

  #1053 opened 6 months ago by fredrik-bakke
  0

• Functoriality of the pullback-hom

  #1134 opened 7 months ago by fredrik-bakke
  0

• Postulating colimits

  #1122 opened 7 months ago by fredrik-bakke
  2

• Document external dependencies for building the website

  #1132 opened 7 months ago by VojtechStep
  0

• Prove uniqueness of homotopy and equivalence induction

  #1123 opened 7 months ago by fredrik-bakke
  0

• Construct `compute-glue-cogap` from appropriate infrastructure

  #1120 opened 7 months ago by fredrik-bakke
  0

• Competing conventions for operations on propositions

  #984 opened 7 months ago by fredrik-bakke
  5

• Equality proofs and proofs of propositions in `elementary-number-theory` should be abstracted

  #1106 opened 8 months ago by fredrik-bakke
  0

• Small refactorings for elementary number theory

  #1043 opened 8 months ago by fredrik-bakke
  21

• Explore what we want to call "isomorphisms"

  #1072 opened 8 months ago by VojtechStep
  1

• The concepts macro does not detect HTML escaped characters

  #1075 opened 8 months ago by fredrik-bakke
  0

• The concepts macro should require the `WD` field if the `WDID` field is specified and vice versa

  #1076 opened 8 months ago by fredrik-bakke
  0

• Wikidata labels should be capitalized when generating the link, not in the label field itself

  #1077 opened 8 months ago by fredrik-bakke
  0

• The concepts macro allows linebreaks in the quoted parts of the invocation

  #1092 opened 8 months ago by VojtechStep
  0

• Argument order for coherence triangles

  #1041 opened 9 months ago by fredrik-bakke
  0

• Clean up git history

  #1068 opened 8 months ago by fredrik-bakke
  10

• Target: Sequential Colimits in Homotopy Type Theory

  #1080 opened 8 months ago by VojtechStep
  0

• Concepts macro doesn't recognize names of Agda data types

  #1073 opened 8 months ago by fredrik-bakke
  1

• Create `logic` namespace

  #1069 opened 8 months ago by fredrik-bakke
  0

• Rename `UU` to `Type`

  #1067 opened 8 months ago by fredrik-bakke
  0

• Bibliography

  #957 opened 8 months ago by EgbertRijke
  1

• The search functionality seems to be limited to 15 results

  #1062 opened 8 months ago by EgbertRijke
  1

• Factor metafiles to a subdirectory

  #1061 opened 8 months ago by fredrik-bakke
  0

• Small refactorings for real numbers

  #1060 opened 9 months ago by fredrik-bakke
  0

• Investigate memory usage when typechecking the whole library

  #985 opened 9 months ago by VojtechStep
  2

• Allow manually running perf testing on pull requests

  #1049 opened 9 months ago by VojtechStep
  0

• Record user statistics for the webpage

  #1029 opened 9 months ago by fredrik-bakke
  2

• Record performance statistics for type-checking

  #1030 opened 9 months ago by fredrik-bakke
  0

• Level universe

  #1023 opened 10 months ago by fredrik-bakke
  1

• Idea: use coherently invertible maps as default notion of equivalence

  #946 opened a year ago by fredrik-bakke
  1

• The module index generator doesn't support modules with unicode characters in their names

  #1027 opened 9 months ago by fredrik-bakke
  14

• Resolve duplicate definitions

  #992 opened 10 months ago by VojtechStep
  0

• Discuss replacing `-whisk-` with `-whisker-`

  #982 opened 10 months ago by VojtechStep
  2

• Sync up nomenclature between towers and cotowers

  #965 opened 10 months ago by VojtechStep
  3

• Add `is-sequential-colimit`

  #966 opened a year ago by VojtechStep
  0

• Retracts of sequential diagrams

  #964 opened a year ago by VojtechStep
  1

• Idea: refactor (nonunital) precategories to have both directions of the associativity witness

  #934 opened a year ago by fredrik-bakke
  1

• Autoformatting for Python files

  #939 opened a year ago by fredrik-bakke
  3

• Idea: refactor categories to build on the theory of wild categories

  #933 opened a year ago by fredrik-bakke
  2

• Necessary truncations on formalizing cardinal arithmetic

  #938 opened a year ago by ElifUskuplu
  0