package mugen

The displacement algebra.

The type of level variables.

The type of freely generated levels.

var is Syntax.Free.var

Smarter version of Syntax.Endo.shifted that collapses multiple displacements

• raises Invalid_argument

  When it attempts to shift the top level.

top is Syntax.Endo.top

equal l1 l2 checks whether l1 and l2 are the same universe level.

• raises Invalid_argument

  When l1 or l2 is shifted top.

lt l1 l2 checks whether l1 is strictly less than l2. Note that trichotomy fails for general universe levels.

• raises Invalid_argument

  When l1 or l2 is shifted top.

leq l1 l2 checks whether l1 is less than or equal to l2. Note that trichotomy fails for general universe levels.

• raises Invalid_argument

  When l1 or l2 is shifted top.

gt l1 l2 is lt l2 l1.

geq l1 l2 is leq l2 l1.

Infix notation.