Questions tagged [without-k]

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.

Filter by
Sorted by
Tagged with
4 votes
1 answer

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

In my understanding, --without-K changes the index unification algorithm so that deletion rules are no longer used, as described in Jesper Cockx' "pattern ...
9 votes
1 answer

How does the elimination rule of the heterogeneous equality type imply a weak version of K?

A heterogeneous equality type has the former $$\cfrac{\Gamma\vdash A~\texttt{type} \quad \Gamma\vdash B~\texttt{type} \quad \Gamma\vdash a:A \quad \Gamma\vdash b:B}{\Gamma\vdash a\simeq b~\texttt{type}...