agda/cubical

Issues

• More elegant construction of ZariskiLattice

  #1110 opened 9 months ago by MatthiasHu
  2

• Formalizing Devalapurkar & Haine

  #1147 opened 4 months ago by Trebor-Huang
  0

• Release new version for agda 2.7

  #1148 opened 3 months ago by felixwellen
  0

• Slightly more generalized universes

  #1022 opened 4 months ago by Trebor-Huang
  2

• `__IMPOSSIBLE__` error in SSet but not in Set

  #1144 opened 4 months ago by FernandoChu
  1

• CI workflow with current agda master

  #1051 opened 6 months ago by felixwellen
  5

• Algebraic geometry

  #1095 opened 6 months ago by mzeuner
  2

• Naming Convention for Disambiguation

  #1126 opened 6 months ago by felixwellen
  1

• Presheaf definition leads to unsolved metavariable for base category

  #1010 opened a year ago by jpoiret
  3

• arithmetic operations of Cubical.Data.Rationals is super slow

  #1124 opened 7 months ago by onestruggler
  1

• Solver for wild categories

  #1118 opened 8 months ago by felixwellen
  0

• Redundancy in definitions for pre-categories and categories

  #1009 opened 9 months ago by mortberg
  15

• Duplication of code in the library

  #1017 opened a year ago by jpoiret
  3

• Move Properties of UnivariateList-Polynomials to CommRing

  #944 opened 2 years ago by felixwellen
  0

• Increasing Universe Polymorphism in Yoneda lemma

  #989 opened 9 months ago by maxsnew
  3

• Figure out why the CommRingSolver doesn't work in this case

  #1097 opened 10 months ago by felixwellen
  5

• `make` fails on macOS Sonoma 14.2.1 with Apple Silicon

  #1090 opened 10 months ago by jordydickinson
  1

• Make the CommRingSolver work better with concrete rings

  #1101 opened 10 months ago by felixwellen
  0

• SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids

  #1088 opened 10 months ago by mzeuner
  1

• Suggested heap size for CI

  #1074 opened a year ago by felixwellen
  1

• Additions to the powerset module

  #1052 opened a year ago by rahulc29
  2

• Some Files are never checked

  #1054 opened a year ago by felixwellen
  6

• Release version v0.5 while changing the release process

  #1014 opened a year ago by felixwellen
  12

• Citation.cff

  #1015 opened a year ago by anuyts
  4

• Change the Constructor Name of Sequential Colimits

  #1046 opened a year ago by kangrongji
  2

• Note licence exceptions

  #1018 opened a year ago by felixwellen
  2

• Remove `isSet` accessors for algebraic structures?

  #1034 opened a year ago by MatthiasHu
  3

• Agda Nat exports Unit somehow

  #840 opened 2 years ago by thomas-lamiaux
  5

• `RecordEquiv` reflection doesn't seem to handle implicit field arguments

  #995 opened 2 years ago by Trebor-Huang
  6

• Update Table of Reviewers

  #942 opened a year ago by felixwellen
  1

• Readme refers to tag: v0.5 for Agda v2.6.3 not such tag exist in repo

  #987 opened a year ago by sebeaumont
  4

• Where should `π₁(RP²)` be?

  #1016 opened a year ago by ice1000
  1

• Suggestion: provide proof that set-coequalizers of finite sets are finite?

  #1004 opened 2 years ago by finegeometer
  2

• Swapping the argument order in equational reasoning

  #998 opened 2 years ago by maxsnew
  5

• Define Universal Property for Algebraic Structures

  #943 opened 2 years ago by felixwellen
  1

• Data.Bool.and and Data.Bool.or are pattern matching on second argument

  #962 opened 2 years ago by phadej
  3

• `Unknown warning flag: UnsupportedIndexedMatch`

  #982 opened 2 years ago by vezwork
  4

• Code for Data.Fin.Properties needs to migrate to Cubical.Nat.Properties/Order

  #978 opened 2 years ago by xekoukou
  0

• Move _$_ from Reflection.Base to Foundations.Function

  #894 opened 2 years ago by ecavallo
  3

• Consider caching Nix artifacts via Cachix

  #960 opened 2 years ago by phijor
  0

• Release cubical-0.4

  #956 opened 2 years ago by felixwellen
  5

• Deduplicate subtypePathReflection

  #930 opened 2 years ago by felixwellen
  0

• Rename Functions.FunExtEquiv to Functions.FunExt?

  #835 opened 2 years ago by ecavallo
  0

• Cubical not typechecking upon install

  #932 opened 2 years ago by cosmoviola
  13

• Update README and add a list of reviewers

  #885 opened 2 years ago by felixwellen
  3

• Where should I put stuffs about 2LTT?

  #911 opened 2 years ago by kangrongji
  0

• Use 'assign' for PR management

  #905 opened 2 years ago by felixwellen
  0

• Should we have a Discord server?

  #886 opened 2 years ago by mzeuner
  2

• Short Names or Long Names?

  #844 opened 2 years ago by kangrongji
  5

• Refactor Int ?

  #838 opened 2 years ago by thomas-lamiaux
  1