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.
NotHidden.
Sort of this type.
Hidden.