← Feed

Posts

• Post #2493675

  A month ago I gave a talk on joint work with Christian Sattler, on axioms for higher category theory. The slides are now available here: https://dwarn.se/slides/7wftop.pdf The idea is to add axioms to homotopy type theory, to allow a development of higher category theory. Notably, this is consistent with the idea that types are spaces, and does not require any significant changes to the type theory.

• Post #908431

  A HoTT exercise: let \( A \) be a type with a binary operation \( * : A \to A \to A \). Suppose that \( * \) is associative, commutative, and idempotent, in the sense that \( \Pi_{a\, b\, c : A} a * (b * c) = (a * b) * c \), \( \Pi_{a\, b : A} a * b = b * a \) and \( \Pi_{a : A} a * a = a \). Show that \( A \) is an hset (and hence a semilattice in the ordinary sense).