search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
452 stars 138 forks source link

Add Boolean Rings #1146

Closed Freek98 closed 1 month ago

Freek98 commented 2 months ago

This PR introduces Boolean rings as idempotent commutative rings.

We then proceed to show these rings allow for the usual symbols and satisfy the usual axioms for boolean algebras.