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.
2
questions
9
votes
1
answer
196
views
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}...
- 5,877
4
votes
1
answer
120
views
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 ...
- 5,877