eqT package:Agda

Type of the equation, living in same context as the rhs.
Can be reduced eagerly.
NotHidden.
Builtin EQUALITY.
Hidden. Empty or Level.
Range of the rewrite expression, if any.
NotHidden.
Sort of this type.
Hidden.