[[!redirects algebra]] [[!redirects Algebra in HoTT]] Here we collect articles about doing set-level algebra in HoTT. ## Decidable objects ## * [[booleans]] * [[decidable universal quantifier]] * [[decidable existential quantifier]] * [[decidable directed graph]] * [[decidable setoid]] * [[decidable set]] * [[decidable preordered type]] * [[decidable strict order]] * [[decidable dense strict order]] ## Abelian groups ## * [[abelian group]] * [[halving group]] category: not redirected to nlab yet