Max Zeuner

This PR proves a "comparison lemma" for sheaves on distributive lattices: Given a presheaf on a basis of a distributive lattice taking values in an arbitrary category (with limits) and...

Use the ringsolver with variables in context

1

I often find myself in the situation where I want to use the ring solver for parts of a long argument like this: ``` ... ≡⟨ ... ⟩ s ·...

See https://github.com/agda/cubical/issues/1095

Algebraic geometry

1

By now, the library has quite a bit of stuff on (constructive) algebraic geometry, but it is spread out. The stuff based on the lattice theoretic approach of [Coquand, Lombardy...

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

1

The fact that morphisms preserve finite sums is proven for rings only but does already hold for monoids! The lemma should be proven in `Monoid.BigOp` first and then for semirings...

Redoing the relevant parts of https://github.com/agda/cubical/pull/1068 for finitely presented algebras and this time without raising universe levels.

This PR contains a version of karatsubas algorithm for multiplying two polynomials in R[X] that does not require R to have decidable equality or an apartness relation. For now its...

This PR proves that lifting functor from sets in a universe to sets in the successor universe is fully faithful and preserves (small) limits. It is a less opaque rewrite...