Added ⊔ for levels
Added ∑-type, reformulated × as special ∑, added +
Starting to implement Tarski's geometry with Makarios's amendments
see http://arxiv.org/abs/1306.0066