# [Agda] Yet another way Agda --without-K is incompatible with univalence

Jesper Cockx Jesper at sikanda.be
Fri Jan 17 12:19:59 CET 2014

```Dear all,

Much to my own surprise, I encountered another problem with the --without-K
option. This is on the latest darcs version of Agda and is unrelated to the
termination checker. As far as I understand, the unification algorithm is
applying the injectivity rule too liberally for data types indexed over
indexed data. But maybe someone else can give a better explanation?

=== BEGIN CODE ===

{-# OPTIONS --without-K #-}

module YetAnotherWithoutKProblem where

-- First, some preliminaries to make this file self-contained.
data _≡_ {a} {A : Set a} (x : A) : A → Set where
refl : x ≡ x

subst : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → Set b) →
{y : A} → x ≡ y → B x → B y
subst B refl b = b

record _≃_ (A B : Set) : Set where
constructor equiv
field
f : A → B
g : B → A
i : (x : A) → g (f x) ≡ x
j : (y : B) → f (g y) ≡ y

-- The univalence axiom.
postulate equiv-to-id : {A B : Set} → A ≃ B → A ≡ B

-- Now consider any concrete space 'mySpace' with a point 'myPoint'.
-- We will show that mySpace has no structure above dimension 2.
postulate mySpace : Set
postulate myPoint : mySpace

-- We define Foo in a way such that 'Foo e' is equivalent with 'refl ≡ e'.
data Foo : myPoint ≡ myPoint → Set where
foo : Foo refl

Foo-equiv : {e : myPoint ≡ myPoint} → Foo e ≃ (refl ≡ e)
Foo-equiv = equiv f g i j
where
f : {e : myPoint ≡ myPoint} → Foo e → refl ≡ e
f foo = refl

g : {e : myPoint ≡ myPoint} → refl ≡ e → Foo e
g refl = foo

i : {e : myPoint ≡ myPoint} (m : Foo e) → g (f m) ≡ m
i foo = refl

j : {e : myPoint ≡ myPoint} (i : refl ≡ e) → f (g i) ≡ i
j refl = refl

-- Here comes the real problem: by injectivity, 'Foo e' is a set ...
test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡ refl
test foo refl = refl

-- ... hence by univalence, so is 'refl ≡ e'.
problem : {e : myPoint ≡ myPoint} → (a : refl ≡ e) → (i : a ≡ a) → i ≡ refl
problem = subst (λ X → (x : X) → (i : x ≡ x) → i ≡ refl)
(equiv-to-id Foo-equiv)
test

=== END CODE ===

All the best,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140117/2be2a9af/attachment.html
```