Why does Agda's `--without-K` option also affect the indices of inductive types, where they have to be of lower levels?

Question

In my understanding, --without-K changes the index unification algorithm so that deletion rules are no longer used, as described in Jesper Cockx' "pattern matching without K" paper. However, the elimination rule of the heterogeneous equality type still implies a weaker version of K, while the ability to define a heterogeneous equality type has nothing to do with index unification. Agda rules out the definition of a heterogeneous equality type by disallowing the type abstraction in the index, but why does this criterion work? Is there any reference on that?

Answer 1

$\newcommand{\Eq}{\dot{\mathsf{Eq}}}$ $\newcommand{\refl}{\mathsf{refl}}$

Per my answer to your other related question, the inductive definition of heterogeneous equality actually does not imply a weak version of axiom K. The idea that it does is some combination of a misreading of the meaning of heterogeneous equality, and 'folklore' not retaining a crucial detail in Conor McBride's thesis.

Rather, the inductive definition:

data HEq (A : Set i) (a : A) : (B : Set i) → B → Set (suc i) where
  refl : HEq A a A a

is equivalent to the type:

$$Σ_{P : A =_{\mathcal{U}} B}\ \mathsf{transport}_P\ a =_B b$$

If we denote this latter type by $\Eq$ (since it's actually equality of pointed types), then the naive statement of 'uniqueness of identity proofs':

$$\Eq(\Eq(A,a,B,b), e, \Eq(A,a,A,a),(\refl,\refl))$$

is actually easily proved by two uses of $J$. Two uses of $J$ also suffices to translate from $\Eq$ to $\mathsf{HEq}$, and it's pretty clearly the inverse of the obvious map in the other direction ($\refl$ maps to $(\refl, \refl)$ and vice versa). Also, it's important to note that this theorem is not the same as axiom K, which is a modified induction principle which doesn't follow from the standard one, even for $\mathsf{HEq}$.

Now, if you ask what universe $\Eq$ is in, Agda will tell you the same answer as the one it forces for $\mathsf{HEq}$. It's big, because of the $A = B$ component. It could (in principle) be as small as $A$ and $B$, but that isn't enabled by the uniform definition of $=$, nor the --without-K checker. It can't be any smaller than $A$ and $B$, though, if you want to account for univalence, because there is a correspondence between $A = B$ and certain functions $A → B$.

With axiom K, though, the type is a singleton, and Agda allows a really limited sort of small sizing that covers it. For instance, Agda actually accepts the definition:

data Eq (A : Set ℓ) (a : A) : A → Set where
  refl : Eq A a a

So, the equality type for arbitrarily large types can live in the lowest universe, as long as K is enabled.