UniMath/agda-unimath

Issues

• Refactor categories to come equipped with an identity system on its morphisms

  #932 opened a year ago
  2

• Project: Sheaves and excision with respect to regular cd-structures

  #930 opened a year ago
  4

• The equivalences on hom-sets in adjunctions of large (pre)categories go the unnatural way

  #926 opened a year ago
  1

• Identity system on implicit Pi types

  #925 opened a year ago
  4

• Refactor extensionality of `Torsor-Abstract-Group`

  #902 opened a year ago
  0

• `apply-universal-property` vs. `recursion`

  #888 opened a year ago
  2

• Add a favicon

  #872 opened a year ago
  7

• Flattening lemma for sequential colimits

  #869 opened a year ago
  0

• Standard sequential colimit and its functoriality

  #868 opened a year ago
  2

• Inconsistent direction of natural transformations between small and large categories

  #855 opened a year ago
  0

• Generate index files based only on tracked files

  #848 opened a year ago
  1

• Stable homotopy groups

  #842 opened a year ago
  0

• The long exact sequence of homotopy groups

  #834 opened a year ago
  0

• Navigation buttons on bottom of webpage do not go anywhere

  #825 opened 9 months ago
  1

• Monomorphisms in the category of groups

  #824 opened a year ago
  0

• Refactor ethane to comply with guidelines

  #821 opened a year ago
  0

• Navigation is impossible on mobile

  #811 opened a year ago
  11

• Lazily fetch `searchindex.json`

  #777 opened a year ago
  0

• Run `link-check` sooner, and irrespective of other pipelines

  #775 opened a year ago
  9

• Category Theory

  #769 opened a year ago
  7

• Remove private definitions from the library

  #768 opened a year ago
  1

• Show that spans are equivalent to relations

  #767 opened a year ago
  0

• Conventions for consistent capitalization

  #759 opened a year ago
  4

• Define unlabeled rooted trees

  #749 opened a year ago
  0

• Define the predicate that `f` maps two different elements to the same value

  #748 opened a year ago
  0

• Open claims for partitions of finite types

  #747 opened a year ago
  0

• Show that the type of Ferrers diagrams of any finite type is π-finite

  #746 opened a year ago
  0

• Show that the number of decidable equivalence relations on a finite type is a Stirling number of the second kind

  #745 opened a year ago
  0

• Show that the map from a pointed `k+1`-element type to the complement of the point is an equivalence

  #744 opened a year ago
  0

• Open claims about `2`-element types

  #743 opened a year ago
  0

• Define `ℂP∞` as the `2`-truncation of the `2`-sphere

  #742 opened a year ago
  0

• Define equivalences of unlabeled structures of a species

  #741 opened a year ago
  0

• Define unital algebras over a ring

  #740 opened a year ago
  0

• Open claims regarding modalities

  #739 opened a year ago
  0

• Open claims about orthogonal factorization systems

  #738 opened a year ago
  0

• Equivalent sets have isomorphic symmetric concrete groups

  #737 opened a year ago
  0

• Equivalences of concrete groups are isomorphisms of concrete groups

  #736 opened a year ago
  0

• Open claims about surjective maps

  #735 opened a year ago
  0

• Show that the type of partial elements is a directed complete poset

  #734 opened a year ago
  0

• Show that `Connected-Map-Into-Truncated-Type l2 k l A` is `k - l - 2`-truncated

  #733 opened a year ago
  0

• Define maximal ideals for rings and commutative rings

  #731 opened a year ago
  0

• Factor out families of equivalences

  #728 opened 10 months ago
  2

• pre-commit shouldn't give an error on empty sections

  #721 opened a year ago
  3

• Remove all holes (and `--allow-unsolved-metas` flags)

  #714 opened a year ago
  1

• Clean up the universal property of the integers

  #713 opened a year ago
  0

• Markdown conventions script does not trigger on ill-formed code blocks

  #704 opened a year ago
  0

• Formalize the Hopf Fibration

  #702 opened a year ago
  0

• Trailing whitespace for line breaks in markdown code

  #696 opened a year ago
  2

• git checkout is >500MB

  #689 opened a year ago
  10

• `make website` shouldn't type check the library

  #679 opened a year ago
  3