[[!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]] ## Rings, modules, and algebras ## * [[integers]] * [[rational numbers]] * [[abelian group]]/[[Z-module]] * [[divisible group]] * [[torsion-free divisible group]]/[[Q-module]] * [[halving group]]/[[D-module]] * [[abelian group homomorphism]] * [[bilinear function]] * [[ring]] * [[commutative ring]] * [[polynomial ring]] * [[univariate polynomial ring]] ## Sequences ## * [[sequence]] * [[left shift operator]] * [[right shift operator]] * [[Z-module]] * [[sequential polynomial]] * [[series operator]] * [[inverse series operator]] * [[sequential derivative]] * [[Q-vector space]] * [[sequential antiderivative]] ## References * [[HoTT Book]] * Henri Lombardi, Claude Quitté, Commutative algebra: Constructive methods. Finite projective modules, [arXiv:1605.04832](https://arxiv.org/abs/1605.04832) category: not redirected to nlab yet