include "Universes.ma".

ninductive Compare: Type[0] ≝
  Equal: Compare
| Greater: Compare
| Less: Compare.