[[!redirects higher algebra]] [[!redirects Higher algebra in HoTT]] Here we collect articles about doing higher algebra or homotopical algebra in HoTT. ## General ## * [[H-space]] * [[A3-space]] * [[grouplike A3-space]] * [[commutative A3-space]] ## Truncations ## * [[contractible type]] * [[proposition]] * [[set]] * [[groupoid]] ## Set-truncated types ## ### Magmas ### * [[monoid]] * [[commutative monoid]] * [[group]] * [[abelian group]]/[[Z-module]] * [[action]] * [[magma]] * [[power-associative magma]] * [[commutant]] * [[abelian group homomorphism]] * [[bilinear function]] ### Rings, modules, and algebras ### * [[Z-module]]/[[abelian group]] * [[abelian group homomorphism]] * [[Z-algebra]] * [[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]] * [[quadratic form]] * [[diagonal]] * [[diagonal form]] * [[Clifford algebra]] * [[geometric algebra]] * [[algebra (module theory)]] ### Fields and cancellation algebras ### * [[field (ring theory)]] * [[residue field]] * [[Heyting field]] * [[discrete field]] * [[reciprocal function]] * [[rational function]] * [[category of partial functions]] * [[difference quotient]] * [[Hausdorff field]] * [[sequentially Hausdorff field]] * [[calculus 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