[[!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]] ## Magmas ## * [[monoid]] * [[commutative monoid]] * [[group]] * [[abelian group]]/[[Z-module]] * [[divisible group]] * [[halving group]]/[[D-module]] * [[torsion-free divisible group]]/[[Q-module]] * [[torsion-free halving group]] * [[action]] * [[magma]] * [[power-associative magma]] * [[commutant]] * [[abelian group homomorphism]] * [[bilinear function]] ### Rings, modules, and algebras ### * [[Z-module]]/[[abelian group]] * [[Q-module]]/[[torsion-free divisible group]] * [[abelian group homomorphism]] * [[bilinear function]] * [[Z-algebra]] * [[Q-algebra]] * [[square function]] * [[quadratic function]] * [[characteristic]] * [[unital Z-algebra]] * [[ring]] * [[commutative ring]] * [[algebra (ring theory)]] * [[commutative algebra (ring theory)]] * [[polynomial ring]] * [[univariate polynomial ring]] * [[power function]] * [[polynomial function]] * [[function algebra]] * [[module]] * [[bimodule]] * [[graded module]] * [[filtered algebra]] * [[quadratic form]] * [[diagonal]] * [[diagonal form]] * [[Clifford algebra]] * [[geometric algebra]] * [[algebra (module theory)]] ## Sequences ## * [[sequence]] * [[left shift operator]] * [[right shift operator]] * [[Z-module]] * [[sequential polynomial]] * [[series operator]] * [[inverse series operator]] * [[sequential derivative]] * [[Q-module]] * [[sequential antiderivative]] * [[sequential differential operator]] * [[sequential linear differential equation]] * [[sequential exponential]] * [[sequential sine]] * [[sequential cosine]] * [[bidirectional sequence]] * [[bidirectional shift operators]] ## Fields and cancellation algebras ## * [[field (ring theory)]] * [[residue field]] * [[Heyting field]] * [[discrete field]] * [[ordered field]] * [[Archimedean ordered field]] * [[interval-complete Archimedean ordered field]] * [[Dedekind complete Archimedean ordered field]] * [[Cauchy complete Archimedean ordered field]] * [[integral domain]] * [[residue integral domain]] * [[Heyting integral domain]] * [[discrete integral domain]] * [[ordered integral domain]] * [[Archimedean ordered integral domain]] * [[interval-complete Archimedean ordered integral domain]] * [[Dedekind complete Archimedean ordered integral domain]] * [[skewfield]] * [[residue skewfield]] * [[Heyting skewfield]] * [[discrete skewfield]] * [[domain (ring theory)]] * [[residue domain]] * [[Heyting domain]] * [[discrete domain]] * [[commutative reciprocal ring]] * [[commutative residue reciprocal ring]] * [[commutative Heyting reciprocal ring]] * [[commutative discrete reciprocal ring]] * [[commutative division ring]] * [[commutative residue division ring]] * [[commutative Heyting division ring]] * [[commutative discrete division ring]] * [[commutative cancellation ring]] * [[commutative residue cancellation ring]] * [[commutative Heyting cancellation ring]] * [[commutative discrete cancellation ring]] * [[reciprocal ring]] * [[residue reciprocal ring]] * [[Heyting reciprocal ring]] * [[discrete reciprocal ring]] * [[division ring]] * [[residue division ring]] * [[Heyting division ring]] * [[discrete division ring]] * [[cancellation ring]] * [[residue cancellation ring]] * [[Heyting cancellation ring]] * [[discrete cancellation ring]] * [[reciprocal Z-algebra]] * [[residue reciprocal Z-algebra]] * [[Heyting reciprocal Z-algebra]] * [[discrete reciprocal Z-algebra]] * [[division Z-algebra]] * [[residue division Z-algebra]] * [[Heyting division Z-algebra]] * [[discrete division Z-algebra]] * [[cancellation Z-algebra]] * [[residue cancellation Z-algebra]] * [[Heyting cancellation Z-algebra]] * [[discrete cancellation Z-algebra]] ## References * [[HoTT Book]] category: navigation