mathlib3

aba7a7bb - Definition of hypertope finished except for connectedness