Function signature 

pub fn signature(
    kind: Kind,
    levels: &[Universe],
    equality: &str,
) -> Result<Term, KernelError>

The canonical Lean signature, with explicit universe instances throughout.