Homotopy Type Theory Higher algebra > history (Rev #5)

Here we collect articles about doing higher algebra or homotopical algebra in HoTT.

Definitions

• contractible type
• proposition
• set
• H-space
• A3-space
• grouplike A3-space
• commutative A3-space
• grouplike A3-space
• monoid
• commutative monoid
• group
• abelian group
• Z-algebra
• unital Z-algebra
• ring
• commutative ring
• action
• power-associative magma
• abelian group homomorphism

References

• HoTT Book