Hypertopes

Stream: general

[Aresh Pourkavoos]

@Violeta Hernández and I are currently formalizing hypertopes on a mathlib branch of the same name. Hopefully there will be a lot of crosstalk between it and the polytopes branch once both are ready. Since we've just started, there are no major issues yet, I just wanted to start the thread in case something comes up.

[Eric Wieser]

(branch#hypertopes?)