Usually refers to an Agda compiler option which restricts type checking to be compatible with versions of type theory which do not support uniqueness of identity proofs.

For more information, see "Without K" in the Agda manual. Related to , which implies --without-K.