[[!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]] ## Inverse images ## * [[inverse image]] * [[iterated inverse image]] * [[infinitely iterated inverse image]] ## Images * [[axiom of replacement]] ## Rings, modules, and algebras ## * [[abelian group]]/[[Z-module]] * [[divisible group]] * [[torsion-free divisible group]]/[[Q-module]] * [[halving group]]/[[D-module]] * [[abelian group homomorphism]] * [[bilinear function]] * [[ring]] * [[commutative ring]] * [[algebra (ring theory)]] * [[Q-algebra]] * [[commutative algebra (ring theory)]] * [[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]] ## Relations ## * [[binary relation]] * [[functional relation]] * [[entire relation]] * [[apartness relation]] * [[order]] * [[strict order]] ## Ordered commutative rings ## * [[ordered integral domain]] * [[Archimedean ordered integral domain]] * [[ordered field]] * [[Archimedean ordered field]] * [[sequentially Cauchy complete Archimedean ordered field]] ## 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