We use the axiom instead of `sorry` to avoid a tsunami of warnings.
init/category
init.control
lean.name