# Without K¶

The option `--without-K`

adds some restrictions to Agda’s
typechecking algorithm in order to ensure compatability with versions
of type theory that do not support UIP (uniqueness of identity
proofs), such as HoTT (homotopy type theory).

The option `--with-K`

can be used to override a global
`--without-K`

in a file, by adding a pragma
`{-# OPTIONS --with-K #-}`

. This option is enabled by default.

## Restrictions on pattern matching¶

When the option `--without-K`

is enabled, then Agda only accepts
certain case splits. More specifically, the unification algorithm for
checking case splits cannot make use of the deletion rule to solve
equations of the form `x = x`

.

For example, the obvious implementation of the K rule is not accepted:

```
K : {A : Set} {x : A} (P : x ≡ x → Set) →
P refl → (x≡x : x ≡ x) → P x≡x
K P p refl = p
```

Pattern matching with the constructor `refl`

on the argument `x≡x`

causes `x`

to be unified with `x`

, which fails because the deletion
rule cannot be used when `--without-K`

is enabled.

On the other hand, the obvious implementation of the J rule is accepted:

```
J : {A : Set} (P : (x y : A) → x ≡ y → Set) →
((x : A) → P x x refl) → (x y : A) (x≡y : x ≡ y) → P x y x≡y
J P p x .x refl = p x
```

Pattern matching with the constructor `refl`

on the argument `x≡y`

causes `x`

to be unified with `y`

. The same applies to Christine
Paulin-Mohring’s version of the J rule:

```
J′ : {A : Set} {x : A} (P : (y : A) → x ≡ y → Set) →
P x refl → (y : A) (x≡y : x ≡ y) → P y x≡y
J′ P p ._ refl = p
```

For more details, see Jesper Cockx’s PhD thesis Dependent Pattern Matching and Proof-Relevant Unification [Cockx (2017)].

## Restrictions on termination checking¶

When `--without-K`

is enabled, Agda’s termination checker restricts
structural descent to arguments ending in data types or `Size`

.
Likewise, guardedness is only tracked when result type is data or
record type:

```
data ⊥ : Set where
mutual
data WOne : Set where wrap : FOne → WOne
FOne = ⊥ → WOne
postulate iso : WOne ≡ FOne
noo : (X : Set) → (WOne ≡ X) → X → ⊥
noo .WOne refl (wrap f) = noo FOne iso f
```

`noo`

is rejected since at type `X`

the structural descent
`f < wrap f`

is discounted `--without-K`

:

```
data Pandora : Set where
C : ∞ ⊥ → Pandora
postulate foo : ⊥ ≡ Pandora
loop : (A : Set) → A ≡ Pandora → A
loop .Pandora refl = C (♯ (loop ⊥ foo))
```

`loop`

is rejected since guardedness is not tracked at type `A`

`--without-K`

.

## Restrictions on universe levels¶

When `--without-K`

is enabled, some indexed datatypes must be
defined in a higher universe level. In particular, the types of all
indices should fit in the sort of the datatype.

For example, usually (i.e. `--with-K`

) Agda allows the following
definition of equality:

```
data _≡₀_ {ℓ} {A : Set ℓ} (x : A) : A → Set where
refl : x ≡₀ x
```

However, with `--without-K`

it must be defined at a higher
universe level:

```
data _≡′_ {ℓ} {A : Set ℓ} : A → A → Set ℓ where
refl : {x : A} → x ≡′ x
```