Mugen
module StructuredType : module type of StructuredType
Structured types used in this library
module Shift : module type of Shift
Displacement algebras
module ShiftWithJoin : module type of ShiftWithJoin
Displacement algebras with joins
module Syntax : module type of Syntax
Syntax of universe levels with displacements
module Semantics : module type of Semantics
Semantic operations for universe levels with displacements