[[!redirects higher algebra]] [[!redirects Higher algebra in HoTT]] < [[nlab:higher algebra]] Here we collect articles about doing higher algebra or homotopical algebra in HoTT. ## Simplicial models ## * [[totally ordered type]] * [[simplex category]] * [[simplicial type]] ## Truncations ## * [[contractible type]] * [[proposition]] * [[set]] * [[groupoid]] ## Groupoid-truncated types ## * [[groupoid enriched in monoids]]