Checks an expression against a type in a given context.

Checks all declarations in a module.

Cubical composition operation.

Checks if two values are convertible (equivalent).

Asserts that two values are convertible, raising an error if not.

Evaluates an expression in a given context.

Evaluates AND formula.

Evaluates OR formula.

Extracts level from Universe or Dir.

Extracts path, u0, and u1 from a PathP type.

Extracts domain and name/codomain from a Pi type.

Helper for Set or Kan types.

Extracts domain and name/codomain from a Sigma type.

Cubical homogeneous composition operation.

Cubical hfill operation.

Identity value constructor.

Maximum of two universe levels.

Implication value constructor (non-dependent Pi).

Infers the type of an expression in a given context.

Infers the type of a value (in empty context).

Negates a formula.

Normalizes a term by evaluating it and then reading it back.

Converts a value back to an AST term (readback/reify).

Cubical transFill operation.

Cubical generalized transport operation.

First projection evaluator.

Second projection evaluator.