CHANGELOG

agda · Jun 7, 2024 · 8048d00 · 8048d00
1 parent 4fbf964
commit 8048d00
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -242,6 +242,12 @@ Additions to existing modules
  record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ))
  record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ))
  ```
+ and additional manifest fields for sub-bundles arising from these in:
+ ```agda
+ IdempotentCommutativeMonoid
+ IdempotentSemiring
+ ```
+
 
 * In `Algebra.Bundles.Raw`
  ```agda